diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-16 09:06:34 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-16 09:06:34 -0700 |
| commit | 5f144347482d8ef5ee1462d0ee6fd2e293184b58 (patch) | |
| tree | dde5801f3b2241618c0b2033bea207961fb7f4aa /src/theory/bv | |
| parent | e5f880a7bb603734a737e026ba64c035b0517468 (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>
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 463ffae79..163d2e78a 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -440,11 +440,13 @@ void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r) EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { int numAssertions = d_bv->numAssertions(); + bool has_full_model = + numAssertions != 0 && d_fullModelAssertionLevel.get() == numAssertions; + Debug("bv-equality-status") << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n"; Debug("bv-equality-status") - << "BVSatSolver has full model? " - << (d_fullModelAssertionLevel.get() == numAssertions) << "\n"; + << "BVSatSolver has full model? " << has_full_model << "\n"; // First check if it trivially rewrites to false/true Node a_eq_b = @@ -453,7 +455,7 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - if (d_fullModelAssertionLevel.get() != numAssertions) + if (!has_full_model) { return theory::EQUALITY_UNKNOWN; } |