Properly clear interrupt for solve() as well. (#5403)

The minisat solver stores whether it has been interrupted in asynch_interrupt and expects it to be reset before another call to solve(). MinisatSatSolver::solve() failed to do this, leading to incorrect unknown results as observed in CVC4/cvc4-projects#106. The alternative MinisatSatSolver::solve(unsigned long& resource) already did the correct thing.
Fixes CVC4/cvc4-projects#106.

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 40fdeee55db1a077f47bc0e4533322028e20cf4b..fa31eb41c7382641552eb6823ab8d2226d983ddd 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -182,7 +182,9 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) {
 SatValue MinisatSatSolver::solve() {
   setupOptions();
   d_minisat->budgetOff();
-  return toSatLiteralValue(d_minisat->solve());
+  SatValue result = toSatLiteralValue(d_minisat->solve());
+  d_minisat->clearInterrupt();
+  return result;
 }
 
 bool MinisatSatSolver::ok() const {