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

Possibly incorrect result for a quantified formula #39

Closed martinjonas closed 5 years ago

martinjonas commented 5 years ago

I have a quantified formula (in the attachment formula.zip) for which Boolector 3.0.1-pre returns sat. I think that this result might be incorrect, as Z3 (4.8.5), CVC4 (1.6), and Q3B (1.0) all return unsat.

I am using the following versions of Boolector and Lingeling:

[btor>main] Boolector Version 3.0.1-pre master-319e4e969523238bce24061b706629cc9fa58cb4
[btor>main]  -std=gnu99 -W -Wall -Wextra -Wredundant-decls -O3
[btor>main] released 2019-03-13T14:16:35
[btor>main] compiled 2019-03-13T14:16:35
[btor>main] GNU 8.2.1

[lingeling] Lingeling
[lingeling] 
[lingeling] Version bcj 78ebb8672540bde0a335aea946bbf32515157d5a

If it helps with the debugging, the formula is a result of applying some rewriting rules to the formula 2017-Preiner-psyco/090.smt2 from BV category of SMT-LIB.

Thank you for looking into it.

mpreiner commented 5 years ago

Hi Martin,

Thanks for the bug report. We'll have a look!