7 files changed, 23 insertions, 5 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();
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 610023b70..b0d710d66 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -106,7 +106,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
 
     // Statistics: (formerly in 'SolverStats')
     //
-  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
+  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), resources_consumed(0)
   , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
 
   , ok                 (true)
@@ -1588,6 +1588,9 @@ CRef Solver::updateLemmas() {
 
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
+  // Avoid adding lemmas indefinitely without resource-out
+  spendResource();
+
   CRef conflict = CRef_Undef;
 
   // Decision level to backtrack to
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 30d72ac75..7831f211b 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -215,6 +215,7 @@ public:
     void    budgetOff();
     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
     void    clearInterrupt();     // Clear interrupt indicator flag.
+    void    spendResource();
 
     // Memory managment:
     //
@@ -252,7 +253,7 @@ public:
 
     // Statistics: (read-only member variable)
     //
-    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, resources_consumed;
     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 
 protected:
@@ -526,8 +527,9 @@ inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 inline bool     Solver::withinBudget() const {
     return !asynch_interrupt &&
-           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
+           (conflict_budget    < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+inline void     Solver::spendResource() { ++resources_consumed; }
 
 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e4956ecc8..4a192d0d2 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -168,10 +168,10 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) {
     d_minisat->setConfBudget(resource);
   }
   Minisat::vec<Minisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
+  unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
   SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
   d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
+  resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
   Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
   return result;
 }
@@ -182,6 +182,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
+void MinisatSatSolver::spendResource() {
+  d_minisat->spendResource();
+}
 
 void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index a919bbcc4..b37371d98 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -62,6 +62,7 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
+  void spendResource();
   void interrupt();
 
   SatValue value(SatLiteral l);
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 929b867c9..8e7e53474 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -61,6 +61,9 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
+  /** Instruct the solver that it should bump its consumed resource count. */
+  virtual void spendResource() = 0;
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;