fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.

3 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index a9c6d2676..60a98e6e5 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -173,6 +173,10 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
  * 
  */
  
+bool Bitblaster::propagate() {
+  return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
+}
+
 bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
   TNode atom; 
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index b27415e0b..16c50be22 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -129,6 +129,7 @@ public:
   Bitblaster(context::Context* c, bv::TheoryBV* bv); 
   ~Bitblaster();
   bool assertToSat(TNode node, bool propagate = true);
+  bool propagate();
   bool solve(bool quick_solve = false);
   void getConflict(std::vector<TNode>& conflict); 
   void explain(TNode atom, std::vector<TNode>& explanation);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 334a704e9..a5a9b9a7e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -93,6 +93,17 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     }
   }
 
+  // We need to ensure we are fully propagated, so propagate now
+  if (d_useSatPropagation) {
+    bool ok = d_bitblaster->propagate();
+    if (!ok) {
+      std::vector<TNode> conflictAtoms;
+      d_bitblaster->getConflict(conflictAtoms);
+      d_bv->setConflict(mkConjunction(conflictAtoms));
+      return false;
+    }
+  }
+
   // solving
   if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
     Assert(!d_bv->inConflict());