mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

missing length constraint for at fixes #2852

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-12 17:22:59 -08:00
parent 74f0665a0b
commit e8cfbb41d3
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_seq.cpp
View file

@ -5480,6 +5480,7 @@ void theory_seq::add_at_axiom(expr* e) {
expr_ref len_s = mk_len(s); expr_ref len_s = mk_len(s);
literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero)); literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero)); literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
expr_ref len_e = mk_len(e);
rational iv; rational iv;
if (m_autil.is_numeral(i, iv) && iv.is_unsigned()) { if (m_autil.is_numeral(i, iv) && iv.is_unsigned()) {
@ -5501,7 +5502,6 @@ void theory_seq::add_at_axiom(expr* e) {
} }
} }
else { else {
expr_ref len_e = mk_len(e);
expr_ref x = mk_skolem(m_pre, s, i); expr_ref x = mk_skolem(m_pre, s, i);
expr_ref y = mk_skolem(m_tail, s, i); expr_ref y = mk_skolem(m_tail, s, i);
expr_ref xey = mk_concat(x, e, y); expr_ref xey = mk_concat(x, e, y);
@ -5513,6 +5513,7 @@ void theory_seq::add_at_axiom(expr* e) {
add_axiom(i_ge_0, mk_eq(e, emp, false)); add_axiom(i_ge_0, mk_eq(e, emp, false));
add_axiom(~i_ge_len_s, mk_eq(e, emp, false)); add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
add_axiom(mk_literal(m_autil.mk_le(len_e, one)));
} }
/** /**