projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b07543b) | patch
Fix handling of `LogicException` during solving (#8000)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 9 Feb 2022 18:42:37 +0000 (10:42 -0800)
committerGitHub <noreply@github.com>
Wed, 9 Feb 2022 18:42:37 +0000 (18:42 +0000)
commit4303c4ee5a9234ee03904b16c519a0ce6fcd80d1
treee8f18a52f44d1c97ebfd43366a9ce1695746d0bbtree
parentb07543b20ab2e263035b75aca0b92636f5a9cdcbcommit | diff
Fix handling of `LogicException` during solving (#8000)

Fixes #7974. This commit fixes our handling of LogicExceptions during solving. Instead of leaving MiniSat in a bad state, it catches the exception, resets the decision trail, prints the error message, and then returns unknown.
src/smt/smt_solver.cpp diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue7974-incomplete-neg-member.smt2 [new file with mode: 0644] blob