From e37954d87bdc55d9b8357f4445b813db6aaab878 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Jul 2018 09:16:52 -0700 Subject: [PATCH] simplify code fix for #1725 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 07eb97f31..48fd0c726 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -532,10 +532,7 @@ unsigned_vector theory_seq::overlap(expr_ref_vector const& ls, expr_ref_vector c return result; } result.reset(); - if (eq_unit(ls[0], rs.back())) { - result.push_back(1); - } - for (unsigned i = 1; i < ls.size(); ++i) { + for (unsigned i = 0; i < ls.size(); ++i) { if (eq_unit(ls[i], rs.back())) { bool same = rs.size() > i; for (unsigned j = 0; same && j < i; ++j) {