projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5f880a) | patch
BV: Fix querying equality status in lazy bit-blaster. (#4618)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 16 Jun 2020 16:06:34 +0000 (09:06 -0700)
committerGitHub <noreply@github.com>
Tue, 16 Jun 2020 16:06:34 +0000 (09:06 -0700)
commit5f144347482d8ef5ee1462d0ee6fd2e293184b58
treedde5801f3b2241618c0b2033bea207961fb7f4aatree
parente5f880a7bb603734a737e026ba64c035b0517468commit | diff
BV: Fix querying equality status in lazy bit-blaster. (#4618)

Fixes #4076.

In the lazy bit-blaster, when querying the equality status, if the SAT
solver has a full model, it is queried for the model values of the
operands of the equality. However, the check if the bit-blaster has a
full model did not consider the case where no assertions have yet been
added, which leads to querying values of bits that are still unassigned
in the SAT solver.

Co-authored-by: <mathias.preiner@gmail.com>
src/theory/bv/bitblast/lazy_bitblaster.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/issue-4076.smt2 [new file with mode: 0644] blob