diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index bb283b32f..6a974db59 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -27,7 +27,7 @@ Revision History:
 #include "tactic/ufbv/ufbv_rewriter.h"
 
 ufbv_rewriter::ufbv_rewriter(ast_manager & m):
-    m_manager(m),
+    m(m),
     m_match_subst(m),
     m_bsimp(m),
     m_todo(m),
@@ -42,27 +42,25 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m):
 ufbv_rewriter::~ufbv_rewriter() {
     reset_dealloc_values(m_fwd_idx);
     reset_dealloc_values(m_back_idx);
-    for (demodulator2lhs_rhs::iterator it = m_demodulator2lhs_rhs.begin(); it != m_demodulator2lhs_rhs.end(); it++) {
-        m_manager.dec_ref(it->m_key);
-        m_manager.dec_ref(it->m_value.first);
-        m_manager.dec_ref(it->m_value.second);
+    for (auto & kv : m_demodulator2lhs_rhs) {
+        m.dec_ref(kv.m_key);
+        m.dec_ref(kv.m_value.first);
+        m.dec_ref(kv.m_value.second);
     }
 }
 
 bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const {
-    if (e->get_kind() == AST_QUANTIFIER) {
+    if (is_quantifier(e)) {
         quantifier * q = to_quantifier(e);
         if (is_forall(q)) {
             expr * qe = q->get_expr();
-            if ((m_manager.is_eq(qe) || m_manager.is_iff(qe))) {
-                app * eq = to_app(q->get_expr());
-                expr * lhs = eq->get_arg(0);
-                expr * rhs = eq->get_arg(1);
+            expr * lhs = nullptr, *rhs = nullptr;
+            if (m.is_eq(qe, lhs, rhs)) {
                 int subset = is_subset(lhs, rhs);
                 int smaller = is_smaller(lhs, rhs);
                 TRACE("demodulator", tout << "testing is_demodulator:\n"
-                      << mk_pp(lhs, m_manager) << "\n"
-                      << mk_pp(rhs, m_manager) << "\n"
+                      << mk_pp(lhs, m) << "\n"
+                      << mk_pp(rhs, m) << "\n"
                       << "subset: " << subset << ", smaller: " << smaller << "\n";);
                 // We only track uninterpreted functions, everything else is likely too expensive.
                 if ((subset == +1 || subset == +2) && smaller == +1) {
@@ -74,9 +72,9 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
 #if 1
                     // lhs = (not rhs) --> (not lhs) = rhs
                     expr * not_rhs;
-                    if (m_manager.is_not(rhs, not_rhs) && is_uninterp(not_rhs)) {
+                    if (m.is_not(rhs, not_rhs) && is_uninterp(not_rhs)) {
                         large = not_rhs;
-                        small = m_manager.mk_not(lhs);
+                        small = m.mk_not(lhs);
                         return true;
                     }
 #endif
@@ -91,23 +89,23 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
 #if 1
                     // (not lhs) = rhs --> lhs = (not rhs)
                     expr * not_lhs;
-                    if (m_manager.is_not(lhs, not_lhs) && is_uninterp(not_lhs)) {
+                    if (m.is_not(lhs, not_lhs) && is_uninterp(not_lhs)) {
                         large = not_lhs;
-                        small = m_manager.mk_not(rhs);
+                        small = m.mk_not(rhs);
                         return true;
                     }
 #endif
                 }
 
-            } else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0))) {
+            } else if (m.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0))) {
                 // this is like (not (f ... )) --> (= (f ...) false)
                 large = to_app(qe)->get_arg(0);
-                small = m_manager.mk_false();
+                small = m.mk_false();
                 return true;
             } else if (is_uninterp(qe)) {
                 // this is like (f ... ) --> (= (f ...) true)
                 large = to_app(qe);
-                small = m_manager.mk_true();
+                small = m.mk_true();
                 return true;
             }
         }
@@ -128,7 +126,7 @@ public:
 int ufbv_rewriter::is_subset(expr * e1, expr * e2) const {
     uint_set ev1, ev2;
 
-    if (m_manager.is_value(e1))
+    if (m.is_value(e1))
         return 1; // values are always a subset!
 
     var_set_proc proc1(ev1);
@@ -146,9 +144,9 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
     unsigned sz1 = 0, sz2 = 0;
 
     // values are always smaller!
-    if (m_manager.is_value(e1))
+    if (m.is_value(e1))
         return +1;
-    else if (m_manager.is_value(e2))
+    else if (m.is_value(e2))
         return -1;
 
     // interpreted stuff is always better than uninterpreted.
@@ -217,7 +215,7 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo
     SASSERT(large->get_kind() == AST_APP);
     SASSERT(demodulator);
     SASSERT(large && small);
-    TRACE("demodulator_fwd", tout << "INSERT: " << mk_pp(demodulator, m_manager) << std::endl; );
+    TRACE("demodulator_fwd", tout << "INSERT: " << mk_pp(demodulator, m) << std::endl; );
 
     func_decl * fd = to_app(large)->get_decl();
 
@@ -231,9 +229,9 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo
     SASSERT(it->m_value);
     it->m_value->insert(demodulator);
 
-    m_manager.inc_ref(demodulator);
-    m_manager.inc_ref(large);
-    m_manager.inc_ref(small);
+    m.inc_ref(demodulator);
+    m.inc_ref(large);
+    m.inc_ref(small);
     m_demodulator2lhs_rhs.insert(demodulator, expr_pair(large, small));
 }
 
@@ -243,9 +241,9 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
     fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
     if (it != m_fwd_idx.end()) {
         demodulator2lhs_rhs::iterator fit = m_demodulator2lhs_rhs.find_iterator(demodulator);
-        m_manager.dec_ref(fit->m_value.first);
-        m_manager.dec_ref(fit->m_value.second);
-        m_manager.dec_ref(demodulator);
+        m.dec_ref(fit->m_value.first);
+        m.dec_ref(fit->m_value.second);
+        m.dec_ref(demodulator);
         m_demodulator2lhs_rhs.erase(demodulator);
         it->m_value->erase(demodulator);
     } else {
@@ -254,12 +252,12 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
 }
 
 bool ufbv_rewriter::check_fwd_idx_consistency() {
-    for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
-        quantifier_set * set = it->m_value;
+    for (auto & kv : m_fwd_idx) {
+        quantifier_set * set = kv.m_value;
         SASSERT(set);
-
-        for (quantifier_set::iterator sit = set->begin(); sit != set->end(); sit++) {
-            if (!m_demodulator2lhs_rhs.contains(*sit)) return false;
+        for (auto e : *set) {
+            if (!m_demodulator2lhs_rhs.contains(e)) 
+                return false;
         }
     }
 
@@ -267,20 +265,20 @@ bool ufbv_rewriter::check_fwd_idx_consistency() {
 }
 
 void ufbv_rewriter::show_fwd_idx(std::ostream & out) {
-    for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
-        quantifier_set * set = it->m_value;
+    for (auto & kv : m_fwd_idx) {
+        quantifier_set * set = kv.m_value;
         SASSERT(!set);
 
-        out << it->m_key->get_name() << ": " << std::endl;
+        out << kv.m_key->get_name() << ": " << std::endl;
 
-        for (quantifier_set::iterator sit = set->begin(); sit != set->end(); sit++) {
-            out << std::hex << (size_t)*sit << std::endl;
+        for (auto e : *set) {
+            out << std::hex << (size_t)e << std::endl;
         }
     }
 
     out << "D2LR: " << std::endl;
-    for (demodulator2lhs_rhs::iterator it = m_demodulator2lhs_rhs.begin(); it != m_demodulator2lhs_rhs.end() ; it++) {
-        out << (size_t) it->m_key << std::endl;
+    for (auto & kv : m_demodulator2lhs_rhs) {
+        out << (size_t) kv.m_key << std::endl;
     }
 }
 
@@ -288,11 +286,8 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_
     fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
     if (it != m_fwd_idx.end()) {
         TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n";
-              for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; });
-        quantifier_set::iterator dit = it->m_value->begin();
-        quantifier_set::iterator dend = it->m_value->end();
-        for ( ; dit != dend ; dit++ ) {
-            quantifier * d = *dit;
+              for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; });
+        for (quantifier* d : *it->m_value) {
 
             SASSERT(m_demodulator2lhs_rhs.contains(d));
             expr_pair l_s;
@@ -302,12 +297,12 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_
             if (large->get_num_args() != m_new_args.size())
                 continue;
 
-            TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m_manager) << std::endl; );
+            TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m) << std::endl; );
 
             SASSERT(large->get_decl() == f);
 
             if (m_match_subst(large, l_s.second, m_new_args.c_ptr(), np)) {
-                TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m_manager) << "\n===>\n" << mk_pp(np, m_manager) << "\n";);
+                TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m) << "\n===>\n" << mk_pp(np, m) << "\n";);
                 return true;
             }
         }
