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

fix #2765

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-01 15:05:38 -08:00
parent 23fcc21543
commit 9ebaf19e47
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_seq.cpp
View file

@ -1895,7 +1895,8 @@ bool theory_seq::check_length_coherence0(expr* e) {
r = assume_equality(e, emp); r = assume_equality(e, emp);
expr* t; expr* t;
unsigned idx; unsigned idx;
if (r != l_true && is_tail(e, t, idx) && idx > m_max_unfolding_depth) { if (r != l_true && is_tail(e, t, idx) &&
idx > m_max_unfolding_depth && m_max_unfolding_lit != null_literal) {
TRACE("seq", tout << "limit unfolding " << m_max_unfolding_depth << " " << mk_pp(e, m) << "\n";); TRACE("seq", tout << "limit unfolding " << m_max_unfolding_depth << " " << mk_pp(e, m) << "\n";);
add_axiom(~m_max_unfolding_lit, mk_eq(e, emp, false)); add_axiom(~m_max_unfolding_lit, mk_eq(e, emp, false));
} }
@ -5449,7 +5450,7 @@ void theory_seq::add_at_axiom(expr* e) {
expr_ref_vector es(m); expr_ref_vector es(m);
expr_ref nth(m); expr_ref nth(m);
unsigned k = iv.get_unsigned(); unsigned k = iv.get_unsigned();
if (k > m_max_unfolding_depth) { if (k > m_max_unfolding_depth && m_max_unfolding_lit != null_literal) {
add_axiom(~m_max_unfolding_lit, i_ge_len_s); add_axiom(~m_max_unfolding_lit, i_ge_len_s);
} }
else { else {