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
335 stars 62 forks source link

Solution soundness bug on BV formulas (--quant-ms) #145

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic BV)
(declare-const bv_47-0 (_ BitVec 47))
(assert (forall ((q20 (_ BitVec 10)) (q21 (_ BitVec 10)) (q22 (_ BitVec 10)) (q23 (_ BitVec 47)) (q24 (_ BitVec 47)) (q25 (_ BitVec 9))) (=> (= q24 q23 bv_47-0 bv_47-0 bv_47-0) (
bvult q25 (_ bv268 9)))))
(check-sat)

boolector 6fce0ac35ec yields sat, but both cvc4 and z3 return unsat

This formula seems trivially unsat because q25 only appears once in the body.

Another one

(set-logic BV)
(declare-fun _substvar_10_ () (_ BitVec 8))
(assert (forall ((q8 (_ BitVec 8)) (q9 (_ BitVec 8)) (q10 (_ BitVec 7))) (=> (= q9 _substvar_10_ q9 q8 q8) (= (_ bv0 7) q10 (_ bv0 7)))))
(check-sat)
rainoftime commented 4 years ago

@aniemetz This issue seems to be related to miniscoping. With the option --quant-ms=0, boolector can return unsat. Could you have a check?

mpreiner commented 1 month ago

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.