From 9ebaf19e477bb36236eaa5227c0f21eef0186ae6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Dec 2019 15:05:38 -0800 Subject: [PATCH] fix #2765 --- src/smt/theory_seq.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 6e9a71245..411a365f3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1895,7 +1895,8 @@ bool theory_seq::check_length_coherence0(expr* e) { r = assume_equality(e, emp); expr* t; 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";); 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 nth(m); 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); } else {