formatting updates

Z3Prover · Apr 13, 2023 · 444238b · 444238b
1 parent f61168c
commit 444238b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp
@@ -92,7 +92,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
             else {
                 result = m.mk_app(f, numeral, _args[0]);
             }
-            TRACE("ac_sharing_detail", tout << "result: " << mk_pp(result, m) << "\n";);
+            TRACE("ac_sharing_detail", tout << "result: " << result << "\n";);
             return BR_DONE;
         }
     }

diff --git a/src/model/value_factory.h b/src/model/value_factory.h
@@ -194,9 +194,8 @@ class simple_factory : public value_factory {
         while (!is_new) {
             result = mk_value(next, s, is_new);
             next++;
-            if (has_max && next > max_size + start) {
-                return nullptr;
-            }
+            if (has_max && next > max_size + start)
+                return nullptr;            
         }
         SASSERT(result != 0);
         return result;