#5452

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 4, 2021 · 9398601 · 9398601
1 parent 2891ac7
commit 9398601
Showing 1 changed file with 3 additions and 6 deletions.
diff --git 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();
             }