print weight if it is different from default #2667

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 14, 2019 · 784e272 · 784e272
1 parent 5f90e72
commit 784e272
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
@@ -957,8 +957,8 @@ class smt2_printer {
         unsigned num_lets = 0;
         format * f_body = pp_let(m_format_stack.back(), num_lets);
         // The current SMT2 frontend uses weight 1 as default.
-#define MIN_WEIGHT 1
-        if (q->has_patterns() || q->get_weight() > MIN_WEIGHT ||
+#define DEFAULT_WEIGHT 1
+        if (q->has_patterns() || q->get_weight() != DEFAULT_WEIGHT ||
             q->get_skid() != symbol::null || (q->get_qid() != symbol::null && !q->get_qid().is_numerical())) {
             ptr_buffer<format> buf;
             buf.push_back(f_body);
@@ -976,7 +976,7 @@ class smt2_printer {
                     buf.push_back(pp_attribute(":no-pattern ", *it));
                 }
             }
-            if (q->get_weight() > MIN_WEIGHT) {
+            if (q->get_weight() != DEFAULT_WEIGHT) {
                 buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
             }
             if (q->get_skid() != symbol::null) {