From cc94930e00452531d005cd8c16c2a088b85c676e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Dec 2025 11:30:22 -0800 Subject: [PATCH] fix #8105 --- src/tactic/core/ctx_simplify_tactic.cpp | 4 ++++ src/tactic/goal.h | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index f1f2f2162..8752c4dfc 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -566,6 +566,8 @@ struct ctx_simplify_tactic::imp { } void operator()(goal & g) { + if (g.inconsistent()) + return; m_occs.reset(); m_occs(g); m_num_steps = 0; @@ -578,6 +580,8 @@ struct ctx_simplify_tactic::imp { proof_ref new_pr(m.mk_rewrite(t, r), m); new_pr = m.mk_modus_ponens(pr, new_pr); g.update(idx++, r, new_pr, dep); + if (g.inconsistent()) + break; } } else { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index b93d655c0..aabd1024b 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -122,7 +122,9 @@ public: expr * form(unsigned i) const { return inconsistent() ? m().mk_false() : m().get(m_forms, i); } proof * pr(unsigned i) const { return m().size(m_proofs) > i ? static_cast(m().get(m_proofs, i)) : nullptr; } - expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : nullptr; } + expr_dependency *dep(unsigned i) const { + return unsat_core_enabled() && i < m().size(m_dependencies) ? m().get(m_dependencies, i) : nullptr; + } void update(unsigned i, expr * f, proof * pr = nullptr, expr_dependency * dep = nullptr);