From 6d31bdcc2110720bf299f13c18eb55c6ab7a0d0c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Mar 2026 15:45:42 -0700 Subject: [PATCH] use sk.mk_seq_eq to avoid disequality propagations Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 40e28c42a..5951d953d 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1420,8 +1420,8 @@ namespace seq { expr_ref vp_len(mk_len(vp), m); expr_ref wau(mk_concat(w, seq.str.mk_unit(a), up), m); expr_ref wbv(mk_concat(w, seq.str.mk_unit(b), vp), m); - expr_ref u_eq(mk_eq(u, wau), m); - expr_ref v_eq(mk_eq(v, wbv), m); + expr_ref u_eq(mk_seq_eq(u, wau), m); + expr_ref v_eq(mk_seq_eq(v, wbv), m); if (m_mark_no_diseq) { m_mark_no_diseq(wau); m_mark_no_diseq(wbv);