From 21590144f726f28d83d33b1f31e1651017baa09d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Mar 2026 04:55:58 +0000 Subject: [PATCH] Have theory_nseq use not_contains_axiom instead of unroll_not_contains Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/f01fe213-d914-43de-b21f-de487abb16fb --- src/smt/seq_axioms.h | 1 + src/smt/theory_nseq.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 525f6b3db..477874bc0 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -92,6 +92,7 @@ namespace smt { void add_unit_axiom(expr* n) { m_ax.unit_axiom(n); } void add_length_axiom(expr* n) { m_ax.length_axiom(n); } void unroll_not_contains(expr* n) { m_ax.unroll_not_contains(n); } + void not_contains_axiom(expr* n) { m_ax.not_contains_axiom(n); } literal is_digit(expr* ch) { return mk_literal(m_ax.is_digit(ch)); } expr_ref add_length_limit(expr* s, unsigned k) { return m_ax.length_limit(s, k); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index c73eec720..d09842ab7 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -246,7 +246,7 @@ namespace smt { if (is_true) m_axioms.contains_true_axiom(e); else - m_axioms.unroll_not_contains(e); + m_axioms.not_contains_axiom(e); } else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { // axioms added via relevant_eh → dequeue_axiom