Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report.

4 files changed, 7 insertions, 3 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5403b992e..e5e28bb0b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -815,7 +815,8 @@ CRef Solver::propagate(TheoryCheckType type)
     if (type == CHECK_FINAL) {
       // Do the theory check
       theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
-      // Pick up the theory propagated literals (there could be some, if new lemmas are added)
+      // Pick up the theory propagated literals (there could be some,
+      // if new lemmas are added)
       propagateTheory();
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 2d70cfeef..6d9fd538f 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -423,7 +423,9 @@ protected:
     int      intro_level      (Var x) const; // User level at which this variable was created
     int      trail_index      (Var x) const; // Index in the trail
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
+public:
     bool     withinBudget     ()      const;
+protected:
 
     // Static helpers:
     //
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index b50c1c09f..99341455c 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -182,8 +182,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
-void MinisatSatSolver::spendResource() {
+bool MinisatSatSolver::spendResource() {
   d_minisat->spendResource();
+  return !d_minisat->withinBudget();
 }
 
 void MinisatSatSolver::interrupt() {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 3992f1adb..3d3cea356 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -62,7 +62,7 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
-  void spendResource();
+  bool spendResource();
   void interrupt();
 
   SatValue value(SatLiteral l);