From c03cda14f1d23f912dc6fab06822bcc69bc1ceef Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 7 Jul 2026 11:07:09 -0700 Subject: [PATCH] Mark quantifier instances that lead to conflicts as relevant --- src/smt/smt_context.h | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8786e73bae..9b79fbfe33 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1733,8 +1733,18 @@ namespace smt { void internalize_instance(expr * body, proof * pr, unsigned generation) { internalize_assertion(body, pr, generation); - if (relevancy()) + 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)); + } + } m_case_split_queue->internalize_instance_eh(body, generation); + } } unsigned get_unsat_core_size() const {