From 098725aa1cdfb15e36911001a32a6ce8495da274 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Sep 2019 15:01:17 +0200 Subject: [PATCH] fix #2553 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 860d0ec99..2d3db1f98 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2979,10 +2979,15 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect expr_ref_vector lhs(m), rhs(m); lhs.append(l2, ls2); rhs.append(r2, rs2); - deps = mk_join(deps, lit); + for (auto const& e : m_eqs) { + if (e.ls() == lhs && e.rs() == rhs) { + return false; + } + } + deps = mk_join(deps, lit); m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps)); propagate_eq(deps, l, r, true); - TRACE("seq", tout << "propagate eq\nlhs: " << lhs << "\nrhs: " << rhs << "\n";); + TRACE("seq", tout << "propagate eq\n" << m_eqs.size() << "\nlhs: " << lhs << "\nrhs: " << rhs << "\n";); return true; } else {