search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Refutation soundness bug on bit-vector formulas #159

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula, boolector 6fce0ac yields unsat, but both cvc4 and z3 give sat

(set-logic BV)
(declare-fun _substvar_245_ () Bool)
(assert (not (forall ((q21 Bool) (q22 (_ BitVec 4)) (q23 (_ BitVec 8))) (not (= q21 true true (not (forall ((q2 (_ BitVec 4)) (q3 (_ BitVec 4)) (q4 Bool) (q5 (_ BitVec 4)) (q6 (_ BitVec 4)) (q7 (_ BitVec 4))) q4)) _substvar_245_ q21 q21 q21 true q21)))))
(check-sat)
rainoftime commented 3 years ago

Another formula

(set-logic BV)
(declare-fun _substvar_2530_ () Bool)
(declare-const v8 Bool)
(assert (or (forall ((q110 (_ BitVec 7))) (not (exists ((q81 Bool) (q82 (_ BitVec 8))) q81))) (not (exists ((q83 (_ BitVec 7)) (q84 (_ BitVec 8))) (forall ((q67 (_ BitVec 8)) (q68 Bool) (q69 (_ BitVec 7)) (q70 (_ BitVec 7)) (q71 Bool)) (not (exists ((q56 (_ BitVec 4)) (q57 (_ BitVec 8)) (q58 (_ BitVec 4))) v8)))))))
(assert (or (not (forall ((q91 (_ BitVec 7)) (q92 (_ BitVec 4)) (q93 (_ BitVec 4))) (=> (distinct q91 (_ bv81 7)) _substvar_2530_))) (not (exists ((q8 Bool) (q9 Bool)) v8))))
(check-sat)
vedadux commented 2 years ago

I took the time to look at this, and have found a much simpler example where the exact same problem happens:

(assert (exists ((q Bool)) (= true (not (forall ((p Bool)) p)) q)))
(check-sat)

Here, the forall block evaluates to false, meaning that the exists block is satisfiable with q = true. The solver Z3 gives the correct answer sat, while Boolector gives unsat. This is all with Boolector version 3.2.2, commit 0783aa84