Fix for bug 733

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index aa5ae9c16279410e350bb79a0134ebaaa2e82642..8a7ccf8c659b3bae2bbf35d4b9f4d03f9baca704 100644 (file)
--- 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 1477f183e4758748a0c9e88cf87d27997e25a34e..e89cacb40780cc35999bb145c304307071322bb4 100644 (file)
--- 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 d50d6b3f976889dc53a922ca9f090be52fb97e48..445d184e4e5a22126ac19825b28457a9b5a583cf 100644 (file)
--- 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 0f41c22ec890d3af3d69b504a12bdf9a9dc97335..da537bdae0b52aa53788231a66b3871472e7e85c 100644 (file)
--- 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 (file)
index 0000000..02ef85d
--- /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)