projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
4721e72
)
changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in...
author
Liana Hadarean
<lianahady@gmail.com>
Wed, 4 Apr 2012 14:23:48 +0000
(14:23 +0000)
committer
Liana Hadarean
<lianahady@gmail.com>
Wed, 4 Apr 2012 14:23:48 +0000
(14:23 +0000)
src/prop/bvminisat/core/Solver.cc
patch
|
blob
|
history
diff --git
a/src/prop/bvminisat/core/Solver.cc
b/src/prop/bvminisat/core/Solver.cc
index 7361a6f6eab3d1a87eaf2c018ad58fd08b13ed27..c5a0a3ce5215962281eeac615391ad77eb93da59 100644
(file)
--- 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++;