From be4b0ffe69282f52faaf23cf4ed1a239c25d1118 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jun 2017 19:36:38 -0700 Subject: [PATCH] fix unsoundness bug instroduced when fixing #1125 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1c293ad8d..ea53f1342 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2879,7 +2879,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref result(m); expr_dep ed; if (m_rep.find_cache(e, ed)) { - eqs = m_dm.mk_join(eqs, ed.second); + if (e != ed.first) { + eqs = m_dm.mk_join(eqs, ed.second); + } result = ed.first; } else { @@ -2889,9 +2891,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ } expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { expr_ref result(m); - dependency* deps = 0; - result = try_expand(e0, deps); + result = try_expand(e0, eqs); if (result) return result; + dependency* deps = 0; expr* e = m_rep.find(e0, deps); expr* e1, *e2, *e3; expr_ref arg1(m), arg2(m);