mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

use sk.mk_seq_eq to avoid disequality propagations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-29 15:45:42 -07:00
parent 09cde1f80c
commit 6d31bdcc21
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_axioms.cpp
View file

@ -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);