merge from arrays-clark branch

2 files changed, 8 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;
     }