diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index efe28c30d..f16bb0ff3 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -102,8 +102,13 @@ public: statistics_report sreport(*this); tactic_report report(name(), *in); m_goal = in.get(); - if (!in->proofs_enabled()) - m_simp->reduce(); + try { + if (!in->proofs_enabled()) + m_simp->reduce(); + } + catch (rewriter_exception& ex) { + throw tactic_exception(ex.msg()); + } m_goal->elim_true(); m_goal->elim_redundancies(); m_goal->inc_depth();