From 828e7a4ed6dd5d952f4ff49d24079411ab0d1abb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2026 11:46:56 -0700 Subject: [PATCH] Update smt_context.h --- src/smt/smt_context.h | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9b79fbfe33..191afdeac6 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1734,14 +1734,12 @@ namespace smt { void internalize_instance(expr * body, proof * pr, unsigned generation) { internalize_assertion(body, pr, generation); if (relevancy()) { - if (inconsistent()) { - app * a = to_app(body); - SASSERT(a->get_decl_kind() == OP_OR); - SASSERT(to_app(a->get_arg(0))->get_decl_kind() == OP_NOT); - SASSERT(is_quantifier(to_app(a->get_arg(0))->get_arg(0))); - for (unsigned i = 1; i < a->get_num_args(); ++i) { - mark_as_relevant(a->get_arg(i)); - } + // 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); } m_case_split_queue->internalize_instance_eh(body, generation); }