From b0247d8201cc7c1076c411618882034a9a5fe49b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Nov 2022 22:20:25 +0700
Subject: [PATCH] add exception handling for rewriter exceptions
---
src/tactic/dependent_expr_state_tactic.h | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
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();