mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

incorrect axiomatization

Browse source 
Fixes repro in https://github.com/Z3Prover/z3/issues/4866#issuecomment-778706682
This commit is contained in:
Nikolaj Bjorner 2021-02-14 15:29:10 -08:00
parent 45af1bd243
commit eac69c5504
1 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/seq_axioms.cpp
View file

@ -202,9 +202,10 @@ bool seq_axioms::is_extract_suffix(expr* s, expr* i, expr* l) {
} }
/* /*
0 <= l <= len(s) => s = ey & l = len(e) s = ey
len(s) < l => s = e l <= 0 => e = empty
l < 0 => e = empty 0 <= l <= len(s) => len(e) = l
len(s) < l => len(e) = len(s)
*/ */
void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) { void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
TRACE("seq", tout << "prefix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";); TRACE("seq", tout << "prefix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";);
@ -214,13 +215,11 @@ void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
expr_ref zero(a.mk_int(0), m); expr_ref zero(a.mk_int(0), m);
expr_ref y = m_sk.mk_post(s, l); expr_ref y = m_sk.mk_post(s, l);
expr_ref ey = mk_concat(e, y); expr_ref ey = mk_concat(e, y);
literal l_ge_0 = mk_ge(l, 0);
literal l_le_s = mk_le(mk_sub(l, ls), 0); literal l_le_s = mk_le(mk_sub(l, ls), 0);
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey)); add_axiom(mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le)); add_axiom(~mk_le(l, 0), mk_eq_empty(e));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, mk_len(y))); add_axiom(~mk_ge(l, 0), ~l_le_s, mk_eq(le, l));
add_axiom(l_le_s, mk_eq(e, s)); add_axiom(l_le_s, mk_eq(e, s));
add_axiom(l_ge_0, mk_eq_empty(e));
} }
/* /*