From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 9 Nov 2020 16:46:23 +0000 (+0100)
Subject: Properly clear interrupt for solve() as well. (#5403)
X-Git-Tag: cvc5-1.0.0~2626
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b894cc0201783a40cd92e9bffe7257d44f8f4e4;p=cvc5.git

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 40fdeee55..fa31eb41c 100644
--- 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 {