wrong get-value answer

[sy6sy2]

Hi,

I have a project that needs to use SMT solvers. My project can works with Z3, CVC4 and BOOLECTOR.

In order to know which one is the best I run my project with each solvers.

But in one case, the get-value reply of Boolector seems wrong.

Here you can find the formula file in order to reproduce the bug:

(set-logic QF_ABV)

; ------[ BOA: Entry variables declarations of BB 0_0x574 -- ∅ (BB entry point of the formula) ]------

(declare-fun memory_entry_0_0x574-empty () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun ebx_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun ecx_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun edx_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun esi_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun edi_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun ebp_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun esp_entry_0_0x574-empty () (_ BitVec 32))
(declare-fun OF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun SF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun ZF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun PF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun CF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun AF_entry_0_0x574-empty () (_ BitVec 1))
(declare-fun DF_entry_0_0x574-empty () (_ BitVec 1))

; ------[ BOA: Concrete regs at BB 0_0x574 -- ∅ entry ]------

(assert (= ebx_entry_0_0x574-empty (_ bv1396 32)))
(assert (= ecx_entry_0_0x574-empty (_ bv1048580 32)))
(assert (= ebp_entry_0_0x574-empty (_ bv1048568 32)))
(assert (= esp_entry_0_0x574-empty (_ bv1048560 32)))
(assert (= CF_entry_0_0x574-empty (_ bv0 1)))
(assert (= ZF_entry_0_0x574-empty (_ bv0 1)))
(assert (= SF_entry_0_0x574-empty (_ bv0 1)))
(assert (= PF_entry_0_0x574-empty (_ bv1 1)))
(assert (= OF_entry_0_0x574-empty (_ bv0 1)))
(assert (= AF_entry_0_0x574-empty (_ bv0 1)))
(assert (= DF_entry_0_0x574-empty (_ bv0 1)))

; ------[ BOA: Concrete stack 32 at BB 0_0x574 -- ∅ entry ]------

(assert (= (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048556 32) (_ bv3 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048556 32) (_ bv2 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048556 32) (_ bv1 32))
) (select memory_entry_0_0x574-empty (_ bv1048556 32))))) (_ bv1396 32)))
(assert (= (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048560 32) (_ bv3 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048560 32) (_ bv2 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048560 32) (_ bv1 32))
) (select memory_entry_0_0x574-empty (_ bv1048560 32))))) (_ bv1048580 32)))
(assert (= (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048568 32) (_ bv3 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048568 32) (_ bv2 32))
) (concat (select memory_entry_0_0x574-empty (bvadd (_ bv1048568 32) (_ bv1 32))
) (select memory_entry_0_0x574-empty (_ bv1048568 32))))) (_ bv1048576 32)))

; ------[ Formula of BB 0_0x574-empty ]------

