mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

add exception handling for rewriter exceptions

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-24 22:20:25 +07:00
parent 1815812889
commit b0247d8201
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/dependent_expr_state_tactic.h
View file

@ -102,8 +102,13 @@ public:
statistics_report sreport(*this); statistics_report sreport(*this);
tactic_report report(name(), *in); tactic_report report(name(), *in);
m_goal = in.get(); m_goal = in.get();
try {
if (!in->proofs_enabled()) if (!in->proofs_enabled())
m_simp->reduce(); m_simp->reduce();
}
catch (rewriter_exception& ex) {
throw tactic_exception(ex.msg());
}
m_goal->elim_true(); m_goal->elim_true();
m_goal->elim_redundancies(); m_goal->elim_redundancies();
m_goal->inc_depth(); m_goal->inc_depth();