@@ -334,7 +329,7 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) {
                 if (m_rewrite_todo[i - 1] == v) {
                     recursive = true;
                     TRACE("demodulator", tout << "Detected demodulator cycle: " <<
-                        mk_pp(a, m_manager) << " --> " << mk_pp(v, m_manager) << std::endl;);
+                        mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;);
                     m_rewrite_cache.insert(e, expr_bool_pair(v, true));
                     break;
                 }
@@ -356,7 +351,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
     if (m_fwd_idx.empty())
         return n;
 
-    TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m_manager) << std::endl; );
+    TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m) << std::endl; );
     app * a;
 
     SASSERT(m_rewrite_todo.empty());
@@ -367,7 +362,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
         TRACE("demodulator_stack", tout << "STACK: " << std::endl;
               for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
                   tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] <<
-                  " = " << mk_pp(m_rewrite_todo[i], m_manager) << std::endl;
+                  " = " << mk_pp(m_rewrite_todo[i], m) << std::endl;
               );
 
         expr * e = m_rewrite_todo.back();
@@ -406,7 +401,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
                         all_untouched = false;
                     m_new_args.push_back(n_child);
                 }
-                expr_ref np(m_manager);
+                expr_ref np(m);
                 if (rewrite1(f, m_new_args, np)) {
                     rewrite_cache(e, np, false);
                     // No pop.
@@ -415,15 +410,15 @@ expr * ufbv_rewriter::rewrite(expr * n) {
                         rewrite_cache(e, actual, true);
                     }
                     else {
-                        expr_ref na(m_manager);
-                        if (f->get_family_id() != m_manager.get_basic_family_id())
-                            na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
+                        expr_ref na(m);
+                        if (f->get_family_id() != m.get_basic_family_id())
+                            na = m.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
                         else
                             m_bsimp.mk_app(f, m_new_args.size(), m_new_args.c_ptr(), na);
-                        TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n";
-                              for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; }
+                        TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m) << "\nnew_args: \n";
+                              for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; }
                               tout << "=====>\n";
