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

Incorrect result for a quantified formula #54

Closed martinjonas closed 4 years ago

martinjonas commented 5 years ago

I have a quantified formula (in the attachment formula.zip) for which the latest version of Boolector returns sat. I think that this result is 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-aa5b2972e8ba9a8c2e0788d3f9c683e7fe87440a
[btor>main]  -std=gnu99 -W -Wall -Wextra -Wredundant-decls -O3
[btor>main] released 2019-06-24T10:29:35
[btor>main] compiled 2019-06-24T10:29:35
[btor>main] GNU 9.1.0
[lingeling] Version bcj 78ebb8672540bde0a335aea946bbf32515157d5a
[lingeling] released Thu May 17 11:57:41 CEST 2018
[lingeling] compiled Fri Jun 21 10:53:36 CEST 2019
[lingeling] gcc (GCC) 9.1.0

Curiously, if I run Boolector only on the second conjunct of this formula, the result is unsat.

Thank you for investigating.

mpreiner commented 5 years ago

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