Fix model of Boolean vars with eager bit-blaster (#2998)
authorAndres Noetzli <noetzli@stanford.edu>
Wed, 15 May 2019 17:38:04 +0000 (17:38 +0000)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 15 May 2019 17:38:04 +0000 (10:38 -0700)
commitf2d113cf3cbb0f4966a7c909b9cd2c14aa753eb1
treedf20d8af54d7d7d33d5ab41e7f2401c51a10d2dc
parentbc550fa115401256616042ccb7a559ec252e319b
Fix model of Boolean vars with eager bit-blaster (#2998)

When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.
src/theory/bv/bitblast/eager_bitblaster.cpp
test/regress/CMakeLists.txt
test/regress/regress0/bv/bool-model.smt2 [new file with mode: 0644]