-                              tout << "na:\n " << mk_pp(na, m_manager) << "\n";);
+                              tout << "na:\n " << mk_pp(na, m) << "\n";);
                         rewrite_cache(e, na, true);
                     }
                     m_rewrite_todo.pop_back();
@@ -436,10 +431,10 @@ expr * ufbv_rewriter::rewrite(expr * n) {
                 const expr_bool_pair ebp = m_rewrite_cache.get(body);
                 SASSERT(ebp.second);
                 expr * new_body = ebp.first;
-                quantifier_ref q(m_manager);
-                q = m_manager.update_quantifier(to_quantifier(actual), new_body);
+                quantifier_ref q(m);
+                q = m.update_quantifier(to_quantifier(actual), new_body);
                 m_new_exprs.push_back(q);
-                expr_ref new_q = elim_unused_vars(m_manager, q, params_ref());
+                expr_ref new_q = elim_unused_vars(m, q, params_ref());
                 m_new_exprs.push_back(new_q);
                 rewrite_cache(e, new_q, true);
                 m_rewrite_todo.pop_back();
@@ -458,7 +453,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
     SASSERT(ebp.second);
     expr * r = ebp.first;
 
-    TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m_manager) << std::endl; );
+    TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m) << std::endl; );
 
     return r;
 }
@@ -517,18 +512,12 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
         SASSERT(it->m_value);
         expr_set temp;
 
