When printing a value in 'smt2' format, ensure that Bools are presented correctly

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

Closed aytey closed 4 years ago

aytey commented 4 years ago

Quick attempt to fix #136

It seems that this was "half done" in https://github.com/Boolector/boolector/commit/55febfd8d61b14acb19538254886435377fc0d59, so I've just tried to make sure the logic is consistent for the example in #136.

I'm not sure why the aforementioned commit formats things like:

((b Bool false))

though (this branch does not do that).

Signed-off-by: Andrew V. Jones andrew.jones@vector.com