From ad6062cd9e1ade2a7d4443588e05c8cfba3e9528 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Mar 2020 12:49:26 -0800 Subject: [PATCH] disable unsound code to fix #3100 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 01c55e6cb..fe47d4dac 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -635,6 +635,16 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c if (same) result.push_back(i+1); } +#if 0 + if (eq_unit(ls[i], rs[0])) { + bool same = ls.size() - i >= rs.size(); + for (unsigned j = 0; same && j < rs.size(); ++j) { + same = eq_unit(ls[i+j], rs[j]); + } + if (same) + result.push_back(i); + } +#endif } m_overlap.insert(pair, result); return result; @@ -757,12 +767,16 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) { expr_ref ZxsE = mk_concat(Z, xsE); expr_ref y1ysZ = mk_concat(y1ys, Z); if (indexes.empty()) { - TRACE("seq", tout << "one case\n";); - TRACE("seq", display_equation(tout, e);); + return false; +#if 0 + TRACE("seq", display_equation(tout << "one case\n", e); + tout << "xs: " << xs << "\n"; + tout << "ys: " << ys << "\n";); literal_vector lits; dependency* dep = e.dep(); propagate_eq(dep, lits, x, y1ysZ, true); propagate_eq(dep, lits, y2, ZxsE, true); +#endif } else { expr_ref ge(m_autil.mk_ge(mk_len(y2), m_autil.mk_int(xs.size())), m);