Better support for resource-limiting when there aren't any actual conflicts.

2 files changed, 6 insertions, 0 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 7322cd0fa..2121d7366 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -97,6 +97,10 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 }
 
+void BVMinisatSatSolver::spendResource(){
+  // do nothing for the BV solver
+}
+
 void BVMinisatSatSolver::interrupt(){
   d_minisat->interrupt();
 }
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index f9d0fbd6a..0101c5d62 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -87,6 +87,8 @@ public:
 
   void markUnremovable(SatLiteral lit);
 
+  void spendResource();
+
   void interrupt();
   
   SatValue solve();