From 0c42d3b079483bb449faf36864a32e5a71093942 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jul 2022 11:41:48 -0700 Subject: [PATCH] small format update Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e1285e749..e5e0c9cb0 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3216,18 +3216,15 @@ void theory_seq::relevant_eh(app* n) { add_ubv_string(n); expr* arg = nullptr; - if (m_sk.is_tail(n, arg)) { + if (m_sk.is_tail(n, arg)) add_length_limit(arg, m_max_unfolding_depth, true); - } - if (m_util.str.is_length(n, arg) && !has_length(arg) && ctx.e_internalized(arg)) { + if (m_util.str.is_length(n, arg) && !has_length(arg) && ctx.e_internalized(arg)) add_length_to_eqc(arg); - } if (m_util.str.is_replace_all(n) || m_util.str.is_replace_re(n) || - m_util.str.is_replace_re_all(n) - ) { + m_util.str.is_replace_re_all(n)) { add_unhandled_expr(n); } }