From 661bb130397b8d26fb558f17a1ea0cbb8eec38f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jul 2026 11:29:20 -0700 Subject: [PATCH] change relevancy marking to top-level on inconsistent states Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7938c7074..9664dd73e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1779,15 +1779,16 @@ namespace smt { void internalize_proxies(expr_ref_vector const& asms, vector>& asm2proxy); void internalize_instance(expr * body, proof * pr, unsigned generation) { + if (inconsistent()) + return; internalize_assertion(body, pr, generation); if (relevancy()) { // if the instantiation creates a conflict, we backtrack immediately. // to retain the conflict clause being relevant we mark it here. // if the instantiation does not create a conflict, default relevancy propagation applies. - if (inconsistent() && is_app(body)) { - for (auto arg : *to_app(body)) - mark_as_relevant(arg); - } + if (inconsistent()) + mark_as_relevant(body); + m_case_split_queue->internalize_instance_eh(body, generation); } }