mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity

avoid disequalities from str.at axioms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-04 16:33:12 -07:00
parent af2769dbc0
commit e242257070
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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

4
src/smt/theory_nseq.cpp
View file

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