get-value of bool returns bit-vector value

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

Closed daniel-larraz closed 3 years ago

daniel-larraz commented 3 years ago

Consider this simple SMTLIB script:

(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun b () Bool)
(check-sat)
(get-value (b))

boolector outputs:

sat
((b #b0))

Expected output:

sat
((b false))

aytey commented 3 years ago

If you're able to build from source, please take a look at https://github.com/Boolector/boolector/pull/137