; ------[ ####  Instr #0: @0x574: add ebx, 0x1a8c   #### ]------

; ------[   ****    DBA instr #0: res32<32> := (0x00001a8c + ebx<32>)   **** ]------
(define-fun
  res320_0_0x574-empty () (_ BitVec 32) (bvadd ebx_entry_0_0x574-empty (_ bv6796 32)))

; ------[   ****    DBA instr #1: OF<1> := ((ebx<32>{31} = 0<1>) & (ebx<32>{31} != res32<32>{31}))  **** ]------
(define-fun
  OF_exit_0_0x574-empty () (_ BitVec 1)
  (bvand (bvcomp ((_ extract 31 31) ebx_entry_0_0x574-empty) (_ bv0 1))
  (bvnot
  (bvcomp ((_ extract 31 31) ebx_entry_0_0x574-empty)
  ((_ extract 31 31) res320_0_0x574-empty)))))

; ------[   ****    DBA instr #2: SF<1> := (res32<32> <s 0<32>) **** ]------
(define-fun
  SF_exit_0_0x574-empty () (_ BitVec 1)
  (ite (bvslt res320_0_0x574-empty (_ bv0 32)) (_ bv1 1) (_ bv0 1)))

; ------[   ****    DBA instr #3: ZF<1> := (res32<32> = 0<32>)  **** ]------
(define-fun
  ZF_exit_0_0x574-empty () (_ BitVec 1) (bvcomp res320_0_0x574-empty (_ bv0 32)))

; ------[   ****    DBA instr #4: AF<1> := (12<5> + (extu ebx<32>{0,3} 5)){4}   **** ]------
(define-fun
  AF_exit_0_0x574-empty () (_ BitVec 1)
  ((_ extract 4 4)
  (bvadd ((_ zero_extend 1) ((_ extract 3 0) ebx_entry_0_0x574-empty)) (_ bv12 5))))

; ------[   ****    DBA instr #5: PF<1> :=  !  ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^       res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}))  **** ]------
(define-fun
  PF_exit_0_0x574-empty () (_ BitVec 1)
  (bvnot
  (bvxor
  (bvxor
  (bvxor
  (bvxor
  (bvxor
  (bvxor
  (bvxor ((_ extract 0 0) res320_0_0x574-empty) ((_ extract 1 1) res320_0_0x574-empty))
  ((_ extract 2 2) res320_0_0x574-empty)) ((_ extract 3 3) res320_0_0x574-empty))
  ((_ extract 4 4) res320_0_0x574-empty)) ((_ extract 5 5) res320_0_0x574-empty))
  ((_ extract 6 6) res320_0_0x574-empty)) ((_ extract 7 7) res320_0_0x574-empty))))

; ------[   ****    DBA instr #6: CF<1> := (0b000000000000000000001101010001100 + (extu ebx<32> 33)){32}    **** ]------
(define-fun
  CF_exit_0_0x574-empty () (_ BitVec 1)
  ((_ extract 32 32)
  (bvadd ((_ zero_extend 1) ebx_entry_0_0x574-empty) (_ bv6796 33))))

; ------[   ****    DBA instr #7: ebx<32> := res32<32>  **** ]------
(define-fun ebx_exit_0_0x574-empty () (_ BitVec 32) res320_0_0x574-empty)

; ------[   ****    DBA instr #8: goto (0x0000057a, 0)  **** ]------

; ------[ ####  Instr #1: @0x57a: call 0x657    #### ]------

; ------[   ****    DBA instr #0: esp<32> := (esp<32> - 4<32>)  **** ]------
(define-fun
  esp_exit_0_0x574-empty () (_ BitVec 32) (bvsub esp_entry_0_0x574-empty (_ bv4 32)))

; ------[   ****    DBA instr #1: @[esp<32>,4] := 0x0000057f    **** ]------
(define-fun mem_case_write_addr0_0_0x574-empty () (_ BitVec 32) esp_exit_0_0x574-empty)
(define-fun
  memory_exit_0_0x574-empty () (Array (_ BitVec 32) (_ BitVec 8))
  (store
  (store
  (store (store memory_entry_0_0x574-empty esp_exit_0_0x574-empty (_ bv127 8))
  (bvadd esp_exit_0_0x574-empty (_ bv1 32)) (_ bv5 8))
  (bvadd esp_exit_0_0x574-empty (_ bv2 32)) (_ bv0 8))
  (bvadd esp_exit_0_0x574-empty (_ bv3 32)) (_ bv0 8)))

; ------[   ****    DBA instr #2: goto (0x00000657, 0) #call with return address @ (0x0000057f, 0)  **** ]------

; ------[ BOA: Exit variables of the formula definitions ]------

(define-fun memory_exit () (Array (_ BitVec 32) (_ BitVec 8)) memory_exit_0_0x574-empty)
(define-fun eax_exit () (_ BitVec 32) eax_entry_0_0x574-empty)
(define-fun ebx_exit () (_ BitVec 32) ebx_exit_0_0x574-empty)
(define-fun ecx_exit () (_ BitVec 32) ecx_entry_0_0x574-empty)
(define-fun edx_exit () (_ BitVec 32) edx_entry_0_0x574-empty)
(define-fun esi_exit () (_ BitVec 32) esi_entry_0_0x574-empty)
(define-fun edi_exit () (_ BitVec 32) edi_entry_0_0x574-empty)
(define-fun ebp_exit () (_ BitVec 32) ebp_entry_0_0x574-empty)
(define-fun esp_exit () (_ BitVec 32) esp_exit_0_0x574-empty)
(define-fun OF_exit () (_ BitVec 1) OF_exit_0_0x574-empty)
(define-fun SF_exit () (_ BitVec 1) SF_exit_0_0x574-empty)
(define-fun ZF_exit () (_ BitVec 1) ZF_exit_0_0x574-empty)
(define-fun PF_exit () (_ BitVec 1) PF_exit_0_0x574-empty)
(define-fun CF_exit () (_ BitVec 1) CF_exit_0_0x574-empty)
(define-fun AF_exit () (_ BitVec 1) AF_exit_0_0x574-empty)
(define-fun DF_exit () (_ BitVec 1) DF_entry_0_0x574-empty)

(push 1)

(define-fun mem_case_symb () (_ BitVec 32) (concat (select memory_exit (bvadd (_ bv1048556 32) (_ bv3 32))
) (concat (select memory_exit (bvadd (_ bv1048556 32) (_ bv2 32))
) (concat (select memory_exit (bvadd (_ bv1048556 32) (_ bv1 32))
) (select memory_exit (_ bv1048556 32))))))

(check-sat)

(get-value (mem_case_symb))

(assert (not (= mem_case_symb (_ bv1407 32))))

(check-sat)

Answer of CVC4:

sat
((mem_case_symb (_ bv1407 32)))
unsat

Answer of Z3:

sat
((mem_case_symb #x0000057f))
unsat

Answer of Boolector:

sat
((mem_case_symb (_ bv0 32))) # The error here!
unsat

I use the last version of master branch.

Thank you for your help!

[aytey]

What's interesting is that if you add:

(assert (= mem_case_symb (_ bv0 32)))

instead of:

(assert (not (= mem_case_symb (_ bv1407 32))))

Then you get:

sat
((mem_case_symb #b00000000000000000000000000000000))
unsat

[mpreiner]

Thanks, I'll have a look!

[sy6sy2]

Thank you! That would be great if you can fix this bug because Boolector is the fastest SMT solver for my use :-P

[sy6sy2]

It works perfectly, thank ou very munch for your quick fix!!