From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 16 Jun 2020 16:06:34 +0000 (-0700)
Subject: BV: Fix querying equality status in lazy bit-blaster. (#4618)
X-Git-Tag: cvc5-1.0.0~3211
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f144347482d8ef5ee1462d0ee6fd2e293184b58;p=cvc5.git

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>
---

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)