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;