From 09cde1f80c2f281260d88d1561c2d9daaa3c1a74 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 29 Mar 2026 15:44:18 -0700 Subject: [PATCH] Port propagate_eq from theory_seq for sk().is_eq in theory_nseq (#9165) Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7c0a330f-3f9f-4c5d-99f2-47fad013538f Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/theory_nseq.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 0a7fa3e22..386236992 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -278,7 +278,17 @@ namespace smt { // axioms added via relevant_eh → dequeue_axiom } else if (m_axioms.sk().is_eq(e, a, b) && is_true) { - // TODO: port propagate_eq from theory_seq. + enode* n1 = ensure_enode(a); + enode* n2 = ensure_enode(b); + if (n1->get_root() != n2->get_root()) { + literal lit(v, false); + ctx.mark_as_relevant(n1); + ctx.mark_as_relevant(n2); + justification* js = ctx.mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx, 1, &lit, 0, nullptr, n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(js)); + } } else if (m_seq.is_skolem(e) || m_seq.str.is_nth_i(e) ||