diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 95638cef73c..720f9054318 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -503,10 +503,7 @@ class pb_preprocess_tactic : public tactic { bool found = false; for (unsigned j = 0; j < args2.size(); ++j) { if (is_complement(args1.get(i), args2.get(j))) { - if (i == 0) { - min_coeff = coeffs2[j]; - } - else if (min_coeff > coeffs2[j]) { + if (i == 0 || min_coeff > coeffs2[j]) { min_coeff = coeffs2[j]; min_index = j; } @@ -517,9 +514,9 @@ class pb_preprocess_tactic : public tactic { if (!found) return; } - for (unsigned i = 0; i < indices.size(); ++i) { - unsigned j = indices[i]; + for (unsigned j : indices) { expr* arg = args2.get(j); + TRACE("pb", tout << "j " << j << " " << min_index << "\n";); if (j == min_index) { args2[j] = m.mk_false(); }