diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 22:57:57 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 22:57:57 -0400 |
| commit | 744792614fdd8da94eecd5b0cad7c3cb19b3d91c (patch) | |
| tree | beaf843bb917f99bc9c1742eafe41be6aab71a08 /src/prop/minisat/core | |
| parent | ecc45b22ce41b6cde8e42a4c1baca4a0cd7c3ea3 (diff) | |
Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report.
Diffstat (limited to 'src/prop/minisat/core')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 2 |
2 files changed, 4 insertions, 1 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: // |