mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 06:28:18 +00:00
Code Activity

Update seq_axioms.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-05 18:13:35 -07:00
parent 2999517d51
commit 979fd5c637
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1309,7 +1309,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(len_y, offs)));
add_clause(~offs_ge_0, ~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) ||