From 8f297666fe91a6088819da77999e12da0a598ccb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Apr 2020 11:40:16 -0700 Subject: [PATCH] fix #4073 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 00145970aea..1e568e0fb39 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3000,19 +3000,20 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { return; } + expr_ref se1(e1, m), se2(e2, m); + m_rewrite(se1); + m_rewrite(se2); if (is_true) { - expr_ref f1 = m_sk.mk_indexof_left(e1, e2); - expr_ref f2 = m_sk.mk_indexof_right(e1, e2); - f = mk_concat(f1, e2, f2); + expr_ref f1 = m_sk.mk_indexof_left(se1, se2); + expr_ref f2 = m_sk.mk_indexof_right(se1, se2); + f = mk_concat(f1, se2, f2); propagate_eq(lit, f, e1, true); - //literal len2_le_len1 = mk_simplified_literal(m_autil.mk_ge(mk_sub(mk_len(e1), mk_len(e2)), m_autil.mk_int(0))); - //add_axiom(~lit, len2_le_len1); } else { - propagate_non_empty(lit, e2); + propagate_non_empty(lit, se2); dependency* dep = m_dm.mk_leaf(assumption(lit)); // |e1| - |e2| <= -1 - literal len_gt = m_ax.mk_le(mk_sub(mk_len(e1), mk_len(e2)), -1); + literal len_gt = m_ax.mk_le(mk_sub(mk_len(se1), mk_len(se2)), -1); ctx.force_phase(len_gt); m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep)); }