diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index a92799c4c71..7728716fd29 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -270,7 +270,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 return BR_DONE;
         }
 
-#if 1
+#if 0
         br_status st;
         expr_ref r(m());
         st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
@@ -282,7 +282,7 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 get_num_internal_exprs(m_counts2, m_todo2, args[i]);
             unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
             unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
-            if (count1 > count2 + num_args)
+            if (count1 > count2)
                 st = BR_FAILED;
         }
         if (st != BR_FAILED)