From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 4 Apr 2012 14:23:48 +0000 (+0000)
Subject: changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in... 
X-Git-Tag: cvc5-1.0.0~8241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc87b6c6b30dbc2ec0336b2fda0a71c77e662267;p=cvc5.git

changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in solve
---

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 7361a6f6e..c5a0a3ce5 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -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++;