projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6cb2e57) | patch
Properly clear interrupt for solve() as well. (#5403)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 9 Nov 2020 16:46:23 +0000 (17:46 +0100)
committerGitHub <noreply@github.com>
Mon, 9 Nov 2020 16:46:23 +0000 (10:46 -0600)
commit4b894cc0201783a40cd92e9bffe7257d44f8f4e4
tree0bde7883f7fd7c6e88f041ff175cb14601ae6341tree
parent6cb2e5743bd886115124256c2a3ad689a5b822a2commit | 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.
src/prop/minisat/minisat.cpp diff | blob | history