print bounded terms for better efficiency

Z3Prover · Oct 21, 2021 · 6eed885 · 6eed885
1 parent 13da6a0
commit 6eed885
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
@@ -967,12 +967,12 @@ namespace opt {
                   tout << "Convert minimization " << orig_term << "\n";
                   tout << "to maxsat: " << term << "\n";
                   for (unsigned i = 0; i < weights.size(); ++i) {
-                      tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n";
+                      tout << mk_pp(terms.get(i), m) << ": " << weights[i] << "\n";
                   }
                   tout << "offset: " << offset << "\n";
                   );
             std::ostringstream out;
-            out << orig_term << ':' << index;
+            out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
             id = symbol(out.str());
             return true;
         }
@@ -995,7 +995,7 @@ namespace opt {
             }
             neg = true;
             std::ostringstream out;
-            out << orig_term << ':' << index;
+            out << mk_bounded_pp(orig_term, m) << ':' << index;
             id = symbol(out.str());
             return true;
         }
@@ -1014,7 +1014,7 @@ namespace opt {
             }
             neg = is_max;
             std::ostringstream out;
-            out << orig_term << ':' << index;
+            out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
             id = symbol(out.str());
             return true;
         }