4 files changed, 17 insertions, 9 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 238a9cbf7..7e6f4fd93 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -153,7 +153,10 @@ Var Solver::newVar(bool sign, bool dvar)
 
 bool Solver::addClause_(vec<Lit>& ps)
 {
-    assert(decisionLevel() == 0);
+  if (decisionLevel() > 0) {
+    cancelUntil(0);
+  }
+    
     if (!ok) return false;
 
     // Check if clause is satisfied and remove false/duplicate literals:
@@ -500,6 +503,7 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
     only_bcp = true;
     ccmin_mode = 0; 
     lbool result = search(-1, UIP_FIRST);
+    return result; 
   } else {
     return l_True;
   }
@@ -842,14 +846,7 @@ lbool Solver::solve_()
     model.clear();
     conflict.clear();
 
-    ccmin_mode = 2;
-
-    // reduce the database
-    reduceDB();
-
-    // this is a new search, reset the parameters
-    restart_first = opt_restart_first;
-    restart_inc = opt_restart_inc;
+    ccmin_mode = 0;
     
     if (!ok) return l_False;
 
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 33d1900c9..c7346d7f7 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -148,6 +148,8 @@ public:
     //
 
     void addMarkerLiteral(Var var) {
+      // make sure it wasn't already marked 
+      Assert(marker[var] == 0); 
       marker[var] = 1;
     }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7d4cb7b1c..abe22cb48 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -86,6 +86,10 @@ PropEngine::~PropEngine() {
   delete d_satSolver;
 }
 
+void PropEngine::processAssertionsStart() {
+  d_theoryEngine->preprocessStart();
+}
+
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 91b9a61e6..93c35bbf3 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -170,6 +170,11 @@ public:
   void shutdown() { }
 
   /**
+   * Signal that a new round of assertions is ready so we can notify the theory engine
+   */
+  void processAssertionsStart();
+
+  /**
    * Converts the given formula to CNF and assert the CNF to the SAT solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert