From 4b894cc0201783a40cd92e9bffe7257d44f8f4e4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 9 Nov 2020 17:46:23 +0100 Subject: [PATCH] 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. --- src/prop/minisat/minisat.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 { -- 2.30.2