changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in...
authorLiana Hadarean <lianahady@gmail.com>
Wed, 4 Apr 2012 14:23:48 +0000 (14:23 +0000)
committerLiana Hadarean <lianahady@gmail.com>
Wed, 4 Apr 2012 14:23:48 +0000 (14:23 +0000)
src/prop/bvminisat/core/Solver.cc

index 7361a6f6eab3d1a87eaf2c018ad58fd08b13ed27..c5a0a3ce5215962281eeac615391ad77eb93da59 100644 (file)
@@ -498,7 +498,8 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
   // run the propagation
   if (propagate) {
     only_bcp = true;
-    return search(-1, UIP_FIRST);
+    ccmin_mode = 0; 
+    lbool result = search(-1, UIP_FIRST);
   } else {
     return l_True;
   }
@@ -841,6 +842,8 @@ lbool Solver::solve_()
     model.clear();
     conflict.clear();
 
+    ccmin_mode = 2;
+    
     if (!ok) return l_False;
 
     solves++;