diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 442bef855db..632b6c0f606 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -24,7 +24,7 @@ Module Name:
 
 void bool_rewriter::updt_params(params_ref const & _p) {
     bool_rewriter_params p(_p);
-    m_flat_and_or          = p.flat();
+    m_flat_and_or          = p.flat_and_or();
     m_elim_and             = p.elim_and();
     m_elim_ite             = p.elim_ite();
     m_local_ctx            = p.local_ctx();
@@ -267,6 +267,15 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 return BR_DONE;
         }
 
+#if 1
+        br_status st;
+        st = m_hoist.mk_or(buffer.size(), buffer.data(), result);
+        if (st == BR_DONE)
+            return BR_REWRITE1;
+        if (st != BR_FAILED)
+            return st;
+#endif
+
         if (s) {
             ast_lt lt;
             std::sort(buffer.begin(), buffer.end(), lt);       
diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h
index a25a0f8a31e..2cec0b2ce82 100644
--- a/src/ast/rewriter/bool_rewriter.h
+++ b/src/ast/rewriter/bool_rewriter.h
@@ -20,6 +20,7 @@ Module Name:
 
 #include "ast/ast.h"
 #include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/hoist_rewriter.h"
 #include "util/params.h"
 
 /**
@@ -50,6 +51,7 @@ Module Name:
 */
 class bool_rewriter {
     ast_manager &  m_manager;
+    hoist_rewriter m_hoist;
     bool           m_flat_and_or;
     bool           m_local_ctx;
     bool           m_elim_and;
@@ -78,7 +80,7 @@ class bool_rewriter {
     void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
 
 public:
-    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
+    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { updt_params(p); }
     ast_manager & m() const { return m_manager; }
     family_id get_fid() const { return m().get_basic_family_id(); }
     bool is_eq(expr * t) const { return m().is_eq(t); }