diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-09 17:46:23 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-09 10:46:23 -0600 |
| commit | 4b894cc0201783a40cd92e9bffe7257d44f8f4e4 (patch) | |
| tree | 0bde7883f7fd7c6e88f041ff175cb14601ae6341 /src/prop | |
| parent | 6cb2e5743bd886115124256c2a3ad689a5b822a2 (diff) | |
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.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/minisat.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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 { |