From e242257070d943d17101037d27bffcbee4aa5eed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 May 2026 16:33:12 -0700 Subject: [PATCH] avoid disequalities from str.at axioms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 4 ++-- src/smt/theory_nseq.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 664d5d352..e3ee8b436 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -638,8 +638,8 @@ namespace seq { add_clause(~i_ge_0, i_ge_len_s, mk_eq(i, len_x)); } - add_clause(i_ge_0, mk_eq(e, emp)); - add_clause(~i_ge_len_s, mk_eq(e, emp)); + add_clause(i_ge_0, mk_seq_eq(e, emp)); + add_clause(~i_ge_len_s, mk_seq_eq(e, emp)); add_clause(~i_ge_0, i_ge_len_s, mk_eq(one, len_e)); add_clause(mk_le(len_e, 1)); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 584162100..3bbbd6d2d 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -343,9 +343,9 @@ namespace smt { else if (m_axioms.sk().is_eq(e, a, b) && is_true) { enode* n1 = ensure_enode(a); enode* n2 = ensure_enode(b); - auto v1 = mk_var(n1); - auto v2 = mk_var(n2); if (n1->get_root() != n2->get_root()) { + auto v1 = mk_var(n1); + auto v2 = mk_var(n2); literal lit(v, false); ctx.mark_as_relevant(n1); ctx.mark_as_relevant(n2);