-        expr_set::iterator sit  = it->m_value->begin();
-        expr_set::iterator send = it->m_value->end();
-        for ( ; sit != send ; sit++ ) {
-            expr * p = *sit;
+        for (expr* p : *it->m_value) {
             if (m_processed.contains(p))
               temp.insert(p);
         }
 
-        sit  = temp.begin();
-        send = temp.end();
-        for ( ; sit != send; sit++) {
-            expr * p = *sit;
+        for (expr * p : temp) {
             // remove p from m_processed and m_back_idx
             m_processed.remove(p);
             remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
@@ -605,18 +594,13 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
     if (it != m_back_idx.end()) {
         SASSERT(it->m_value);
         expr_set all_occurrences;
-        expr_ref l(m_manager);
+        expr_ref l(m);
 
-        expr_set::iterator esit = it->m_value->begin();
-        expr_set::iterator esend = it->m_value->end();
-        for ( ; esit != esend ; esit++)
-          all_occurrences.insert(*esit);
+        for (auto s : *it->m_value) 
+          all_occurrences.insert(s);
 
         // Run over all f-demodulators
-        esit = all_occurrences.begin();
-        esend = all_occurrences.end();
-        for ( ; esit != esend ; esit++ ) {
-            expr * occ = *esit;
+        for (expr* occ : all_occurrences) {
 
             if (!is_quantifier(occ))
                 continue;
@@ -625,15 +609,15 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
             demodulator2lhs_rhs::iterator d2lr_it = m_demodulator2lhs_rhs.find_iterator(to_quantifier(occ));
             if (d2lr_it != m_demodulator2lhs_rhs.end()) {
                 l = d2lr_it->m_value.first;
-                quantifier_ref d(m_manager);
-                func_decl_ref df(m_manager);
+                quantifier_ref d(m);
+                func_decl_ref df(m);
                 d = to_quantifier(occ);
                 df = to_app(l)->get_decl();
 
                 // Now we know there is an occurrence of f in d
                 //   if n' can rewrite d {
                 if (can_rewrite(d, lhs)) {
-                    TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m_manager) << std::endl; );
+                    TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m) << std::endl; );
                     //     remove d from m_fwd_idx
                     remove_fwd_idx(df, d);
                     //     remove d from m_back_idx
@@ -647,16 +631,11 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
             }
         }
     }
-
-    //for (ptr_vector<expr>::iterator it = to_remove.begin(); it != to_remove.end(); it++) {
-    //    expr * d = *it;
-    //    remove_back_idx_proc proc(m_manager, m_back_idx, d);
-    //    for_each_expr(proc, d);
-    //}
 }
 
-void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
-    if (m_manager.proofs_enabled()) {
+void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, 
+                               expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
+    if (m.proofs_enabled()) {
         TRACE("tactic", tout << "PRE_DEMODULATOR=true is not supported when proofs are enabled.";);
         // Let us not waste time with proof production
         new_exprs.append(n, exprs);
@@ -666,7 +645,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
 
     TRACE("demodulator", tout << "before demodulator:\n";
                          for ( unsigned i = 0 ; i < n ; i++ )
-                            tout << mk_pp(exprs[i], m_manager) << std::endl; );
+                            tout << mk_pp(exprs[i], m) << std::endl; );
 
     // Initially, m_todo contains all formulas. That is, it contains the argument exprs. m_fwd_idx, m_processed, m_back_idx are empty.
     unsigned max_vid = 0;
@@ -679,17 +658,18 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
 
     while (!m_todo.empty()) {
         // let n be the next formula in m_todo.
-        expr_ref cur(m_manager);
+        expr_ref cur(m);
         cur = m_todo.back();
         m_todo.pop_back();
 
         // rewrite cur using m_fwd_idx, and let n' be the result.
-        expr * np = rewrite(cur);
+        expr_ref np(rewrite(cur), m);
         // at this point, it should be the case that there is no demodulator in m_fwd_idx that can rewrite n'.
-        SASSERT(rewrite(np)==np);
+        // unless there is a demodulator cycle
+        // SASSERT(rewrite(np)==np);
 
         //    if (n' is not a demodulator) {
-        expr_ref large(m_manager), small(m_manager);
+        expr_ref large(m), small(m);
         if (!is_demodulator(np, large, small)) {
             // insert n' into m_processed
             m_processed.insert(np);
@@ -699,8 +679,8 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
         } else {
             // np is a demodulator that allows us to replace 'large' with 'small'.
             TRACE("demodulator", tout << "Found demodulator: " << std::endl;
-                                 tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " <<
-                                      std::endl << mk_pp(small.get(), m_manager) << std::endl; );
+                                 tout << mk_pp(large.get(), m) << std::endl << " ---> " <<
+                                      std::endl << mk_pp(small.get(), m) << std::endl; );
 
             TRACE("demodulator_s", tout << "Found demodulator: " << std::endl;
                                    tout << to_app(large)->get_decl()->get_name() <<
@@ -709,7 +689,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
                                        tout << to_app(small)->get_decl()->get_name() <<
                                         "[" << to_app(small)->get_depth() << "]" << std::endl;
                                    else
-                                       tout << mk_pp(small.get(), m_manager) << std::endl; );
+                                       tout << mk_pp(small.get(), m) << std::endl; );
 
             // let f be the top symbol of n'
             SASSERT(is_app(large));
@@ -728,35 +708,26 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
     }
 
     // the result is the contents of m_processed + all demodulators in m_fwd_idx.
