diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp
index 4116945f0..40ad4604a 100644
--- a/src/ast/rewriter/hoist_rewriter.cpp
+++ b/src/ast/rewriter/hoist_rewriter.cpp
@@ -13,8 +13,6 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2019-2-4
 
-Notes:
-
 --*/
 
 
@@ -25,19 +23,17 @@ Notes:
 
 
 hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
-    m_manager(m), m_args1(m), m_args2(m), m_subst(m) { 
+    m(m), m_args1(m), m_args2(m), m_subst(m) { 
     updt_params(p); 
 }
 
 br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
-    if (num_args < 2) {
+    if (num_args < 2) 
         return BR_FAILED;
-    }
-    for (unsigned i = 0; i < num_args; ++i) {
-        if (!is_and(es[i], nullptr)) {
+
+    for (unsigned i = 0; i < num_args; ++i) 
+        if (!is_and(es[i], nullptr)) 
             return BR_FAILED;
-        }
-    }
 
     bool turn = false;
     m_preds1.reset(); 
@@ -52,12 +48,10 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
     VERIFY(is_and(es[0], args[turn]));
     expr* e1, *e2;
     for (expr* e : *(args[turn])) {
-        if (m().is_eq(e, e1, e2)) {            
+        if (m.is_eq(e, e1, e2))             
             (*uf)[turn].merge(mk_var(e1), mk_var(e2));
-        }
-        else {
+        else 
             (*preds)[turn].insert(e);
-        }
     }
     unsigned round = 0;
     for (unsigned j = 1; j < num_args; ++j) {
@@ -72,44 +66,39 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
         VERIFY(is_and(es[j], args[turn]));
 
         for (expr* e : *args[turn]) {
-            if (m().is_eq(e, e1, e2)) {
+            if (m.is_eq(e, e1, e2)) {
                 m_es.push_back(e1);                
                 m_uf0.merge(mk_var(e1), mk_var(e2));
             }    
-            else if ((*preds)[last].contains(e)) {
+            else if ((*preds)[last].contains(e)) 
                 (*preds)[turn].insert(e);
-            }
         }
 
-        if ((*preds)[turn].empty() && m_es.empty()) {
+        if ((*preds)[turn].empty() && m_es.empty()) 
             return BR_FAILED;
-        }
 
         m_eqs.reset();
         for (expr* e : m_es) {
-            if (m_mark.is_marked(e)) {
+            if (m_mark.is_marked(e)) 
                 continue;
-            }
             unsigned u = mk_var(e);
             unsigned v = u;
             m_roots.reset();
             do {
                 m_mark.mark(e);
                 unsigned r = (*uf)[last].find(v);
-                if (m_roots.find(r, e2)) {
-                    m_eqs.push_back(std::make_pair(e, e2));
-                }
-                else {
+                if (m_roots.find(r, e2)) 
+                    m_eqs.push_back({e, e2});
+                else 
                     m_roots.insert(r, e);
-                }
                 v = m_uf0.next(v);
                 e = mk_expr(v);
             }
             while (u != v);
         }
         reset((*uf)[turn]);
-        for (auto const& p : m_eqs) 
-            (*uf)[turn].merge(mk_var(p.first), mk_var(p.second));
+        for (auto const& [e1, e2] : m_eqs) 
+            (*uf)[turn].merge(mk_var(e1), mk_var(e2));
         if ((*preds)[turn].empty() && m_eqs.empty()) 
             return BR_FAILED;
     }
@@ -118,25 +107,23 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
         return BR_DONE;
     }
     // p & eqs & (or fmls)
-    expr_ref_vector fmls(m());
+    expr_ref_vector fmls(m);
     m_subst.reset();
     for (expr * p : (*preds)[turn]) {
         expr* q = nullptr;
-        if (m().is_not(p, q)) {
-            m_subst.insert(q, m().mk_false());
-        }
-        else {
-            m_subst.insert(p, m().mk_true());
-        }
+        if (m.is_not(p, q)) 
+            m_subst.insert(q, m.mk_false());
+        else 
+            m_subst.insert(p, m.mk_true());
         fmls.push_back(p);
     }
     for (auto& p : m_eqs) {
-        if (m().is_value(p.first))
+        if (m.is_value(p.first))
             std::swap(p.first, p.second);
         m_subst.insert(p.first, p.second);
-        fmls.push_back(m().mk_eq(p.first, p.second));
+        fmls.push_back(m.mk_eq(p.first, p.second));
     }    
-    expr_ref ors(::mk_or(m(), num_args, es), m());
+    expr_ref ors(::mk_or(m, num_args, es), m);
     m_subst(ors);
     fmls.push_back(ors);
     result = mk_and(fmls);
@@ -146,9 +133,8 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
 
 unsigned hoist_rewriter::mk_var(expr* e) {
     unsigned v = 0;
-    if (m_expr2var.find(e, v)) {
+    if (m_expr2var.find(e, v)) 
         return v;
-    }
     m_uf1.mk_var();
     v = m_uf2.mk_var();
     SASSERT(v == m_var2expr.size());
@@ -158,15 +144,14 @@ unsigned hoist_rewriter::mk_var(expr* e) {
 }
 
 expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
-    expr_ref result(m());
-    expr_ref_vector args(m()), fmls(m());
+    expr_ref result(m);
+    expr_ref_vector args(m), fmls(m);
     for (unsigned i = 0; i < num_args; ++i) {
         VERIFY(is_and(es[i], &m_args1));
         fmls.reset();
-        for (expr* e : m_args1) {
+        for (expr* e : m_args1) 
             if (!preds.contains(e))
                 fmls.push_back(e);
-        }
         args.push_back(::mk_and(fmls));
     }
     fmls.reset();
@@ -188,19 +173,18 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
 }
 
 bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
-    if (m().is_and(e)) {
+    if (m.is_and(e)) {
         if (args) {
             args->reset();
             args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
         }
         return true;
     }
-    if (m().is_not(e, e) && m().is_or(e)) {
+    if (m.is_not(e, e) && m.is_or(e)) {
         if (args) {
             args->reset();
-            for (expr* arg : *to_app(e)) {
-                args->push_back(::mk_not(m(), arg));
-            }
+            for (expr* arg : *to_app(e)) 
+                args->push_back(::mk_not(m, arg));
         }
         return true;
     }
diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h
index 2c627ad59..cc83bfa56 100644
--- a/src/ast/rewriter/hoist_rewriter.h
+++ b/src/ast/rewriter/hoist_rewriter.h
@@ -26,7 +26,7 @@ Notes:
 #include "util/obj_hashtable.h"
 
 class hoist_rewriter {
-    ast_manager &  m_manager;
+    ast_manager &                   m;
     expr_ref_vector                 m_args1, m_args2;
     obj_hashtable<expr>             m_preds1, m_preds2;
     basic_union_find                m_uf1, m_uf2, m_uf0;
@@ -34,11 +34,9 @@ class hoist_rewriter {
     svector<std::pair<expr*,expr*>> m_eqs;
     u_map<expr*>                    m_roots;
     expr_safe_replace               m_subst;
-    obj_map<expr, unsigned> m_expr2var;
-    ptr_vector<expr>        m_var2expr;
-    expr_mark               m_mark;
-
-    br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
+    obj_map<expr, unsigned>         m_expr2var;
+    ptr_vector<expr>                m_var2expr;
+    expr_mark                       m_mark;
 
     bool is_and(expr* e, expr_ref_vector* args);
 
@@ -52,12 +50,12 @@ class hoist_rewriter {
 
 public:
     hoist_rewriter(ast_manager & m, params_ref const & p = params_ref());
-    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); }       
+    family_id get_fid() const { return m.get_basic_family_id(); }
+    bool is_eq(expr * t) const { return m.is_eq(t); }       
     void updt_params(params_ref const & p) {}
     static void get_param_descrs(param_descrs & r) {}
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);    
+    br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);    
 };
 
 struct hoist_rewriter_cfg : public default_rewriter_cfg {