mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 15:37:58 +00:00
Code Activity

fix unsound len(substr) axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-26 15:38:25 -07:00
parent 1f8b08108c
commit ad2934f8cf
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

@ -1243,7 +1243,7 @@ namespace seq {
else if (seq.str.is_extract(x, y, offs, l)) {
// len(extract(y, o, l)) = l if len(y) >= o + l, o >= 0, l >= 0
// len(extract(y, o, l)) = 0 if o < 0 or l <= 0 or len(y) < o
// len(extract(y, o, l)) = o + l - len(y) if o <= len(y) < o + l
// len(extract(y, o, l)) = len(y) - o if o <= len(y) < o + l
expr_ref len_y(mk_len(y), m);
expr_ref z(a.mk_int(0), m);
expr_ref y_ge_l = mk_ge(a.mk_sub(len_y, a.mk_add(offs, l)), 0);
@ -1255,7 +1255,7 @@ namespace seq {
add_clause(offs_ge_0, mk_eq(n, z));
add_clause(l_ge_0, mk_eq(n, z));
add_clause(y_ge_o, mk_eq(n, z));
add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(a.mk_add(offs, l), len_y)));
add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(len_y, offs)));
}
else if (seq.str.is_unit(x) ||
seq.str.is_empty(x) ||