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 /examples/hashsmt/sha1_collision.cpp | |
| 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 'examples/hashsmt/sha1_collision.cpp')
0 files changed, 0 insertions, 0 deletions