diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 14:23:48 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 14:23:48 +0000 |
| commit | bc87b6c6b30dbc2ec0336b2fda0a71c77e662267 (patch) | |
| tree | c88fd183dc597e0044522835644462e9e3123ba0 | |
| parent | 4721e72430a69a0082f0f3313d8fc452f83579dc (diff) | |
changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in solve
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 |
1 files changed, 4 insertions, 1 deletions
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++; |