From 444238bc538e4017c38cf2955daad873503b04f6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Apr 2023 14:28:08 -0700
Subject: [PATCH] formatting updates

---
 src/ast/rewriter/maximize_ac_sharing.cpp | 2 +-
 src/model/value_factory.h                | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp
index a8bee62d5..b5ebb9f1c 100644
--- 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
index edb12b095..20c383efe 100644
--- a/src/model/value_factory.h
+++ b/src/model/value_factory.h
@@ -194,9 +194,8 @@ public:
         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;