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

SAT/UNSAT return code when dumping a formula simplified to true/false #168

Closed symphorien closed 3 years ago

symphorien commented 3 years ago

Usecase: when using boolector in AIGER dump mode, if the formula is proved unsat, boolector seems to not output anything instead of outputing an unsat AIGER formula. It's apparenlty impossible to distinguish "formula was sat" and "formula was unsat" in the current state of things. Solution: This PR makes use of the boolector exit codes to convey this information.

Tests pass when this patch is applied on top of 3.2.1 (one test does not pass on current master, and it still does not pass with this patch applied obviously).

mpreiner commented 3 years ago

@symphorien Thanks for pointing this out. I went ahead and fixed the issue in the AIGER printer (https://github.com/Boolector/boolector/commit/ad16fd1b47fdce57cc55ca5f1b2f4f7c95b2f631). Boolector now prints the correct AIGER file.

symphorien commented 3 years ago

Thanks, it's much better!