mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
simplify code fix for #1725
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ec6260342b
commit
e37954d87b
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue