From 5f144347482d8ef5ee1462d0ee6fd2e293184b58 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 16 Jun 2020 09:06:34 -0700 Subject: [PATCH] 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: --- src/theory/bv/bitblast/lazy_bitblaster.cpp | 8 +++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/bv/issue-4076.smt2 | 15 +++++++++++++++ 3 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/bv/issue-4076.smt2 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; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f225c2ed6..93d6a3ef8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -361,6 +361,7 @@ set(regress_0_tests regress0/bv/fuzz41.smtv1.smt2 regress0/bv/issue3621.smt2 regress0/bv/issue-4075.smt2 + regress0/bv/issue-4076.smt2 regress0/bv/issue-4130.smt2 regress0/bv/int_to_bv_err_on_demand_1.smt2 regress0/bv/mul-neg-unsat.smt2 diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 new file mode 100644 index 000000000..3a80dc5f0 --- /dev/null +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(set-option :produce-models true) +(declare-fun a ((_ BitVec 2)) Int) +(declare-fun b (Int) (_ BitVec 2)) +(declare-const c Int) +(declare-const d Int) +(assert (= (a #b01) 1)) +(assert(= 0 (a (bvlshr (b c) (b d))))) +(push) +(check-sat) +(pop) +(check-sat) -- 2.30.2