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

[Bug] Wrong result for `(= false false true)` #44

Closed pkreutzer closed 5 years ago

pkreutzer commented 5 years ago

Hi there,

the current version of Boolector reports sat for the following SMT-LIB v2 script, but the correct result is unsat (cf. p. 36 in version 2.6 of the language standard):

(set-logic QF_UFBV)
(assert (= false false true))
(check-sat)

It seems that Boolector handles = as left-assoc, even though it is defined to be chainable. Both z3 and CVC4 report the correct result.

mpreiner commented 5 years ago

Thanks for reporting! Is fixed on master.