From 5fc2b04dea9e53c7f194a55f36f01381d8da64d1 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 7 Jul 2026 13:01:44 -0700 Subject: [PATCH] Mark quantifier instances that lead to conflicts as relevant (#10064) This patch fixes a corner case where quantifier conflicts can create fresh terms that aren't marked as relevant. I couldn't easily produce a minimal query that this patch turns stable, nor did the patch stabilize the query I have been working on, but I think the example below still illustrates the problem: ``` (set-option :auto_config false) (set-option :type_check true) (set-option :smt.case_split 3) (set-option :smt.mbqi false) (declare-fun R (Int) Bool) (declare-fun S (Int) Bool) (declare-fun dummy (Int) Bool) (assert (or (R 0) (dummy 0))) (assert (forall ((x Int)) (! (and (not (R x)) (not (S x))) :pattern ((R x)) :qid not_r_not_s ))) (assert (forall ((x Int)) (! (S x) :pattern ((S x)) :qid s_true ))) (check-sat) ``` The query is unstable (due to the same interaction between relevancy and triggers in https://github.com/Z3Prover/z3/issues/7444): if the solver assigns `(dummy 0)` first, it returns `unknown`. If the solver assigns `(R 0)` first, we would expect an `unsat`. The current implementation returns `unknown` because `not_r_not_s` leads to a quantifier conflict, which creates `S(x)` without marking it (or any of its ancestors) as relevant. --------- Co-authored-by: Can Cebeci Co-authored-by: Nikolaj Bjorner --- src/smt/smt_context.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8786e73bae..191afdeac6 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1733,8 +1733,16 @@ namespace smt { void internalize_instance(expr * body, proof * pr, unsigned generation) { internalize_assertion(body, pr, generation); - if (relevancy()) + 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); + } m_case_split_queue->internalize_instance_eh(body, generation); + } } unsigned get_unsat_core_size() const {