From 3d1ad64367948039f67f653e34f19359e3c9c496 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.stanford.edu>
Date: Tue, 28 Mar 2017 18:29:48 -0700
Subject: [PATCH] Fix for bug 733

---
 src/theory/bv/bitblaster_template.h  |  5 ++++-
 src/theory/bv/lazy_bitblaster.cpp    | 10 ++++++----
 src/theory/theory.h                  |  5 +++++
 test/regress/regress0/bv/Makefile.am |  1 +
 test/regress/regress0/bv/bug733.smt2 |  8 ++++++++
 5 files changed, 24 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress0/bv/bug733.smt2

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index aa5ae9c16..8a7ccf8c6 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -161,7 +161,10 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
 
-  context::CDO<bool> d_satSolverFullModel;
+  // The size of the fact queue when we most recently called solve() in the
+  // bit-vector SAT solver. This is the level at which we should have
+  // a full model in the bv SAT solver.
+  context::CDO<int> d_fullModelAssertionLevel;
 
   void addAtom(TNode atom);
   bool hasValue(TNode a);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 1477f183e..e89cacb40 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -45,7 +45,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
   , d_bbAtoms()
   , d_abstraction(NULL)
   , d_emptyNotify(emptyNotify)
-  , d_satSolverFullModel(c, false)
+  , d_fullModelAssertionLevel(c, 0)
   , d_name(name)
   , d_statistics(name) {
 
@@ -290,7 +290,7 @@ bool TLazyBitblaster::solve() {
     }
   }
   Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
-  d_satSolverFullModel.set(true);
+  d_fullModelAssertionLevel.set(d_bv->numAssertions());
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
@@ -393,8 +393,9 @@ void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) {
 
 
 EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
+  int numAssertions = d_bv->numAssertions();
   Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n";
-  Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n";
+  Debug("bv-equality-status")<< "BVSatSolver has full model? " << (d_fullModelAssertionLevel.get() == numAssertions) <<"\n";
 
   // First check if it trivially rewrites to false/true
   Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b));
@@ -402,8 +403,9 @@ 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_satSolverFullModel.get())
+  if (d_fullModelAssertionLevel.get() != numAssertions) {
     return theory::EQUALITY_UNKNOWN;
+  }
 
   // Check if cache is valid (invalidated in check and pops)
   if (d_bv->d_invalidateModelCache.get()) {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index d50d6b3f9..445d184e4 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -734,6 +734,11 @@ public:
     return !d_facts.empty(); 
   }
 
+  /** Return total number of facts asserted to this theory */
+  size_t numAssertions() {
+    return d_facts.size();
+  }
+  
   typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
 
   /**
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 0f41c22ec..da537bdae 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -117,6 +117,7 @@ BUG_TESTS = \
 	bug260a.smt \
 	bug260b.smt \
 	bug440.smt \
+	bug733.smt2 \
 	bug734.smt2 \
 	bug_extract_mult_leading_bit.smt2
 
diff --git a/test/regress/regress0/bv/bug733.smt2 b/test/regress/regress0/bv/bug733.smt2
new file mode 100644
index 000000000..02ef85d82
--- /dev/null
+++ b/test/regress/regress0/bv/bug733.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(check-sat)
-- 
2.30.2