-    obj_hashtable<expr>::iterator pit = m_processed.begin();
-    obj_hashtable<expr>::iterator pend = m_processed.end();
-    for ( ; pit != pend ; pit++ ) {
-        new_exprs.push_back(*pit);
-        TRACE("demodulator", tout << mk_pp(*pit, m_manager) << std::endl; );
+    for (expr* e : m_processed) {
+        new_exprs.push_back(e);
+        TRACE("demodulator", tout << mk_pp(e, m) << std::endl; );
     }
 
-    fwd_idx_map::iterator fit = m_fwd_idx.begin();
-    fwd_idx_map::iterator fend = m_fwd_idx.end();
-    for ( ; fit != fend ; fit++ ) {
-        if (fit->m_value) {
-            quantifier_set::iterator dit = fit->m_value->begin();
-            quantifier_set::iterator dend = fit->m_value->end();
-            for ( ; dit != dend ; dit++ ) {
-                expr * e = *dit;
+    for (auto const& kv : m_fwd_idx) {
+        if (kv.m_value) {
+            for (expr* e : *kv.m_value) {
                 new_exprs.push_back(e);
-                TRACE("demodulator", tout << mk_pp(*dit, m_manager) << std::endl; );
+                TRACE("demodulator", tout << mk_pp(e, m) << std::endl; );
             }
         }
     }
 
-    TRACE("demodulator", tout << "after demodulator:\n";
-                         for ( unsigned i = 0 ; i < new_exprs.size() ; i++ )
-                            tout << mk_pp(new_exprs[i].get(), m_manager) << std::endl; );
+    TRACE("demodulator", tout << "after demodulator:\n" << new_exprs << "\n";);
 }
 
 
 ufbv_rewriter::match_subst::match_subst(ast_manager & m):
-    m_manager(m),
+    m(m),
     m_subst(m) {
 }
 
diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/tactic/ufbv/ufbv_rewriter.h
index c6e01528c..ca8d3062b 100644
--- a/src/tactic/ufbv/ufbv_rewriter.h
+++ b/src/tactic/ufbv/ufbv_rewriter.h
@@ -101,11 +101,11 @@ class ufbv_rewriter {
     typedef std::pair<expr *, bool> expr_bool_pair;
 
     class plugin {
-        ast_manager& m_manager;
+        ast_manager& m;
     public:
-        plugin(ast_manager& m): m_manager(m) { }        
-        void ins_eh(expr* k, expr_bool_pair v) { m_manager.inc_ref(k); m_manager.inc_ref(v.first); }
-        void del_eh(expr* k, expr_bool_pair v) { m_manager.dec_ref(k); m_manager.dec_ref(v.first); }
+        plugin(ast_manager& m): m(m) { }        
+        void ins_eh(expr* k, expr_bool_pair v) { m.inc_ref(k); m.inc_ref(v.first); }
+        void del_eh(expr* k, expr_bool_pair v) { m.dec_ref(k); m.dec_ref(v.first); }
         static unsigned to_int(expr const * k) { return k->get_id(); }
     };
     typedef array_map<expr*, expr_bool_pair, plugin> expr_map;
@@ -127,7 +127,7 @@ class ufbv_rewriter {
 
         void reset();
 
-        ast_manager &         m_manager;
+        ast_manager &         m;
         substitution          m_subst;
         cache                 m_cache;
         svector<expr_pair>    m_todo;
@@ -157,7 +157,7 @@ class ufbv_rewriter {
         bool operator()(expr * t, expr * i);
     };
 
-    ast_manager &       m_manager;
+    ast_manager &       m;
     match_subst         m_match_subst;
     bool_rewriter       m_bsimp;
     fwd_idx_map         m_fwd_idx;