summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-04-25 18:43:12 -0400
committerlianah <lianahady@gmail.com>2013-04-30 15:54:24 -0400
commit94dc66d4cb4061a80bffe1ec72d2ab98e44dd626 (patch)
tree0daa9a883d4be5ccf8e863d6305814ef6f12b564 /src/prop
parent7701ac73a62a466eaf4e55c1c2dc238c7110b02f (diff)
added bvule, bvsle operator elimination rulesl; added bvurem lemma generation
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 6bbe4bb3e..ab25fa6cb 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -106,6 +106,7 @@ SatValue BVMinisatSatSolver::solve(){
SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+ ++d_statistics.d_statCallsToSolve;
if(resource == 0) {
d_minisat->budgetOff();
} else {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback