diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 61aa48d9c..a08ef09af 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -25,6 +25,7 @@ Revision History:
 #include "ast/normal_forms/nnf.h"
 #include "ast/pattern/pattern_inference.h"
 #include "ast/macros/quasi_macros.h"
+#include "ast/occurs.h"
 #include "smt/asserted_formulas.h"
 
 asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
@@ -133,7 +134,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
     m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
     m_params.set_bool("gcd_rounding", true);
     m_params.set_bool("expand_select_store", true);
-    m_params.set_bool("expand_nested_stores", true);
+    //m_params.set_bool("expand_nested_stores", true);
     m_params.set_bool("bv_sort_ac", true);
     m_params.set_bool("som", true);
     m_rewriter.updt_params(m_params);
@@ -555,6 +556,14 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
         return false;
     }
     SASSERT(is_ground(lhs) && is_ground(rhs));
+#if 0
+    if (is_uninterp_const(lhs) && is_app(rhs) && to_app(rhs)->get_num_args() > 0 && !occurs(lhs, rhs)) {
+        return true;
+    }
+    if (is_uninterp_const(rhs) && is_app(lhs) && to_app(lhs)->get_num_args() > 0 && !occurs(rhs, lhs)) {
+        return false;
+    }
+#endif
     if (depth(lhs) > depth(rhs)) {
         return true;
     }
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index b9bb54f0d..898eb5ed7 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -105,7 +105,7 @@ namespace smt {
 
     dyn_ack_manager::dyn_ack_manager(context & ctx, dyn_ack_params & p):
         m_context(ctx),
-        m_manager(ctx.get_manager()),
+        m(ctx.get_manager()),
         m_params(p) {
     }
 
@@ -115,12 +115,9 @@ namespace smt {
     }
 
     void dyn_ack_manager::reset_app_pairs() {
-        svector<app_pair>::iterator it  = m_app_pairs.begin();
-        svector<app_pair>::iterator end = m_app_pairs.end();
-        for (; it != end; ++it) {
-            app_pair & p = *it;
-            m_manager.dec_ref(p.first);
-            m_manager.dec_ref(p.second);
+        for (app_pair& p : m_app_pairs) {
+            m.dec_ref(p.first);
+            m.dec_ref(p.second);
         }
         m_app_pairs.reset();
     }
@@ -144,22 +141,24 @@ namespace smt {
         SASSERT(n1->get_decl() == n2->get_decl());
         SASSERT(n1->get_num_args() == n2->get_num_args());
         SASSERT(n1 != n2);
-        if (m_manager.is_eq(n1))
+        if (m.is_eq(n1)) {
             return;
+        }
         if (n1->get_id() > n2->get_id())
             std::swap(n1,n2);
         app_pair p(n1, n2);
-        if (m_instantiated.contains(p))
+        if (m_instantiated.contains(p)) {
             return;
+        }
         unsigned num_occs = 0;
         if (m_app_pair2num_occs.find(n1, n2, num_occs)) {
-            TRACE("dyn_ack", tout << "used_cg_eh:\n" << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\nnum_occs: " << num_occs << "\n";);
+            TRACE("dyn_ack", tout << "used_cg_eh:\n" << mk_pp(n1, m) << "\n" << mk_pp(n2, m) << "\nnum_occs: " << num_occs << "\n";);
             num_occs++;
         }
         else {
             num_occs = 1;
-            m_manager.inc_ref(n1);
-            m_manager.inc_ref(n2);
+            m.inc_ref(n1);
+            m.inc_ref(n2);
             m_app_pairs.push_back(p);
         }
         SASSERT(num_occs > 0);
@@ -169,34 +168,35 @@ namespace smt {
         SASSERT(m_app_pair2num_occs.find(n1, n2, num_occs2) && num_occs == num_occs2);
 #endif
         if (num_occs == m_params.m_dack_threshold) {
-            TRACE("dyn_ack", tout << "found candidate:\n" << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\nnum_occs: " << num_occs << "\n";);
+            TRACE("dyn_ack", tout << "found candidate:\n" << mk_pp(n1, m) << "\n" << mk_pp(n2, m) << "\nnum_occs: " << num_occs << "\n";);
             m_to_instantiate.push_back(p);
         }
     }
 
     void dyn_ack_manager::eq_eh(app * n1, app * n2, app* r) {
-        if (n1 == n2 || r == n1 || r == n2 || m_manager.is_bool(n1)) {
+        if (n1 == n2 || r == n1 || r == n2 || m.is_bool(n1)) {
             return;
         }
         if (n1->get_id() > n2->get_id())
             std::swap(n1,n2);
         TRACE("dyn_ack", 
-              tout << mk_pp(n1, m_manager) << " = " << mk_pp(n2, m_manager) 
-              << " = " << mk_pp(r, m_manager) << "\n";);
+              tout << mk_pp(n1, m) << " = " << mk_pp(n2, m) 
+              << " = " << mk_pp(r, m) << "\n";);
         app_triple tr(n1, n2, r);
-        if (m_triple.m_instantiated.contains(tr))
+        if (m_triple.m_instantiated.contains(tr)) {
             return;
+        }
         unsigned num_occs = 0;
         if (m_triple.m_app2num_occs.find(n1, n2, r, num_occs)) {
-            TRACE("dyn_ack", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) 
-                  << mk_pp(r, m_manager) << "\n" << "\nnum_occs: " << num_occs << "\n";);
+            TRACE("dyn_ack", tout << mk_pp(n1, m) << "\n" << mk_pp(n2, m) 
+                  << mk_pp(r, m) << "\n" << "\nnum_occs: " << num_occs << "\n";);
             num_occs++;
         }
         else {
             num_occs = 1;
-            m_manager.inc_ref(n1);
-            m_manager.inc_ref(n2);
-            m_manager.inc_ref(r);
+            m.inc_ref(n1);
+            m.inc_ref(n2);
+            m.inc_ref(r);
             m_triple.m_apps.push_back(tr);
         }
         SASSERT(num_occs > 0);
@@ -206,8 +206,8 @@ namespace smt {
         SASSERT(m_triple.m_app2num_occs.find(n1, n2, r, num_occs2) && num_occs == num_occs2);
 #endif
         if (num_occs == m_params.m_dack_threshold) {
-            TRACE("dyn_ack", tout << "found candidate:\n" << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) 
-                  << "\n" << mk_pp(r, m_manager) 
+            TRACE("dyn_ack", tout << "found candidate:\n" << mk_pp(n1, m) << "\n" << mk_pp(n2, m) 
+                  << "\n" << mk_pp(r, m) 
                   << "\nnum_occs: " << num_occs << "\n";);
             m_triple.m_to_instantiate.push_back(tr);
         }
@@ -245,9 +245,9 @@ namespace smt {
         for (; it != end; ++it) {
             app_pair & p = *it;
             if (m_instantiated.contains(p)) {
-                TRACE("dyn_ack", tout << "1) erasing:\n" << mk_pp(p.first, m_manager) << "\n" << mk_pp(p.second, m_manager) << "\n";);
-                m_manager.dec_ref(p.first);
-                m_manager.dec_ref(p.second);
+                TRACE("dyn_ack", tout << "1) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
+                m.dec_ref(p.first);
+                m.dec_ref(p.second);
                 SASSERT(!m_app_pair2num_occs.contains(p.first, p.second));
                 continue;
             }
@@ -261,10 +261,10 @@ namespace smt {
             num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
             if (num_occs <= 1) {
                 num_deleted++;
-                TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m_manager) << "\n" << mk_pp(p.second, m_manager) << "\n";);
+                TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
                 m_app_pair2num_occs.erase(p.first, p.second);
-                m_manager.dec_ref(p.first);
-                m_manager.dec_ref(p.second);
+                m.dec_ref(p.first);
+                m.dec_ref(p.second);
                 continue;
             }
             *it2 = p;
@@ -283,20 +283,19 @@ namespace smt {
     }
 
     class dyn_ack_clause_del_eh : public clause_del_eh {
-        dyn_ack_manager & m_manager;
+        dyn_ack_manager & m;
     public:
         dyn_ack_clause_del_eh(dyn_ack_manager & m):
-            m_manager(m) {
+            m(m) {
         }
         ~dyn_ack_clause_del_eh() override {}
-        void operator()(ast_manager & m, clause * cls) override {
-            m_manager.del_clause_eh(cls);
+        void operator()(ast_manager & _m, clause * cls) override {
+            m.del_clause_eh(cls);
             dealloc(this);
         }
     };
 
     void dyn_ack_manager::del_clause_eh(clause * cls) {
-        TRACE("dyn_ack", tout << "del_clause_eh: "; m_context.display_clause(tout, cls); tout << "\n";);
         m_context.m_stats.m_num_del_dyn_ack++;
         
         app_pair p((app*)nullptr,(app*)nullptr);
@@ -342,7 +341,7 @@ namespace smt {
         app * eq  = m_context.mk_eq_atom(n1, n2);
         m_context.internalize(eq, true);
         literal l = m_context.get_literal(eq);
-        TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m_manager) << "\nliteral: "; 
+        TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: "; 
               m_context.display_literal(tout, l); tout << "\n";);
         return l;
     }
@@ -354,7 +353,7 @@ namespace smt {
         SASSERT(n1 != n2);
         m_context.m_stats.m_num_dyn_ack++;
         TRACE("dyn_ack_inst", tout << "dyn_ack: " << n1->get_id() << " " << n2->get_id() << "\n";);
-        TRACE("dyn_ack", tout << "expanding Ackermann's rule for:\n" << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n";);
+        TRACE("dyn_ack", tout << "expanding Ackermann's rule for:\n" << mk_pp(n1, m) << "\n" << mk_pp(n2, m) << "\n";);
         unsigned num_args = n1->get_num_args();
         literal_buffer lits;
         for (unsigned i = 0; i < num_args; i++) {
@@ -372,7 +371,7 @@ namespace smt {
         clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
 
         justification * js = nullptr;
-        if (m_manager.proofs_enabled())
+        if (m.proofs_enabled())
             js = alloc(dyn_ack_justification, n1, n2);
         clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
@@ -392,13 +391,10 @@ namespace smt {
     }
 
     void dyn_ack_manager::reset_app_triples() {
-        svector<app_triple>::iterator it  = m_triple.m_apps.begin();
-        svector<app_triple>::iterator end = m_triple.m_apps.end();
-        for (; it != end; ++it) {
-            app_triple & p = *it;
-            m_manager.dec_ref(p.first);
-            m_manager.dec_ref(p.second);
-            m_manager.dec_ref(p.third);
+        for (app_triple& p : m_triple.m_apps) {
+            m.dec_ref(p.first);
+            m.dec_ref(p.second);
+            m.dec_ref(p.third);
         }
         m_triple.m_apps.reset();
     }
@@ -408,9 +404,9 @@ namespace smt {
         SASSERT(n1 != n2 && n1 != r && n2 != r);
         m_context.m_stats.m_num_dyn_ack++;
         TRACE("dyn_ack_inst", tout << "dyn_ack: " << n1->get_id() << " " << n2->get_id() << " " << r->get_id() << "\n";);
-        TRACE("dyn_ack", tout << "expanding Ackermann's rule for:\n" << mk_pp(n1, m_manager) << "\n" 
-              << mk_pp(n2, m_manager) << "\n"
-              << mk_pp(r,  m_manager) << "\n";
+        TRACE("dyn_ack", tout << "expanding Ackermann's rule for:\n" << mk_pp(n1, m) << "\n" 
+              << mk_pp(n2, m) << "\n"
+              << mk_pp(r,  m) << "\n";
               );
         app_triple tr(n1, n2, r);
         SASSERT(m_triple.m_app2num_occs.contains(n1, n2, r));
@@ -424,7 +420,7 @@ namespace smt {
         clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
 
         justification * js = nullptr;
-        if (m_manager.proofs_enabled())
+        if (m.proofs_enabled())
             js = alloc(dyn_ack_justification, n1, n2);
         clause * cls = m_context.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
         if (!cls) {
@@ -467,10 +463,10 @@ namespace smt {
         for (; it != end; ++it) {
             app_triple & p = *it;
             if (m_triple.m_instantiated.contains(p)) {
-                TRACE("dyn_ack", tout << "1) erasing:\n" << mk_pp(p.first, m_manager) << "\n" << mk_pp(p.second, m_manager) << "\n";);
-                m_manager.dec_ref(p.first);
-                m_manager.dec_ref(p.second);
-                m_manager.dec_ref(p.third);
+                TRACE("dyn_ack", tout << "1) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
+                m.dec_ref(p.first);
+                m.dec_ref(p.second);
+                m.dec_ref(p.third);
                 SASSERT(!m_triple.m_app2num_occs.contains(p.first, p.second, p.third));
                 continue;
             }
@@ -484,11 +480,11 @@ namespace smt {
             num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
             if (num_occs <= 1) {
                 num_deleted++;
-                TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m_manager) << "\n" << mk_pp(p.second, m_manager) << "\n";);
+                TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
                 m_triple.m_app2num_occs.erase(p.first, p.second, p.third);
-                m_manager.dec_ref(p.first);
-                m_manager.dec_ref(p.second);
-                m_manager.dec_ref(p.third);
+                m.dec_ref(p.first);
+                m.dec_ref(p.second);
+                m.dec_ref(p.third);
                 continue;
             }
             *it2 = p;
@@ -509,10 +505,8 @@ namespace smt {
 
 #ifdef Z3DEBUG
     bool dyn_ack_manager::check_invariant() const {
-        clause2app_pair::iterator it  = m_clause2app_pair.begin();
-        clause2app_pair::iterator end = m_clause2app_pair.end();
-        for (; it != end; ++it) {
-            app_pair const & p = it->get_value();
+        for (auto const& kv : m_clause2app_pair) {
+            app_pair const & p = kv.get_value();
             SASSERT(m_instantiated.contains(p));
             SASSERT(!m_app_pair2num_occs.contains(p.first, p.second));
         }
diff --git a/src/smt/dyn_ack.h b/src/smt/dyn_ack.h
index 9986dd498..0f8ae024a 100644
--- a/src/smt/dyn_ack.h
+++ b/src/smt/dyn_ack.h
@@ -44,7 +44,7 @@ namespace smt {
         typedef obj_map<clause, app_triple>         clause2app_triple;
 
         context &                                  m_context;
-        ast_manager &                              m_manager;
+        ast_manager &                              m;
         dyn_ack_params &                           m_params;
         app_pair2num_occs                          m_app_pair2num_occs;
         app_pair_vector                            m_app_pairs;
diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp
index 409827d43..4aee1f98c 100644
--- a/src/smt/smt_clause.cpp
+++ b/src/smt/smt_clause.cpp
@@ -123,7 +123,7 @@ namespace smt {
             if (lit.sign()) args[args.size()-1] = m.mk_not(args.back());
         }
         expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m);
-        return out << disj;
+        return out << mk_bounded_pp(disj, m, 3);
     }
 
 };
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index d863ca544..17a367b0b 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -16,10 +16,11 @@ Author:
 Revision History:
 
 --*/
-#include "smt/smt_context.h"
-#include "smt/smt_conflict_resolution.h"
+
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "smt/smt_context.h"
+#include "smt/smt_conflict_resolution.h"
 
 namespace smt {
 
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 259b3ccf4..3a25e5f52 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -27,12 +27,12 @@ Revision History:
 namespace smt {
 
     expr_ref context::antecedent2fml(index_set const& vars) {
-        expr_ref_vector premises(m_manager);
+        expr_ref_vector premises(m);
         index_set::iterator it = vars.begin(), end = vars.end();
         for (; it != end; ++it) {
             expr* e =  bool_var2expr(*it);
             e = m_assumption2orig.find(e);
-            premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e));
+            premises.push_back(get_assignment(*it) != l_false ? e : m.mk_not(e));
         }
         return mk_and(premises);
     }
@@ -47,7 +47,6 @@ namespace smt {
     // - e is a data-type recognizer of a variable that is to be fixed.
     // 
     void context::extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq) {
-        ast_manager& m = m_manager;
         datatype_util dt(m);
         expr* e1, *e2;       
         expr_ref fml(m);        
@@ -103,7 +102,6 @@ namespace smt {
     }
 
     void context::justify(literal lit, index_set& s) {
-        ast_manager& m = m_manager;
         (void)m;
         b_justification js = get_justification(lit.var());
         switch (js.get_kind()) {
@@ -163,7 +161,6 @@ namespace smt {
     // 
 
     unsigned context::delete_unfixed(expr_ref_vector& unfixed) {
-        ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
         obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
         for (; it != end; ++it) {
@@ -216,7 +213,6 @@ namespace smt {
     // 
     unsigned context::extract_fixed_eqs(expr_ref_vector& conseq) {
         TRACE("context", tout << "extract fixed consequences\n";);
-        ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
         expr_ref fml(m), eq(m);
         obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
@@ -253,7 +249,6 @@ namespace smt {
     }
 
     literal context::mk_diseq(expr* e, expr* val) {
-        ast_manager& m = m_manager;
         if (m.is_bool(e) && b_internalized(e)) {
             return literal(get_bool_var(e), m.is_true(val));
         }
@@ -276,7 +271,6 @@ namespace smt {
         m_antecedents.reset();
         m_antecedents.insert(true_literal.var(), index_set());
         pop_to_base_lvl();
-        ast_manager& m = m_manager;
         expr_ref_vector vars(m), assumptions(m);
         m_var2val.reset();
         m_var2orig.reset();
@@ -459,7 +453,7 @@ namespace smt {
             }
             m_antecedents.insert(lit.var(), s);
             if (_nasms.contains(lit.index())) {
-                expr_ref_vector core(m_manager);
+                expr_ref_vector core(m);
                 index_set::iterator it = s.begin(), end = s.end();
                 for (; it != end; ++it) {
                     core.push_back(var2expr[*it]);
@@ -528,7 +522,7 @@ namespace smt {
         unsigned num_restarts = 0;
 
         while (true) {
-            if (m_manager.canceled()) {
+            if (m.canceled()) {
                 is_sat = l_undef;
                 break;
             }
@@ -581,10 +575,10 @@ namespace smt {
     lbool context::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
         unsigned_vector ps;
         max_cliques<neg_literal> mc;
-        expr_ref lit(m_manager);
+        expr_ref lit(m);
         for (unsigned i = 0; i < vars.size(); ++i) {
             expr* n = vars[i];
-            bool neg = m_manager.is_not(n, n);
+            bool neg = m.is_not(n, n);
             if (b_internalized(n)) {
                 ps.push_back(literal(get_bool_var(n), neg).index());
             }
@@ -602,7 +596,7 @@ namespace smt {
         vector<unsigned_vector> _mutexes;
         mc.cliques(ps, _mutexes);
         for (unsigned i = 0; i < _mutexes.size(); ++i) {
-            expr_ref_vector lits(m_manager);
+            expr_ref_vector lits(m);
             for (unsigned j = 0; j < _mutexes[i].size(); ++j) {
                 literal2expr(to_literal(_mutexes[i][j]), lit);
                 lits.push_back(lit);
@@ -618,7 +612,6 @@ namespace smt {
     // 
     void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                         expr_ref_vector const& conseq, expr_ref_vector const& unfixed) {
-        ast_manager& m = m_manager;
         expr_ref tmp(m);
         SASSERT(!inconsistent());
         for (unsigned i = 0; i < conseq.size(); ++i) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index de90df979..d47e8dde3 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -17,32 +17,32 @@ Revision History:
 
 --*/
 #include<math.h>
-#include "smt/smt_context.h"
 #include "util/luby.h"
+#include "util/warning.h"
+#include "util/timeit.h"
+#include "util/union_find.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
-#include "util/warning.h"
-#include "smt/smt_quick_checker.h"
-#include "ast/proofs/proof_checker.h"
-#include "ast/ast_util.h"
-#include "smt/uses_theory.h"
-#include "model/model.h"
-#include "smt/smt_for_each_relevant_expr.h"
-#include "util/timeit.h"
-#include "ast/well_sorted.h"
-#include "util/union_find.h"
-#include "smt/smt_model_generator.h"
-#include "smt/smt_model_checker.h"
-#include "smt/smt_model_finder.h"
-#include "model/model_pp.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_translation.h"
 #include "ast/recfun_decl_plugin.h"
+#include "ast/proofs/proof_checker.h"
+#include "ast/ast_util.h"
+#include "ast/well_sorted.h"
+#include "model/model.h"
+#include "model/model_pp.h"
+#include "smt/smt_context.h"
+#include "smt/smt_quick_checker.h"
+#include "smt/uses_theory.h"
+#include "smt/smt_for_each_relevant_expr.h"
+#include "smt/smt_model_generator.h"
+#include "smt/smt_model_checker.h"
+#include "smt/smt_model_finder.h"
 
 namespace smt {
 
     context::context(ast_manager & m, smt_params & p, params_ref const & _p):
-        m_manager(m),
+        m(m),
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
@@ -63,9 +63,8 @@ namespace smt {
         m_final_check_idx(0),
         m_is_auxiliary(false),
         m_cg_table(m),
-        m_dyn_ack_manager(*this, p),
         m_is_diseq_tmp(nullptr),
-        m_units_to_reassert(m_manager),
+        m_units_to_reassert(m),
         m_qhead(0),
         m_simp_qhead(0),
         m_simp_counter(0),
@@ -77,6 +76,7 @@ namespace smt {
         m_not_l(null_literal),
         m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
         m_unsat_proof(m),
+        m_dyn_ack_manager(*this, p),
         m_unknown("unknown"),
         m_unsat_core(m),
 #ifdef Z3DEBUG
@@ -139,7 +139,7 @@ namespace smt {
     */
 
     bool context::get_cancel_flag() {
-        return !m_manager.limit().inc();
+        return !m.limit().inc();
     }
 
     void context::updt_params(params_ref const& p) {
@@ -246,7 +246,7 @@ namespace smt {
     }
 
     context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
-        context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa);
+        context * new_ctx = alloc(context, m, p ? *p : m_fparams, pa);
         new_ctx->m_is_auxiliary = true;
         new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
         copy_plugins(*this, *new_ctx);
@@ -254,14 +254,14 @@ namespace smt {
     }
 
     void context::init() {
-        app * t       = m_manager.mk_true();
+        app * t       = m.mk_true();
         mk_bool_var(t);
         SASSERT(get_bool_var(t) == true_bool_var);
         SASSERT(true_literal.var() == true_bool_var);
         m_assignment[true_literal.index()]     = l_true;
         m_assignment[false_literal.index()]    = l_false;
-        if (m_manager.proofs_enabled()) {
-            proof * pr = m_manager.mk_true_proof();
+        if (m.proofs_enabled()) {
+            proof * pr = m.mk_true_proof();
 
             set_justification(true_bool_var, m_bdata[true_bool_var], b_justification(mk_justification(justification_proof_wrapper(*this, pr))));
         }
@@ -271,7 +271,7 @@ namespace smt {
         m_true_enode  = mk_enode(t, true, true, false);
         // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
         // m_true_enode->mark_as_interpreted();
-        app * f       = m_manager.mk_false();
+        app * f       = m.mk_false();
         m_false_enode = mk_enode(f, true, true, false);
         // m_false_enode->mark_as_interpreted();
     }
@@ -286,13 +286,13 @@ namespace smt {
        See comments in theory::mk_eq_atom
     */
     app * context::mk_eq_atom(expr * lhs, expr * rhs) {
-        family_id fid = m_manager.get_sort(lhs)->get_family_id();
+        family_id fid = m.get_sort(lhs)->get_family_id();
         theory * th   = get_theory(fid);
         if (th)
             return th->mk_eq_atom(lhs, rhs);
         if (lhs->get_id() > rhs->get_id())
             std::swap(lhs, rhs);
-        return m_manager.mk_eq(lhs, rhs);
+        return m.mk_eq(lhs, rhs);
     }
 
     void context::set_justification(bool_var v, bool_var_data& d, b_justification const& j) {
@@ -324,7 +324,7 @@ namespace smt {
         if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
             m_atom_propagation_queue.push_back(l);
 
-        if (m_manager.has_trace_stream())
+        if (m.has_trace_stream())
             trace_assign(l, j, decision);
 
         m_case_split_queue->assign_lit_eh(l);
@@ -438,7 +438,7 @@ namespace smt {
                             expr * e = bool_var2expr(first_lit.var());
                             // IMPORTANT: this kind of propagation asserts negative literals of the form (= A1 A2) where
                             // A1 and A2 are array terms. So, it may be interesting to disable it for array eqs.
-                            //if (!(m_manager.is_eq(e) && m_manager.get_sort(to_app(e)->get_arg(0))->get_family_id() == m_manager.get_family_id("array")))
+                            //if (!(m.is_eq(e) && m.get_sort(to_app(e)->get_arg(0))->get_family_id() == m.get_family_id("array")))
                             mark_as_relevant(e);
                         }
                     }
@@ -502,7 +502,7 @@ namespace smt {
     */
     void context::add_eq(enode * n1, enode * n2, eq_justification js) {
         unsigned old_trail_size = m_trail_stack.size();
-        scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
+        scoped_suspend_rlimit _suspend_cancel(m.limit());
 
         try {
             TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
@@ -543,7 +543,7 @@ namespace smt {
             // It is necessary to propagate relevancy to other elements of
             // the equivalence class. This is necessary to enforce the invariant
             // in the field m_parent of the enode class.
-            if (is_relevant(r1)) { // && !m_manager.is_eq(r1->get_owner())) !is_eq HACK
+            if (is_relevant(r1)) { // && !m.is_eq(r1->get_owner())) !is_eq HACK
                 // NOTE for !is_eq HACK... the !is_eq HACK does not propagate relevancy when two
                 // equality enodes are congruent. I tested this optimization because in V1
                 // relevancy is not propagated for congruent equalities.
@@ -553,7 +553,7 @@ namespace smt {
                 // To use it, I need to go over the code and analyze all affected places.
                 mark_as_relevant(r2);
             }
-            else if (is_relevant(r2)) { // && !m_manager.is_eq(r2->get_owner())) { // !is_eq HACK
+            else if (is_relevant(r2)) { // && !m.is_eq(r2->get_owner())) { // !is_eq HACK
                 mark_as_relevant(r1);
             }
 
@@ -602,7 +602,7 @@ namespace smt {
         catch (...) {
             // Restore trail size since procedure was interrupted in the middle.
             // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
-            TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";);
+            TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m.limit().get_cancel_flag() << "\n";);
             m_trail_stack.shrink(old_trail_size);
             throw;
         }
@@ -617,7 +617,7 @@ namespace smt {
         for (enode * parent : enode::parents(r1)) {
             CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && parent->is_true_eq() && m_cg_table.contains_ptr(parent), tout << parent->get_owner_id() << "\n";);
             CTRACE("add_eq", !parent->is_marked() && parent->is_cgc_enabled() && !parent->is_true_eq() &&  parent->is_cgr() && !m_cg_table.contains_ptr(parent), 
-                   tout << "cgr !contains " << parent->get_owner_id() << " " << mk_pp(parent->get_decl(), m_manager) << "\n";
+                   tout << "cgr !contains " << parent->get_owner_id() << " " << mk_pp(parent->get_decl(), m) << "\n";
                    for (enode* n : enode::args(parent))  tout << n->get_root()->get_owner_id() << " " << n->get_root()->hash() << " ";
                    tout << "\n";
                    tout << "contains: " << m_cg_table.contains(parent) << "\n";
@@ -1085,10 +1085,10 @@ namespace smt {
         enode * r1 = n1->get_root();
         enode * r2 = n2->get_root();
         TRACE("add_diseq", tout << "assigning: #" << n1->get_owner_id() << " != #" << n2->get_owner_id() << "\n";
-              tout << mk_ll_pp(n1->get_owner(), m_manager) << " != ";
-              tout << mk_ll_pp(n2->get_owner(), m_manager) << "\n";
-              tout << mk_ll_pp(r1->get_owner(), m_manager) << " != ";
-              tout << mk_ll_pp(r2->get_owner(), m_manager) << "\n";
+              tout << mk_ll_pp(n1->get_owner(), m) << " != ";
+              tout << mk_ll_pp(n2->get_owner(), m) << "\n";
+              tout << mk_ll_pp(r1->get_owner(), m) << " != ";
+              tout << mk_ll_pp(r2->get_owner(), m) << "\n";
               );
 
         DEBUG_CODE(
@@ -1126,7 +1126,7 @@ namespace smt {
                 theory_id  t1 = l1->get_th_id();
                 theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : l1->get_th_var();
                 theory * th   = get_theory(t1);
-                TRACE("add_diseq", tout << m_manager.get_family_name(t1) << "\n";);
+                TRACE("add_diseq", tout << m.get_family_name(t1) << "\n";);
                 if (th->use_diseqs()) {
                     theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t1) : r2->get_th_var(t1);
                     if (v2 != null_theory_var)
@@ -1143,17 +1143,17 @@ namespace smt {
        context.
     */
     bool context::is_diseq(enode * n1, enode * n2) const {
-        SASSERT(m_manager.get_sort(n1->get_owner()) == m_manager.get_sort(n2->get_owner()));
+        SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner()));
         context * _this = const_cast<context*>(this);
         if (!m_is_diseq_tmp) {
-            app * eq       = m_manager.mk_eq(n1->get_owner(), n2->get_owner());
-            m_manager.inc_ref(eq);
-            _this->m_is_diseq_tmp = enode::mk_dummy(m_manager, m_app2enode, eq);
+            app * eq       = m.mk_eq(n1->get_owner(), n2->get_owner());
+            m.inc_ref(eq);
+            _this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
         }
-        else if (m_manager.get_sort(m_is_diseq_tmp->get_owner()->get_arg(0)) != m_manager.get_sort(n1->get_owner())) {
-            m_manager.dec_ref(m_is_diseq_tmp->get_owner());
-            app * eq = m_manager.mk_eq(n1->get_owner(), n2->get_owner());
-            m_manager.inc_ref(eq);
+        else if (m.get_sort(m_is_diseq_tmp->get_owner()->get_arg(0)) != m.get_sort(n1->get_owner())) {
+            m.dec_ref(m_is_diseq_tmp->get_owner());
+            app * eq = m.mk_eq(n1->get_owner(), n2->get_owner());
+            m.inc_ref(eq);
             m_is_diseq_tmp->m_func_decl_id = UINT_MAX;
             m_is_diseq_tmp->m_owner = eq;
         }
@@ -1278,13 +1278,11 @@ namespace smt {
                 if (!p2->is_cgr())
                     continue;
                 list<enode*> * ps = table.find(p2);
-                if (ps) {
-                    while (ps) {
-                        enode * p1 = ps->head();
-                        if (p1->get_root() != p2->get_root() && is_ext_diseq(p1, p2, depth - 1))
-                            return true;
-                        ps = ps->tail();
-                    }
+                while (ps) {
+                    enode * p1 = ps->head();
+                    if (p1->get_root() != p2->get_root() && is_ext_diseq(p1, p2, depth - 1))
+                        return true;
+                    ps = ps->tail();
                 }
             }
         }
@@ -1361,10 +1359,10 @@ namespace smt {
                 return false;
             if (d.is_eq()) {
                 app * n   = to_app(m_bool_var2expr[v]);
-                SASSERT(m_manager.is_eq(n));
+                SASSERT(m.is_eq(n));
                 expr * lhs = n->get_arg(0);
                 expr * rhs = n->get_arg(1);
-                if (m_manager.is_bool(lhs)) {
+                if (m.is_bool(lhs)) {
                     // no-op
                 }
                 else if (val == l_true) {
@@ -1389,7 +1387,7 @@ namespace smt {
                 // becomes an unit-clause and the remaining literal is the negation of a quantifier.
                 CTRACE("assign_quantifier_bug", get_assignment(v) != l_true,
                        tout << "#" << bool_var2expr(v)->get_id() << " val: " << get_assignment(v) << "\n";
-                       tout << mk_pp(bool_var2expr(v), m_manager) << "\n";
+                       tout << mk_pp(bool_var2expr(v), m) << "\n";
                        display(tout););
                 SASSERT(is_quantifier(m_bool_var2expr[v]));
                 if (get_assignment(v) == l_true) {
@@ -1468,7 +1466,7 @@ namespace smt {
     */
     void context::push_new_th_diseqs(enode * r, theory_var v, theory * th) {
         if (!th->use_diseqs()) {
-            TRACE("push_new_th_diseqs", tout << m_manager.get_family_name(th->get_id()) << " not using diseqs\n";);
+            TRACE("push_new_th_diseqs", tout << m.get_family_name(th->get_id()) << " not using diseqs\n";);
             return;
         }
         TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " v" << v << "\n";);
@@ -1515,7 +1513,7 @@ namespace smt {
        \pre The expression must be attached to a boolean variable.
     */
     inline lbool context::get_assignment_core(expr * n) const {
-        CTRACE("get_assignment_bug", !b_internalized(n), tout << "n:\n" << mk_pp(n, m_manager) << "\n"; display(tout););
+        CTRACE("get_assignment_bug", !b_internalized(n), tout << "n:\n" << mk_pp(n, m) << "\n"; display(tout););
         SASSERT(b_internalized(n));
         unsigned id  = n->get_id();
         bool_var var = get_bool_var_of_id(id);
@@ -1529,19 +1527,19 @@ namespace smt {
        is inspected instead.
     */
     lbool context::get_assignment(expr * n) const {
-        if (m_manager.is_false(n))
+        if (m.is_false(n))
             return l_false;
         expr* arg = nullptr;
-        if (m_manager.is_not(n, arg))
+        if (m.is_not(n, arg))
             return ~get_assignment_core(arg);
         return get_assignment_core(n);
     }
 
     lbool context::find_assignment(expr * n) const {
-        if (m_manager.is_false(n))
+        if (m.is_false(n))
             return l_false;
         expr* arg = nullptr;
-        if (m_manager.is_not(n, arg)) {
+        if (m.is_not(n, arg)) {
             if (b_internalized(arg))
                 return ~get_assignment_core(arg);
             return l_undef;
@@ -1557,12 +1555,12 @@ namespace smt {
     */
     lbool context::get_assignment(enode * n) const {
         expr * owner = n->get_owner();
-        if (!m_manager.is_bool(owner))
+        if (!m.is_bool(owner))
             return l_undef;
         if (n == m_false_enode)
             return l_false;
         bool_var v = get_bool_var_of_id(owner->get_id());
-        CTRACE("missing_propagation", v == null_bool_var, tout << mk_pp(owner, m_manager) << "\n";);
+        CTRACE("missing_propagation", v == null_bool_var, tout << mk_pp(owner, m) << "\n";);
         return get_assignment(v);
     }
 
@@ -1571,7 +1569,7 @@ namespace smt {
     */
     void context::get_assignments(expr_ref_vector& assignments) {
         for (literal lit : m_assigned_literals) {
-            expr_ref e(m_manager);
+            expr_ref e(m);
             literal2expr(lit, e);
             assignments.push_back(std::move(e));
         }
@@ -1590,7 +1588,7 @@ namespace smt {
                     m_atom_propagation_queue.push_back(literal(v, val == l_false));
             }
         }
-        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";);
+        TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m) << " " << m_scope_lvl << "\n";);
         m_case_split_queue->relevant_eh(n);
 
         if (is_app(n)) {
@@ -1602,7 +1600,7 @@ namespace smt {
 
             theory * propagated_th = nullptr;
             family_id fid = to_app(n)->get_family_id();
-            if (fid != m_manager.get_basic_family_id()) {
+            if (fid != m.get_basic_family_id()) {
                 theory * th = get_theory(fid);
                 if (th != nullptr) {
                     th->relevant_eh(to_app(n));
@@ -1712,7 +1710,7 @@ namespace smt {
                 return false;
             unsigned qhead = m_qhead;
             {
-                scoped_suspend_rlimit _suspend_cancel(m_manager.limit(), at_base_level());
+                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
                 if (!bcp())
                     return false;
                 if (!propagate_th_case_split(qhead))
@@ -1733,7 +1731,7 @@ namespace smt {
                     return false;
             }
             if (!get_cancel_flag()) {
-                scoped_suspend_rlimit _suspend_cancel(m_manager.limit(), at_base_level());
+                scoped_suspend_rlimit _suspend_cancel(m.limit(), at_base_level());
                 m_qmanager->propagate();
             }
             if (inconsistent())
@@ -1759,7 +1757,7 @@ namespace smt {
     }
 
     void context::assign_quantifier(quantifier * q) {
-        TRACE("assumption", tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("assumption", tout << mk_pp(q, m) << "\n";);
         m_qmanager->assign_eh(q);
     }
 
@@ -1821,7 +1819,7 @@ namespace smt {
         push_scope();
         TRACE("decide", tout << "splitting, lvl: " << m_scope_lvl << "\n";);
 
-        TRACE("decide_detail", tout << mk_pp(bool_var2expr(var), m_manager) << "\n";);
+        TRACE("decide_detail", tout << mk_pp(bool_var2expr(var), m) << "\n";);
 
         bool is_pos;
 
@@ -1920,8 +1918,8 @@ namespace smt {
     */
     void context::push_scope() {
 
-        if (m_manager.has_trace_stream() && !m_is_auxiliary)
-            m_manager.trace_stream() << "[push] " << m_scope_lvl << "\n";
+        if (m.has_trace_stream() && !m_is_auxiliary)
+            m.trace_stream() << "[push] " << m_scope_lvl << "\n";
 
         m_scope_lvl++;
         m_region.push_scope();
@@ -2001,7 +1999,7 @@ namespace smt {
         CTRACE("context", !m_flushing, display_clause_smt2(tout << "deleting ", *cls) << "\n";);
         if (!cls->deleted())
             remove_cls_occs(cls);
-        cls->deallocate(m_manager);
+        cls->deallocate(m);
         m_stats.m_num_del_clause++;
     }
 
@@ -2054,7 +2052,7 @@ namespace smt {
         while (i != old_lim) {
             --i;
             justification * js = justifications[i];
-            js->del_eh(m_manager);
+            js->del_eh(m);
             if (!js->in_region()) {
                 dealloc(js);
             }
@@ -2219,7 +2217,7 @@ namespace smt {
             clause_vector & v = m_clauses_to_reinit[i];
             for (clause* cls : v) {
                 if (cls->deleted()) {
-                    cls->release_atoms(m_manager);
+                    cls->release_atoms(m);
                     cls->m_reinit              = false;
                     cls->m_reinternalize_atoms = false;
                     continue;
@@ -2263,7 +2261,7 @@ namespace smt {
                         // So, when reinternalizing the NOT-atom I should set the gate_ctx to false,
                         // and force expression to be reinternalized.
                         // Otherwise I set gate_ctx to true
-                        bool gate_ctx = !m_manager.is_not(atom);
+                        bool gate_ctx = !m.is_not(atom);
                         internalize(atom, gate_ctx);
                         SASSERT(b_internalized(atom));
                         bool_var v      = get_bool_var(atom);
@@ -2312,11 +2310,6 @@ namespace smt {
                     }
                 }
 
-                // SASSERT(!(cls->get_num_literals() == 3 &&
-                //          (cls->get_literal(0).index() == 624 || cls->get_literal(0).index() == 103 || cls->get_literal(0).index() == 629) &&
-                //          (cls->get_literal(1).index() == 624 || cls->get_literal(1).index() == 103 || cls->get_literal(1).index() == 629) &&
-                //          (cls->get_literal(2).index() == 624 || cls->get_literal(2).index() == 103 || cls->get_literal(2).index() == 629)));
-
                 if (keep && m_scope_lvl > m_base_lvl) {
                     m_clauses_to_reinit[m_scope_lvl].push_back(cls);
                 }
@@ -2324,7 +2317,7 @@ namespace smt {
                     // clause do not need to be in the reinit stack anymore,
                     // because it will be deleted when the base level is
                     // backtracked.
-                    cls->release_atoms(m_manager);
+                    cls->release_atoms(m);
                     cls->m_reinit              = false;
                     cls->m_reinternalize_atoms = false;
                 }
@@ -2366,8 +2359,8 @@ namespace smt {
     unsigned context::pop_scope_core(unsigned num_scopes) {
 
         try {
-            if (m_manager.has_trace_stream() && !m_is_auxiliary)
-                m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
+            if (m.has_trace_stream() && !m_is_auxiliary)
+                m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
 
             TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
             TRACE("pop_scope_detail", display(tout););
@@ -2492,7 +2485,7 @@ namespace smt {
             literal l = cls[i];
             switch(get_assignment(l)) {
             case l_false:
-                if (m_manager.proofs_enabled())
+                if (m.proofs_enabled())
                     simp_lits.push_back(~l);
                 if (lit_occs_enabled())
                     m_lit_occs[l.index()].erase(&cls);
@@ -2514,7 +2507,7 @@ namespace smt {
             SASSERT(j >= 2);
         }
 
-        if (m_manager.proofs_enabled() && !simp_lits.empty()) {
+        if (m.proofs_enabled() && !simp_lits.empty()) {
             SASSERT(m_scope_lvl == m_base_lvl);
             justification * js = cls.get_justification();
             justification * new_js = nullptr;
@@ -2561,7 +2554,7 @@ namespace smt {
                         // it is safe to replace with axiom, we are at the base level.
                         SASSERT(m_scope_lvl == m_base_lvl);
                         bool_var v0 = l0.var();
-                        if (m_manager.proofs_enabled()) {
+                        if (m.proofs_enabled()) {
                             SASSERT(m_search_lvl == m_base_lvl);
                             literal_buffer simp_lits;
                             unsigned num_lits = cls->get_num_literals();
@@ -2857,7 +2850,7 @@ namespace smt {
 
     void context::push() {
         TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););
-        scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
+        scoped_suspend_rlimit _suspend_cancel(m.limit());
         pop_to_base_lvl();
         setup_context(false);
         bool was_consistent = !inconsistent();
@@ -2902,8 +2895,8 @@ namespace smt {
         del_justifications(m_justifications, 0);
         reset_tmp_clauses();
         if (m_is_diseq_tmp) {
-            m_is_diseq_tmp->del_eh(m_manager, false);
-            m_manager.dec_ref(m_is_diseq_tmp->get_owner());
+            m_is_diseq_tmp->del_eh(m, false);
+            m.dec_ref(m_is_diseq_tmp->get_owner());
             enode::del_dummy(m_is_diseq_tmp);
             m_is_diseq_tmp = nullptr;
         }
@@ -2912,9 +2905,9 @@ namespace smt {
 
     void context::assert_expr_core(expr * e, proof * pr) {
         if (get_cancel_flag()) return;
-        SASSERT(is_well_sorted(m_manager, e));
-        TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m_manager) << "\n";);
-        TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
+        SASSERT(is_well_sorted(m, e));
+        TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m) << "\n";);
+        TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
         pop_to_base_lvl();
         if (pr == nullptr)
             m_asserted_formulas.assert_expr(e);
@@ -3027,7 +3020,7 @@ namespace smt {
                     literal l2 = *set_it;
                     if (l2 != l) {
                         b_justification js(l);
-                        TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr()););
+                        TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.c_ptr()););
                         assign(~l2, js);
                         if (inconsistent()) {
                             TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
@@ -3068,13 +3061,13 @@ namespace smt {
 
     void context::internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy) {
         for (expr* e : asms) {
-            if (is_valid_assumption(m_manager, e)) {
-                asm2proxy.push_back(std::make_pair(e, expr_ref(e, m_manager)));
+            if (is_valid_assumption(m, e)) {
+                asm2proxy.push_back(std::make_pair(e, expr_ref(e, m)));
             }
             else {
-                expr_ref proxy(m_manager), fml(m_manager);
-                proxy = m_manager.mk_fresh_const("proxy", m_manager.mk_bool_sort());
-                fml = m_manager.mk_implies(proxy, e);
+                expr_ref proxy(m), fml(m);
+                proxy = m.mk_fresh_const("proxy", m.mk_bool_sort());
+                fml = m.mk_implies(proxy, e);
                 m_asserted_formulas.assert_expr(fml);
                 asm2proxy.push_back(std::make_pair(e, proxy));
             }
@@ -3125,7 +3118,7 @@ namespace smt {
     bool context::validate_assumptions(expr_ref_vector const& asms) {
         for (expr* a : asms) {
             SASSERT(a);
-            if (!is_valid_assumption(m_manager, a)) {
+            if (!is_valid_assumption(m, a)) {
                 warning_msg("an assumption must be a propositional variable or the negation of one");
                 return false;
             }
@@ -3143,11 +3136,11 @@ namespace smt {
         clause* clausep = nullptr;
         if (lits.size() >= 2) {
             justification* js = nullptr;
-            if (m_manager.proofs_enabled()) {
+            if (m.proofs_enabled()) {
                 proof * pr = mk_clause_def_axiom(lits.size(), lits.c_ptr(), nullptr);
                 js = mk_justification(justification_proof_wrapper(*this, pr));
             }
-            clausep = clause::mk(m_manager, lits.size(), lits.c_ptr(), CLS_AUX, js);
+            clausep = clause::mk(m, lits.size(), lits.c_ptr(), CLS_AUX, js);
         }
         m_tmp_clauses.push_back(std::make_pair(clausep, lits));
     }
@@ -3215,9 +3208,9 @@ namespace smt {
             for (auto const& p: asm2proxy) {
                 expr_ref curr_assumption = p.second;
                 expr* orig_assumption = p.first;
-                if (m_manager.is_true(curr_assumption)) continue;
-                SASSERT(is_valid_assumption(m_manager, curr_assumption));
-                proof * pr = m_manager.mk_asserted(curr_assumption);
+                if (m.is_true(curr_assumption)) continue;
+                SASSERT(is_valid_assumption(m, curr_assumption));
+                proof * pr = m.mk_asserted(curr_assumption);
                 internalize_assertion(curr_assumption, pr, 0);
                 literal l = get_literal(curr_assumption);
                 if (l == true_literal)
@@ -3229,8 +3222,8 @@ namespace smt {
                 m_literal2assumption.insert(l.index(), orig_assumption);
                 // internalize_assertion marked l as relevant.
                 SASSERT(is_relevant(l));
-                TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";);
-                if (m_manager.proofs_enabled())
+                TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m) << "\n";);
+                if (m.proofs_enabled())
                     assign(l, mk_justification(justification_proof_wrapper(*this, pr)));
                 else
                     assign(l, b_justification::mk_axiom());
@@ -3283,7 +3276,7 @@ namespace smt {
                 already_found_assumptions.insert(l.index());
                 expr* orig_assumption = m_literal2assumption[l.index()];
                 m_unsat_core.push_back(orig_assumption);
-                TRACE("assumptions", tout << l << ": " << mk_pp(orig_assumption, m_manager) << "\n";);
+                TRACE("assumptions", tout << l << ": " << mk_pp(orig_assumption, m) << "\n";);
             }
         }
         reset_assumptions();
@@ -3307,8 +3300,8 @@ namespace smt {
        Return true if succeeded.
     */
     bool context::check_preamble(bool reset_cancel) {
-        if (m_manager.has_trace_stream() && !m_is_auxiliary)
-            m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";
+        if (m.has_trace_stream() && !m_is_auxiliary)
+            m.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";
 
         if (memory::above_high_watermark()) {
             m_last_search_failure = MEMOUT;
@@ -3341,7 +3334,7 @@ namespace smt {
                 if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) {
                     IF_VERBOSE(10, verbose_stream() 
                                << "invalid assignment " << (lit.sign() ? "true" : "false") 
-                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m_manager, 2) << "\n");
+                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 2) << "\n");
                 }
             }
             for (clause* cls : m_aux_clauses) {
@@ -3377,7 +3370,7 @@ namespace smt {
 
 
         internalize_assertions();
-        expr_ref_vector theory_assumptions(m_manager);
+        expr_ref_vector theory_assumptions(m);
         add_theory_assumptions(theory_assumptions);
         if (!theory_assumptions.empty()) {
             TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
@@ -3431,7 +3424,7 @@ namespace smt {
         lbool r;
         do {
             pop_to_base_lvl();
-            expr_ref_vector asms(m_manager, num_assumptions, assumptions);
+            expr_ref_vector asms(m, num_assumptions, assumptions);
             internalize_assertions();
             add_theory_assumptions(asms);                
             TRACE("unsat_core_bug", tout << asms << "\n";);        
@@ -3561,7 +3554,7 @@ namespace smt {
         }
 
         TRACE("guessed_literals",
-              expr_ref_vector guessed_lits(m_manager);
+              expr_ref_vector guessed_lits(m);
               get_guessed_literals(guessed_lits);
               tout << guessed_lits << "\n";);
         end_search();
@@ -3852,9 +3845,9 @@ namespace smt {
     }
 
     void context::check_proof(proof * pr) {
-        if (m_manager.proofs_enabled() && m_fparams.m_check_proof) {
-            proof_checker pf(m_manager);
-            expr_ref_vector side_conditions(m_manager);
+        if (m.proofs_enabled() && m_fparams.m_check_proof) {
+            proof_checker pf(m);
+            expr_ref_vector side_conditions(m);
             pf.check(pr, side_conditions);
         }
     }
@@ -3911,7 +3904,7 @@ namespace smt {
                 internalized_quantifiers() &&
                 num_lits == 1 &&
                 conflict_lvl > m_search_lvl + 1 &&
-                !m_manager.proofs_enabled() &&
+                !m.proofs_enabled() &&
                 m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;
 
             if (delay_forced_restart) {
@@ -3934,17 +3927,17 @@ namespace smt {
                       tout << l << " ";
                       display_literal(tout, l);
                       tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
-                           << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";
+                           << mk_pp(bool_var2expr(l.var()), m) << "\n";
                   });
 
-            if (m_manager.has_trace_stream() && !m_is_auxiliary) {
-                m_manager.trace_stream() << "[conflict] ";
-                display_literals(m_manager.trace_stream(), num_lits, lits);
-                m_manager.trace_stream() << "\n";
+            if (m.has_trace_stream() && !m_is_auxiliary) {
+                m.trace_stream() << "[conflict] ";
+                display_literals(m.trace_stream(), num_lits, lits);
+                m.trace_stream() << "\n";
             }
 
 #ifdef Z3DEBUG
-            expr_ref_vector expr_lits(m_manager);
+            expr_ref_vector expr_lits(m);
             svector<bool>   expr_signs;
             for (unsigned i = 0; i < num_lits; i++) {
                 literal l = lits[i];
@@ -3957,13 +3950,13 @@ namespace smt {
             }
 #endif
             proof * pr = nullptr;
-            if (m_manager.proofs_enabled()) {
+            if (m.proofs_enabled()) {
                 pr = m_conflict_resolution->get_lemma_proof();
                 // check_proof(pr);
-                TRACE("context_proof", tout << mk_ll_pp(pr, m_manager););
+                TRACE("context_proof", tout << mk_ll_pp(pr, m););
                 TRACE("context_proof_hack",
                       static ast_mark visited;
-                      ast_ll_pp(tout, m_manager, pr, visited););
+                      ast_ll_pp(tout, m, pr, visited););
             }
             // I invoke pop_scope_core instead of pop_scope because I don't want
             // to reset cached generations... I need them to rebuild the literals
@@ -3992,7 +3985,7 @@ namespace smt {
                         // For reference, here is the buggy version
                         // BEGIN BUGGY VERSION
                         // bool_var v = get_bool_var(atom);
-                        // CTRACE("resolve_conflict_crash", v == null_bool_var, tout << mk_ismt2_pp(atom, m_manager) << "\n";);
+                        // CTRACE("resolve_conflict_crash", v == null_bool_var, tout << mk_ismt2_pp(atom, m) << "\n";);
                         // SASSERT(v != null_bool_var);
                         // literal new_l   = literal(v, l.sign());
                         // END BUGGY VERSION
@@ -4012,16 +4005,16 @@ namespace smt {
                       tout << l << " ";
                       display_literal(tout, l);
                       tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
-                           << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";
+                           << mk_pp(bool_var2expr(l.var()), m) << "\n";
                   });
 #ifdef Z3DEBUG
             for (unsigned i = 0; i < num_lits; i++) {
                 literal l = lits[i];
                 if (expr_signs[i] != l.sign()) {
                     expr* real_atom;
-                    VERIFY(m_manager.is_not(expr_lits.get(i), real_atom));
+                    VERIFY(m.is_not(expr_lits.get(i), real_atom));
                     // the sign must have flipped when internalizing
-                    CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);
+                    CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m) << "\n" << mk_pp(bool_var2expr(l.var()), m) << "\n";);
                     SASSERT(real_atom == bool_var2expr(l.var()));
                 }
                 else {
@@ -4030,7 +4023,7 @@ namespace smt {
             }
 #endif
             justification * js = nullptr;
-            if (m_manager.proofs_enabled()) {
+            if (m.proofs_enabled()) {
                 js = alloc(justification_proof_wrapper, *this, pr, false);
             }
 #if 0
@@ -4047,7 +4040,7 @@ namespace smt {
                     verbose_stream() << "[sat] avg. clause size: " << ((double) total/(double) counter) << ", max: " << max << std::endl;
                     for (unsigned i = 0; i < num_lits; i++) {
                         literal l = lits[i];
-                        verbose_stream() << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";
+                        verbose_stream() << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m) << "\n";
                     }
                 }
             }
@@ -4069,7 +4062,7 @@ namespace smt {
                   for (unsigned i = 0; i < num_lits; i++) {
                       display_literal(tout, v[i]);
                       tout << "\n";
-                      v[i].display(tout, m_manager, m_bool_var2expr.c_ptr());
+                      v[i].display(tout, m, m_bool_var2expr.c_ptr());
                       tout << "\n\n";
                   }
                   tout << "\n";);
@@ -4080,7 +4073,7 @@ namespace smt {
         else if (m_fparams.m_clause_proof) {
             m_unsat_proof = m_clause_proof.get_proof();
         }
-        else if (m_manager.proofs_enabled()) {
+        else if (m.proofs_enabled()) {
             m_unsat_proof = m_conflict_resolution->get_lemma_proof();
             check_proof(m_unsat_proof);
         }
@@ -4111,7 +4104,7 @@ namespace smt {
 
     void context::get_relevant_labels(expr* cnstr, buffer<symbol> & result) {
         if (m_fparams.m_check_at_labels) {
-            check_at_labels checker(m_manager);
+            check_at_labels checker(m);
             if (cnstr && !checker.check(cnstr)) {
                 warning_msg("Boogie generated formula that can require multiple '@' labels in a counter-example");
             }
@@ -4131,7 +4124,7 @@ namespace smt {
         for (expr * curr : m_b_internalized_stack) { 
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 // if curr is a label literal, then its tags will be copied to result.
-                m_manager.is_label_lit(curr, result);
+                m.is_label_lit(curr, result);
             }
         }
     }
@@ -4147,7 +4140,7 @@ namespace smt {
         for (expr * curr : m_b_internalized_stack) {
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 lbls.reset();
-                if (m_manager.is_label_lit(curr, lbls)) {
+                if (m.is_label_lit(curr, lbls)) {
                     bool include = false;
                     if (at_lbls) {
                         // include if there is a label with the '@' sign.
@@ -4183,7 +4176,7 @@ namespace smt {
                     result.push_back(curr);
                     break;
                 case l_false:
-                    result.push_back(m_manager.mk_not(curr));
+                    result.push_back(m.mk_not(curr));
                     break;
                 default:
                     break;
@@ -4207,7 +4200,7 @@ namespace smt {
             unsigned guess_idx = s.m_assigned_literals_lim;
             literal guess      = m_assigned_literals[guess_idx];
             SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM);
-            expr_ref lit(m_manager);
+            expr_ref lit(m);
             literal2expr(guess, lit);
             result.push_back(std::move(lit));
         }
@@ -4237,11 +4230,11 @@ namespace smt {
         expr * _lhs = lhs->get_owner();
         expr * _rhs = rhs->get_owner();
         expr * eq = mk_eq_atom(_lhs, _rhs);
-        TRACE("assume_eq", tout << "creating interface eq:\n" << mk_pp(eq, m_manager) << "\n";);
-        if (m_manager.is_false(eq)) {
+        TRACE("assume_eq", tout << "creating interface eq:\n" << mk_pp(eq, m) << "\n";);
+        if (m.is_false(eq)) {
             return false;
         }
-        bool r    = false;
+        bool r = false;
         if (!b_internalized(eq)) {
             // I do not invoke internalize(eq, true), because I want to
             // mark the try_true_first flag before invoking theory::internalize_eq_eh.
@@ -4250,13 +4243,13 @@ namespace smt {
             //  (<= (- x y) 0)
             //  (>= (- y x) 0)
             // for the new equality atom (= x y).
-            if (m_manager.is_eq(eq)) {
+            if (m.is_eq(eq)) {
                 internalize_formula_core(to_app(eq), true);
                 bool_var v        = get_bool_var(eq);
                 bool_var_data & d = get_bdata(v);
                 d.set_eq_flag();
                 set_true_first_flag(v);
-                sort * s    = m_manager.get_sort(to_app(eq)->get_arg(0));
+                sort * s    = m.get_sort(to_app(eq)->get_arg(0));
                 theory * th = m_theories.get_plugin(s->get_family_id());
                 if (th)
                     th->internalize_eq_eh(to_app(eq), v);
@@ -4272,19 +4265,17 @@ namespace smt {
         bool_var_data & d = m_bdata[v];
         if (!d.try_true_first()) {
             set_true_first_flag(v);
-            r       = true;
+            r = true;
             TRACE("assume_eq", tout << "marked as ieq.\n";);
         }
         if (get_assignment(v) == l_undef) {
             TRACE("assume_eq", tout << "variable is unassigned.\n";);
-            r       = true;
+            r = true;
         }
-        if (relevancy()) {
-            if (!is_relevant(eq)) {
-                TRACE("assume_eq", tout << "marking eq as relevant.\n";);
-                mark_as_relevant(eq);
-                r   = true;
-            }
+        if (relevancy() && !is_relevant(eq)) {
+            TRACE("assume_eq", tout << "marking eq as relevant.\n";);
+            mark_as_relevant(eq);
+            r = true;
         }
         TRACE("assume_eq", tout << "variable value: " << get_assignment(v) << "\n";);
         TRACE("assume_eq", tout << "assume_eq result: " << r << "\n";);
@@ -4294,7 +4285,7 @@ namespace smt {
     bool context::is_shared(enode * n) const {
         n = n->get_root();
         unsigned num_th_vars = n->get_num_th_vars();
-        if (m_manager.is_ite(n->get_owner())) {
+        if (m.is_ite(n->get_owner())) {
             return true;
         }
         switch (num_th_vars) {
@@ -4314,7 +4305,7 @@ namespace smt {
 
             for (enode * parent : enode::parents(n)) {
                 family_id fid = parent->get_owner()->get_family_id();
-                if (fid != th_id && fid != m_manager.get_basic_family_id()) {
+                if (fid != th_id && fid != m.get_basic_family_id()) {
                     TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";);
                     return true;
                 }
@@ -4354,7 +4345,7 @@ namespace smt {
     }
 
     bool context::get_value(enode * n, expr_ref & value) {
-        sort * s      = m_manager.get_sort(n->get_owner());
+        sort * s      = m.get_sort(n->get_owner());
         family_id fid = s->get_family_id();
         theory * th   = get_theory(fid);
         if (th == nullptr)
@@ -4444,7 +4435,6 @@ namespace smt {
     }
 
     void context::add_rec_funs_to_model() {
-        ast_manager& m = m_manager;
         if (!m_model) return;
         for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
             expr* e = m_asserted_formulas.get_formula(i);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 9cec2b757..c651e933d 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -79,7 +79,7 @@ namespace smt {
 
 
     protected:
-        ast_manager &               m_manager;
+        ast_manager &               m;
         smt_params &                m_fparams;
         params_ref                  m_params;
         setup                       m_setup;
@@ -95,9 +95,7 @@ namespace smt {
         progress_callback *         m_progress_callback;
         unsigned                    m_next_progress_sample;
         clause_proof                m_clause_proof;
-
         region                      m_region;
-
         fingerprint_set             m_fingerprints;
 
         expr_ref_vector             m_b_internalized_stack; // stack of the boolean expressions already internalized.
@@ -126,7 +124,6 @@ namespace smt {
         vector<enode_vector>        m_decl2enodes;  // decl -> enode (for decls with arity > 0)
         enode_vector                m_empty_vector;
         cg_table                    m_cg_table;
-        dyn_ack_manager             m_dyn_ack_manager;
         struct new_eq {
             enode *                 m_lhs;
             enode *                 m_rhs;
@@ -201,6 +198,7 @@ namespace smt {
 
         obj_map<expr, unsigned>      m_cached_generation;
         obj_hashtable<expr>          m_cache_generation_visited;
+        dyn_ack_manager             m_dyn_ack_manager;
 
         // -----------------------------------
         //
@@ -258,7 +256,7 @@ namespace smt {
         // -----------------------------------
     public:
         ast_manager & get_manager() const {
-            return m_manager;
+            return m;
         }
 
         th_rewriter & get_rewriter() {
@@ -519,17 +517,17 @@ namespace smt {
 
         void literal2expr(literal l, expr_ref & result) const {
             if (l == true_literal)
-                result = m_manager.mk_true();
+                result = m.mk_true();
             else if (l == false_literal)
-                result = m_manager.mk_false();
+                result = m.mk_false();
             else if (l.sign())
-                result = m_manager.mk_not(bool_var2expr(l.var()));
+                result = m.mk_not(bool_var2expr(l.var()));
             else
                 result = bool_var2expr(l.var());
         }
 
         expr_ref literal2expr(literal l) const {
-            expr_ref result(m_manager);
+            expr_ref result(m);
             literal2expr(l, result);
             return result;
         }
@@ -701,7 +699,7 @@ namespace smt {
         }
 
         bool lit_internalized(expr const * n) const {
-            return m_manager.is_false(n) || (m_manager.is_not(n) ? b_internalized(to_app(n)->get_arg(0)) : b_internalized(n));
+            return m.is_false(n) || (m.is_not(n) ? b_internalized(to_app(n)->get_arg(0)) : b_internalized(n));
         }
 
         bool e_internalized(expr const * n) const {
@@ -737,7 +735,7 @@ namespace smt {
 
     public:
         bool binary_clause_opt_enabled() const {
-            return !m_manager.proofs_enabled() && m_fparams.m_binary_clause_opt;
+            return !m.proofs_enabled() && m_fparams.m_binary_clause_opt;
         }
     protected:
         bool_var_data & get_bdata(expr const * n) {
@@ -1304,7 +1302,7 @@ namespace smt {
 
         std::ostream& display_literal(std::ostream & out, literal l) const;
 
-        std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m_manager, m_bool_var2expr.c_ptr()); return out; }
+        std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m, m_bool_var2expr.c_ptr()); return out; }
 
         void display_literal_info(std::ostream & out, literal l) const;
 
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 474c44821..9972e91d1 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -191,7 +191,7 @@ namespace smt {
                     if (n->is_true_eq() && n2->is_true_eq())
                         continue;
                     CTRACE("missing_propagation", congruent(n, n2),
-                           tout << mk_pp(n->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n";
+                           tout << mk_pp(n->get_owner(), m) << "\n" << mk_pp(n2->get_owner(), m) << "\n";
                            display(tout););
                     SASSERT(!congruent(n, n2));
                 }
@@ -202,12 +202,12 @@ namespace smt {
 
     bool context::check_missing_bool_enode_propagation() const {
         for (enode* n : m_enodes) {
-            if (m_manager.is_bool(n->get_owner()) && get_assignment(n) == l_undef) {
+            if (m.is_bool(n->get_owner()) && get_assignment(n) == l_undef) {
                 enode * first = n;
                 do {
                     CTRACE("missing_propagation", get_assignment(n) != l_undef,
-                           tout << mk_pp(first->get_owner(), m_manager) << "\nassignment: " << get_assignment(first) << "\n" 
-                           << mk_pp(n->get_owner(), m_manager) << "\nassignment: " << get_assignment(n) << "\n";);
+                           tout << mk_pp(first->get_owner(), m) << "\nassignment: " << get_assignment(first) << "\n" 
+                           << mk_pp(n->get_owner(), m) << "\nassignment: " << get_assignment(n) << "\n";);
                     SASSERT(get_assignment(n) == l_undef);
                     n = n->get_next();
                 }
@@ -239,18 +239,18 @@ namespace smt {
         unsigned sz = m_asserted_formulas.get_num_formulas();
         for (unsigned i = 0; i < sz; i++) {
             expr * n = m_asserted_formulas.get_formula(i);
-            if (m_manager.is_or(n)) {
-                CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m_manager) << "\n";);
+            if (m.is_or(n)) {
+                CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m) << "\n";);
                 SASSERT(is_relevant(n));
-                TRACE("check_relevancy", tout << "checking:\n" << mk_ll_pp(n, m_manager) << "\n";);
+                TRACE("check_relevancy", tout << "checking:\n" << mk_ll_pp(n, m) << "\n";);
                 SASSERT(m_relevancy_propagator->check_relevancy_or(to_app(n), true));
             }
-            else if (m_manager.is_not(n)) {
-                CTRACE("relevancy_bug", !is_relevant(to_app(n)->get_arg(0)), tout << "n: " << mk_ismt2_pp(n, m_manager) << "\n";);
+            else if (m.is_not(n)) {
+                CTRACE("relevancy_bug", !is_relevant(to_app(n)->get_arg(0)), tout << "n: " << mk_ismt2_pp(n, m) << "\n";);
                 SASSERT(is_relevant(to_app(n)->get_arg(0)));
             }
             else {
-                CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m_manager) << "\n";);
+                CTRACE("relevancy_bug", !is_relevant(n), tout << "n: " << mk_ismt2_pp(n, m) << "\n";);
                 SASSERT(is_relevant(n));
             }
         }
@@ -263,11 +263,11 @@ namespace smt {
     */
     bool context::check_eqc_bool_assignment() const {
         for (enode* e : m_enodes) {
-            if (m_manager.is_bool(e->get_owner())) {
+            if (m.is_bool(e->get_owner())) {
                 enode * r = e->get_root();
                 CTRACE("eqc_bool", get_assignment(e) != get_assignment(r), 
-                       tout << "#" << e->get_owner_id() << "\n" << mk_pp(e->get_owner(), m_manager) << "\n";
-                       tout << "#" << r->get_owner_id() << "\n" << mk_pp(r->get_owner(), m_manager) << "\n";
+                       tout << "#" << e->get_owner_id() << "\n" << mk_pp(e->get_owner(), m) << "\n";
+                       tout << "#" << r->get_owner_id() << "\n" << mk_pp(r->get_owner(), m) << "\n";
                        tout << "assignments: " << get_assignment(e) << " " << get_assignment(r) << "\n";
                        display(tout););
                 SASSERT(get_assignment(e) == get_assignment(r));
@@ -301,19 +301,19 @@ namespace smt {
         for (bool_var v = 0; v < num; v++) {
             if (has_enode(v)) {
                 enode * n = bool_var2enode(v);
-                if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m_manager.is_iff(n->get_owner())) {
-                    TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m_manager) << "\n";);
+                if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m.is_iff(n->get_owner())) {
+                    TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "\n";);
                     enode * lhs = n->get_arg(0)->get_root();
                     enode * rhs = n->get_arg(1)->get_root();
                     if (rhs->is_interpreted() && lhs->is_interpreted())
                         continue;
                     TRACE("check_th_diseq_propagation", tout << "num. theory_vars: " << lhs->get_num_th_vars() << " " 
-                          << mk_pp(m_manager.get_sort(lhs->get_owner()), m_manager) << "\n";);
+                          << mk_pp(m.get_sort(lhs->get_owner()), m) << "\n";);
                     theory_var_list * l = lhs->get_th_var_list();
                     while (l) {
                         theory_id th_id = l->get_th_id();
                         theory * th = get_theory(th_id);
-                        TRACE("check_th_diseq_propagation", tout << "checking theory: " << m_manager.get_family_name(th_id) << "\n";);
+                        TRACE("check_th_diseq_propagation", tout << "checking theory: " << m.get_family_name(th_id) << "\n";);
                         // if the theory doesn't use diseqs, then the diseqs are not propagated.
                         if (th->use_diseqs() && rhs->get_th_var(th_id) != null_theory_var) {
                             bool found = false;
@@ -323,7 +323,7 @@ namespace smt {
                                     enode * lhs_prime = th->get_enode(eq.m_lhs)->get_root();
                                     enode * rhs_prime = th->get_enode(eq.m_rhs)->get_root();
                                     TRACE("check_th_diseq_propagation", 
-                                          tout << m_manager.get_family_name(eq.m_th_id) << "\n";);
+                                          tout << m.get_family_name(eq.m_th_id) << "\n";);
 
                                     if ((lhs == lhs_prime && rhs == rhs_prime) ||
                                         (rhs == lhs_prime && lhs == rhs_prime)) {
@@ -336,11 +336,11 @@ namespace smt {
                             if (!found) {
                             // missed theory diseq propagation
                                 display(std::cout);
-                                std::cout << "checking theory: " << m_manager.get_family_name(th_id) << "\n";
+                                std::cout << "checking theory: " << m.get_family_name(th_id) << "\n";
                                 std::cout << "root: #" << n->get_root()->get_owner_id() << " node: #" << n->get_owner_id() << "\n";
-                                std::cout << mk_pp(n->get_owner(), m_manager) << "\n";
+                                std::cout << mk_pp(n->get_owner(), m) << "\n";
                                 std::cout << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() << "\n";
-                                std::cout << mk_bounded_pp(lhs->get_owner(), m_manager) << " " << mk_bounded_pp(rhs->get_owner(), m_manager) << "\n";
+                                std::cout << mk_bounded_pp(lhs->get_owner(), m) << " " << mk_bounded_pp(rhs->get_owner(), m) << "\n";
                             }
                             VERIFY(found);
                         }
@@ -389,7 +389,6 @@ namespace smt {
         if (!m_proto_model) {
             return true;
         }
-        ast_manager& m = m_manager;
         for (literal lit : m_assigned_literals) {
             if (!is_relevant(lit)) {
                 continue;
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 0823f33d5..f85b803f4 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -98,14 +98,14 @@ namespace smt {
     }
 
     std::ostream& context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
-        display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n"); return out;
+        display_verbose(out, m, num_lits, lits, m_bool_var2expr.c_ptr(), "\n"); return out;
     }
 
     std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const {
         if (l.sign())
-            out << "  (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") ";
+            out << "  (not " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << ") ";
         else
-            out << "  " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " ";
+            out << "  " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << " ";
         return out;
     }
 
@@ -144,7 +144,7 @@ namespace smt {
     void context::display_enode_defs(std::ostream & out) const {
         for (enode * x : m_enodes) {
             expr * n = x->get_owner();
-            ast_def_ll_pp(out, m_manager, n, get_pp_visited(), true, false);
+            ast_def_ll_pp(out, m, n, get_pp_visited(), true, false);
         }
     }
 
@@ -152,7 +152,7 @@ namespace smt {
         unsigned num = get_num_bool_vars();
         for (unsigned v = 0; v < num; v++) {
             expr * n = m_bool_var2expr[v];
-            ast_def_ll_pp(out, m_manager, n, get_pp_visited(), true, false);
+            ast_def_ll_pp(out, m, n, get_pp_visited(), true, false);
         }
     }
 
@@ -162,18 +162,18 @@ namespace smt {
             display_literal(out, l);
             out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
                 << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
-                << mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n";
+                << mk_bounded_pp(bool_var2expr(l.var()), m, 2) << "\n\n";
         }
         return out;
     }
 
     std::ostream& context::display_clause(std::ostream & out, clause const * cls) const {
-        cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
+        cls->display_compact(out, m, m_bool_var2expr.c_ptr());
         return out;
     }
 
     std::ostream& context::display_clause_smt2(std::ostream & out, clause const& cls) const {
-        cls.display_smt2(out, m_manager, m_bool_var2expr.c_ptr());
+        cls.display_smt2(out, m, m_bool_var2expr.c_ptr());
         return out;
     }
 
@@ -200,11 +200,11 @@ namespace smt {
                         out << "binary clauses:\n";
                         first = false;
                     }
-                    expr_ref t1(m_manager), t2(m_manager);
+                    expr_ref t1(m), t2(m);
                     literal2expr(neg_l1, t1);
                     literal2expr(l2, t2);
-                    expr_ref disj(m_manager.mk_or(t1, t2), m_manager);
-                    out << disj << "\n";
+                    expr_ref disj(m.mk_or(t1, t2), m);
+                    out << mk_bounded_pp(disj, m, 3) << "\n";
 #if 0
                     out << "(clause ";
                     display_literal(out, neg_l1);
@@ -225,23 +225,23 @@ namespace smt {
                 display_literal(out, lit);
                 if (!is_relevant(lit)) out << " n ";
                 out << ": ";
-                display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
+                display_verbose(out, m, 1, &lit, m_bool_var2expr.c_ptr());
                 out << "\n";
             }
         }
     }
 
     void context::display_assignment_as_smtlib2(std::ostream& out, symbol const&  logic) const {
-        ast_smt_pp pp(m_manager);
+        ast_smt_pp pp(m);
         pp.set_benchmark_name("lemma");
         pp.set_status("unknown");
         pp.set_logic(logic);
         for (literal lit : m_assigned_literals) {
-            expr_ref n(m_manager);
+            expr_ref n(m);
             literal2expr(lit, n);
             pp.add_assumption(n);
         }
-        pp.display_smt2(out, m_manager.mk_true());
+        pp.display_smt2(out, m.mk_true());
     }
 
     void context::display_eqc(std::ostream & out) const {
@@ -255,7 +255,7 @@ namespace smt {
                     first = false;
                 }
                 out << "#" << n->get_id() << " -> #" << r->get_id() << ": ";
-                out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n";
+                out << mk_pp(n, m) << " -> " << mk_pp(r, m) << "\n";
             }
         }
     }
@@ -373,7 +373,7 @@ namespace smt {
 
     void context::display_unsat_core(std::ostream & out) const {
         for (expr* c : m_unsat_core) {
-            out << mk_pp(c, m_manager) << "\n";
+            out << mk_pp(c, m) << "\n";
         }
     }
 
@@ -426,10 +426,10 @@ namespace smt {
     }
 
     void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
-        ast_pp_util visitor(m_manager);
-        expr_ref_vector fmls(m_manager);
+        ast_pp_util visitor(m);
+        expr_ref_vector fmls(m);
         visitor.collect(fmls);
-        expr_ref n(m_manager);
+        expr_ref n(m);
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
             literal2expr(l, n);
@@ -459,10 +459,10 @@ namespace smt {
     void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
                                                unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
                                                literal consequent, symbol const& logic) const {
-        ast_pp_util visitor(m_manager);
-        expr_ref_vector fmls(m_manager);
+        ast_pp_util visitor(m);
+        expr_ref_vector fmls(m);
         visitor.collect(fmls);
-        expr_ref n(m_manager);
+        expr_ref n(m);
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
             literal2expr(l, n);
@@ -470,7 +470,7 @@ namespace smt {
         }
         for (unsigned i = 0; i < num_eq_antecedents; i++) {
             enode_pair const & p = eq_antecedents[i];
-            n = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
+            n = m.mk_eq(p.first->get_owner(), p.second->get_owner());
             fmls.push_back(n);
         }
         if (consequent != false_literal) {
@@ -564,7 +564,7 @@ namespace smt {
             out.width(6);
             out << std::left << n->get_id();
             out << ", relevant: " << is_relevant(n);
-            if (m_manager.is_bool(n)) {
+            if (m.is_bool(n)) {
                 out << ", val: ";
                 out.width(7);
                 out << std::right;
@@ -615,8 +615,8 @@ namespace smt {
     }
 
     void context::trace_assign(literal l, b_justification j, bool decision) const {
-        SASSERT(m_manager.has_trace_stream());
-        std::ostream & out = m_manager.trace_stream();
+        SASSERT(m.has_trace_stream());
+        std::ostream & out = m.trace_stream();
         out << "[assign] ";
         display_literal(out, l);
         if (decision)
diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp
index 770a6451b..9899ba322 100644
--- a/src/smt/smt_context_stat.cpp
+++ b/src/smt/smt_context_stat.cpp
@@ -25,10 +25,9 @@ namespace smt {
         if (m_lemmas.empty())
             return 0;
         unsigned long long acc            = 0;
-        clause_vector::const_iterator it  = m_lemmas.begin();
-        clause_vector::const_iterator end = m_lemmas.end();
-        for (; it != end; ++it)
-            acc += (*it)->get_activity();
+        for (clause const* cp : m_lemmas) {
+            acc += cp->get_activity();
+        }
         return static_cast<unsigned>(acc / m_lemmas.size());
     }
 
@@ -39,10 +38,9 @@ namespace smt {
     }
 
     static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
-        clause_vector::const_iterator it  = v.begin();
-        clause_vector::const_iterator end = v.end();
-        for (; it != end; ++it)
-            acc_num_occs(*it, lit2num_occs);
+        for (auto cp : v) {
+            acc_num_occs(cp, lit2num_occs);
+        }
     }
 
     void context::display_literal_num_occs(std::ostream & out) const {
@@ -56,7 +54,7 @@ namespace smt {
             if (lit2num_occs[lidx] > 0) {
                 out << lit2num_occs[lidx] << " ";
                 // display_literal(out, l);
-                out << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m_manager);
+                out << l.sign() << " " << mk_pp(bool_var2expr(l.var()), m);
                 out << "\n";
             }
         }
@@ -64,11 +62,8 @@ namespace smt {
 
     void context::display_num_assigned_literals_per_lvl(std::ostream & out) const {
         unsigned n = 0;
-        svector<scope>::const_iterator it  = m_scopes.begin();
-        svector<scope>::const_iterator end = m_scopes.end();
         out << "[";
-        for (; it != end; ++it) {
-            scope const & s = *it;
+        for (scope const& s : m_scopes) {
             SASSERT(n <= s.m_assigned_literals_lim);
             out << (s.m_assigned_literals_lim - n) << " ";
             n = s.m_assigned_literals_lim;
@@ -84,10 +79,9 @@ namespace smt {
     }
 
     static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
-        clause_vector::const_iterator it  = v.begin();
-        clause_vector::const_iterator end = v.end();
-        for (; it != end; ++it)
-            acc_var_num_occs(*it, var2num_occs);
+        for (auto const& n : v) {
+            acc_var_num_occs(n, var2num_occs);
+        }
     }
 
     void context::display_var_occs_histogram(std::ostream & out) const {
@@ -122,10 +116,9 @@ namespace smt {
     }
 
     static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
-        clause_vector::const_iterator it  = v.begin();
-        clause_vector::const_iterator end = v.end();
-        for (; it != end; ++it)
-            acc_var_num_min_occs(*it, var2num_min_occs);
+        for (auto const& c : v) {
+            acc_var_num_min_occs(c, var2num_min_occs);
+        }
     }
 
     void context::display_num_min_occs(std::ostream & out) const {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 3049959bf..0ee56069e 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -110,7 +110,7 @@ namespace smt {
         if (is_quantifier(n))
             return true;
         SASSERT(is_app(n));
-        if (m_manager.is_bool(n)) {
+        if (m.is_bool(n)) {
             if (b_internalized(n))
                 return true;
         }
@@ -137,13 +137,13 @@ namespace smt {
 
         SASSERT(def_int);
 
-        if (m_manager.is_term_ite(n)) {
+        if (m.is_term_ite(n)) {
             ts_visit_child(to_app(n)->get_arg(0), true, tcolors, fcolors, todo, visited);
             ts_visit_child(to_app(n)->get_arg(1), false, tcolors, fcolors, todo, visited);
             ts_visit_child(to_app(n)->get_arg(2), false, tcolors, fcolors, todo, visited);
             return visited;
         }
-        bool new_gate_ctx = m_manager.is_bool(n) && (is_gate(m_manager, n) || m_manager.is_not(n));
+        bool new_gate_ctx = m.is_bool(n) && (is_gate(m, n) || m.is_not(n));
         unsigned j = to_app(n)->get_num_args();
         while (j > 0) {
             --j;
@@ -170,7 +170,7 @@ namespace smt {
             case Grey:
                 SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, todo));
                 set_color(tcolors, fcolors, curr, gate_ctx, Black);
-                if (n != curr && !m_manager.is_not(curr))
+                if (n != curr && !m.is_not(curr))
                     sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));
                 break;
             case Black:
@@ -190,8 +190,8 @@ namespace smt {
        \remark pr is 0 if proofs are disabled.
     */
     void context::internalize_assertion(expr * n, proof * pr, unsigned generation) {
-        TRACE("internalize_assertion", tout << mk_pp(n, m_manager) << "\n";); 
-        TRACE("internalize_assertion_ll", tout << mk_ll_pp(n, m_manager) << "\n";); 
+        TRACE("internalize_assertion", tout << mk_pp(n, m) << "\n";); 
+        TRACE("internalize_assertion_ll", tout << mk_ll_pp(n, m) << "\n";); 
         TRACE("generation", tout << "generation: " << m_generation << "\n";);
         TRACE("incompleteness_bug", tout << "[internalize-assertion]: #" << n->get_id() << "\n";);
         flet<unsigned> l(m_generation, generation);
@@ -201,7 +201,7 @@ namespace smt {
             // stack overflow.
             // a caveat is that theory internalizers do rely on recursive descent so
             // internalization over these follows top-down
-            TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager););
+            TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m););
             svector<expr_bool_pair> sorted_exprs;
             top_sort_expr(n, sorted_exprs);
             TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
@@ -209,12 +209,12 @@ namespace smt {
                 expr* e = kv.first;
                 if (!is_app(e) || 
                     to_app(e)->get_family_id() == null_family_id || 
-                    to_app(e)->get_family_id() == m_manager.get_basic_family_id()) 
+                    to_app(e)->get_family_id() == m.get_basic_family_id()) 
                     internalize(e, kv.second);
             }
         }
-        SASSERT(m_manager.is_bool(n));
-        if (is_gate(m_manager, n)) {
+        SASSERT(m.is_bool(n));
+        if (is_gate(m, n)) {
             switch(to_app(n)->get_decl_kind()) {
             case OP_AND: {
                 for (expr * arg : *to_app(n)) {
@@ -265,7 +265,7 @@ namespace smt {
             }
             mark_as_relevant(n);
         }
-        else if (m_manager.is_distinct(n)) {
+        else if (m.is_distinct(n)) {
             assert_distinct(to_app(n), pr);
             mark_as_relevant(n);
         }
@@ -291,22 +291,22 @@ namespace smt {
 #define DISTINCT_SZ_THRESHOLD 32
 
     void context::assert_distinct(app * n, proof * pr) {
-        TRACE("assert_distinct", tout << mk_pp(n, m_manager) << "\n";);
+        TRACE("assert_distinct", tout << mk_pp(n, m) << "\n";);
         unsigned num_args = n->get_num_args();
-        if (num_args == 0 || num_args <= DISTINCT_SZ_THRESHOLD || m_manager.proofs_enabled()) {
+        if (num_args == 0 || num_args <= DISTINCT_SZ_THRESHOLD || m.proofs_enabled()) {
             assert_default(n, pr);
             return;
         }
-        sort * s = m_manager.get_sort(n->get_arg(0));
-        sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager);
-        func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager);
+        sort * s = m.get_sort(n->get_arg(0));
+        sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
+        func_decl_ref f(m.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m);
         for (expr * arg : *n) {
-            app_ref fapp(m_manager.mk_app(f, arg), m_manager);
-            app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager);
+            app_ref fapp(m.mk_app(f, arg), m);
+            app_ref val(m.mk_fresh_const("unique-value", u), m);
             enode * e   = mk_enode(val, false, false, true);
             e->mark_as_interpreted();
-            app_ref eq(m_manager.mk_eq(fapp, val), m_manager);
-            TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";);
+            app_ref eq(m.mk_eq(fapp, val), m);
+            TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m) << "\n";);
             assert_default(eq, nullptr);
             mark_as_relevant(eq.get());
             // TODO: we may want to hide the auxiliary values val and the function f from the model.
@@ -331,12 +331,12 @@ namespace smt {
        - gate_ctx is true if the expression is in the context of a logical gate.
     */
     void context::internalize(expr * n, bool gate_ctx) {
-        TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";);
-        TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";);
+        TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";);
+        TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m) << "\n";);
         if (is_var(n)) {
             throw default_exception("Formulas should not contain unbound variables");
         }
-        if (m_manager.is_bool(n)) {
+        if (m.is_bool(n)) {
             SASSERT(is_quantifier(n) || is_app(n));
             internalize_formula(n, gate_ctx);
         }
@@ -355,12 +355,12 @@ namespace smt {
        \brief Internalize the given formula into the logical context.
     */
     void context::internalize_formula(expr * n, bool gate_ctx) {
-        TRACE("internalize_bug", tout << "internalize formula: #" << n->get_id() << ", gate_ctx: " << gate_ctx << "\n" << mk_pp(n, m_manager) << "\n";);
-        SASSERT(m_manager.is_bool(n));
-        if (m_manager.is_true(n) || m_manager.is_false(n))
+        TRACE("internalize_bug", tout << "internalize formula: #" << n->get_id() << ", gate_ctx: " << gate_ctx << "\n" << mk_pp(n, m) << "\n";);
+        SASSERT(m.is_bool(n));
+        if (m.is_true(n) || m.is_false(n))
             return;
 
-        if (m_manager.is_not(n) && gate_ctx) {
+        if (m.is_not(n) && gate_ctx) {
             // a boolean variable does not need to be created if n a NOT gate is in
             // the context of a gate.
             internalize(to_app(n)->get_arg(0), true);
@@ -396,9 +396,9 @@ namespace smt {
             return;
         }
 
-        if (m_manager.is_eq(n) && !m_manager.is_iff(n))
+        if (m.is_eq(n) && !m.is_iff(n))
             internalize_eq(to_app(n), gate_ctx);
-        else if (m_manager.is_distinct(n))
+        else if (m.is_distinct(n))
             internalize_distinct(to_app(n), gate_ctx);
         else if (is_app(n) && internalize_theory_atom(to_app(n), gate_ctx))
             return;
@@ -412,15 +412,15 @@ namespace smt {
        \brief Internalize an equality.
     */
     void context::internalize_eq(app * n, bool gate_ctx) {
-        TRACE("internalize", tout << mk_pp(n, m_manager) << "\n";);
+        TRACE("internalize", tout << mk_pp(n, m) << "\n";);
         SASSERT(!b_internalized(n));
-        SASSERT(m_manager.is_eq(n));
+        SASSERT(m.is_eq(n));
         internalize_formula_core(n, gate_ctx);
         bool_var v        = get_bool_var(n);
         bool_var_data & d = get_bdata(v);
         d.set_eq_flag();
         
-        sort * s    = m_manager.get_sort(n->get_arg(0));
+        sort * s    = m.get_sort(n->get_arg(0));
         theory * th = m_theories.get_plugin(s->get_family_id());
         if (th)
             th->internalize_eq_eh(n, v);
@@ -430,10 +430,10 @@ namespace smt {
        \brief Internalize distinct constructor.
     */
     void context::internalize_distinct(app * n, bool gate_ctx) {
-        TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m_manager) << "\n";);
+        TRACE("distinct", tout << "internalizing distinct: " << mk_pp(n, m) << "\n";);
         SASSERT(!b_internalized(n));
-        SASSERT(m_manager.is_distinct(n));
-        expr_ref def(m_manager.mk_distinct_expanded(n->get_num_args(), n->get_args()), m_manager);
+        SASSERT(m.is_distinct(n));
+        expr_ref def(m.mk_distinct_expanded(n->get_num_args(), n->get_args()), m);
         internalize(def, true);
         bool_var v    = mk_bool_var(n);
         literal l(v);
@@ -456,10 +456,10 @@ namespace smt {
     bool context::internalize_theory_atom(app * n, bool gate_ctx) {
         SASSERT(!b_internalized(n));
         theory * th  = m_theories.get_plugin(n->get_family_id());
-        TRACE("datatype_bug", tout << "internalizing theory atom:\n" << mk_pp(n, m_manager) << "\n";);
+        TRACE("datatype_bug", tout << "internalizing theory atom:\n" << mk_pp(n, m) << "\n";);
         if (!th || !th->internalize_atom(n, gate_ctx))
             return false;
-        TRACE("datatype_bug", tout << "internalization succeeded\n" << mk_pp(n, m_manager) << "\n";);
+        TRACE("datatype_bug", tout << "internalization succeeded\n" << mk_pp(n, m) << "\n";);
         SASSERT(b_internalized(n));
         TRACE("internalize_theory_atom", tout << "internalizing theory atom: #" << n->get_id() << "\n";);
         bool_var v        = get_bool_var(n);
@@ -524,8 +524,8 @@ namespace smt {
        context. 
     */
     void context::internalize_quantifier(quantifier * q, bool gate_ctx) {
-        TRACE("internalize_quantifier", tout << mk_pp(q, m_manager) << "\n";);
-        CTRACE("internalize_quantifier_zero", q->get_weight() == 0, tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";);
+        CTRACE("internalize_quantifier_zero", q->get_weight() == 0, tout << mk_pp(q, m) << "\n";);
         SASSERT(gate_ctx); // limitation of the current implementation
         SASSERT(!b_internalized(q));
         SASSERT(is_forall(q));
@@ -543,22 +543,22 @@ namespace smt {
     }
 
     void context::internalize_lambda(quantifier * q) {
-        TRACE("internalize_quantifier", tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";);
         SASSERT(is_lambda(q));
-        app_ref lam_name(m_manager.mk_fresh_const("lambda", m_manager.get_sort(q)), m_manager);
-        app_ref eq(m_manager), lam_app(m_manager);
-        expr_ref_vector vars(m_manager);
+        app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m);
+        app_ref eq(m), lam_app(m);
+        expr_ref_vector vars(m);
         vars.push_back(lam_name);
         unsigned sz = q->get_num_decls();
         for (unsigned i = 0; i < sz; ++i) {
-            vars.push_back(m_manager.mk_var(sz - i - 1, q->get_decl_sort(i)));
+            vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i)));
         }
-        array_util autil(m_manager);
+        array_util autil(m);
         lam_app = autil.mk_select(vars.size(), vars.c_ptr());
-        eq = m_manager.mk_eq(lam_app, q->get_expr());
-        quantifier_ref fa(m_manager);
-        expr * patterns[1] = { m_manager.mk_pattern(lam_app) };
-        fa = m_manager.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m_manager.lambda_def_qid(), symbol::null, 1, patterns);
+        eq = m.mk_eq(lam_app, q->get_expr());
+        quantifier_ref fa(m);
+        expr * patterns[1] = { m.mk_pattern(lam_app) };
+        fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns);
         internalize_quantifier(fa, true);
         if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name);
         m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
@@ -571,15 +571,15 @@ namespace smt {
         SASSERT(!b_internalized(n));
         SASSERT(!e_internalized(n));
 
-        CTRACE("resolve_conflict_crash", m_manager.is_not(n), tout << mk_ismt2_pp(n, m_manager) << "\ngate_ctx: " << gate_ctx << "\n";);
+        CTRACE("resolve_conflict_crash", m.is_not(n), tout << mk_ismt2_pp(n, m) << "\ngate_ctx: " << gate_ctx << "\n";);
 
-        bool _is_gate  = is_gate(m_manager, n) || m_manager.is_not(n);
+        bool _is_gate  = is_gate(m, n) || m.is_not(n);
         // process args
         for (expr * arg : *n) {
             internalize(arg, _is_gate);
         }
         
-        CTRACE("internalize_bug", b_internalized(n), tout << mk_ll_pp(n, m_manager) << "\n";);
+        CTRACE("internalize_bug", b_internalized(n), tout << mk_ll_pp(n, m) << "\n";);
         
         bool is_new_var = false;
         bool_var v;
@@ -602,7 +602,7 @@ namespace smt {
         // 1) it is not in the context of a gate, or
         // 2) it has arguments and it is not a gate (i.e., uninterpreted predicate or equality).
         if (!e_internalized(n) && (!gate_ctx || (!_is_gate && n->get_num_args() > 0))) {
-            bool suppress_args = _is_gate || m_manager.is_not(n);
+            bool suppress_args = _is_gate || m.is_not(n);
             bool merge_tf      = !gate_ctx;
             mk_enode(n, suppress_args, merge_tf, true);
             set_enode_flag(v, is_new_var);
@@ -617,7 +617,7 @@ namespace smt {
         // Now, if v is assigned before being associated with an enode, then
         // v is not going to be inserted in m_atom_propagation_queue, and
         // propagate_bool_var_enode() method is not going to be invoked for v.
-        if (is_new_var && n->get_family_id() == m_manager.get_basic_family_id()) {
+        if (is_new_var && n->get_family_id() == m.get_basic_family_id()) {
             switch (n->get_decl_kind()) {
             case OP_NOT:
                 SASSERT(!gate_ctx);
@@ -632,7 +632,7 @@ namespace smt {
                 add_or_rel_watches(to_app(n));
                 break;
             case OP_EQ:
-                if (m_manager.is_iff(n))
+                if (m.is_iff(n))
                     mk_iff_cnstr(to_app(n));
                 break;
             case OP_ITE:
@@ -758,7 +758,7 @@ namespace smt {
             return;
         }
 
-        if (m_manager.is_term_ite(n)) {
+        if (m.is_term_ite(n)) {
             internalize_ite_term(n);
             return; // it is not necessary to apply sort constraint
         }
@@ -781,8 +781,8 @@ namespace smt {
         expr * c  = n->get_arg(0);
         expr * t  = n->get_arg(1);
         expr * e  = n->get_arg(2);
-        app_ref eq1(mk_eq_atom(n, t), m_manager);
-        app_ref eq2(mk_eq_atom(n, e), m_manager);
+        app_ref eq1(mk_eq_atom(n, t), m);
+        app_ref eq2(mk_eq_atom(n, e), m);
         mk_enode(n, 
                  true /* suppress arguments, I don't want to apply CC on ite terms */,
                  false /* it is a term, so it should not be merged with true/false */,
@@ -796,12 +796,12 @@ namespace smt {
         literal eq1_lit = get_literal(eq1);
         literal eq2_lit = get_literal(eq2);
         TRACE("internalize_ite_term_bug",
-              tout << mk_ismt2_pp(n, m_manager) << "\n";
-              tout << mk_ismt2_pp(c, m_manager) << "\n";
-              tout << mk_ismt2_pp(t, m_manager) << "\n";
-              tout << mk_ismt2_pp(e, m_manager) << "\n";              
-              tout << mk_ismt2_pp(eq1, m_manager) << "\n";              
-              tout << mk_ismt2_pp(eq2, m_manager) << "\n";              
+              tout << mk_ismt2_pp(n, m) << "\n";
+              tout << mk_ismt2_pp(c, m) << "\n";
+              tout << mk_ismt2_pp(t, m) << "\n";
+              tout << mk_ismt2_pp(e, m) << "\n";              
+              tout << mk_ismt2_pp(eq1, m) << "\n";              
+              tout << mk_ismt2_pp(eq2, m) << "\n";              
               tout << "literals:\n" << c_lit << " " << eq1_lit << " " << eq2_lit << "\n";);
         mk_gate_clause(~c_lit, eq1_lit);
         mk_gate_clause( c_lit, eq2_lit);
@@ -851,7 +851,7 @@ namespace smt {
     */
     bool_var context::mk_bool_var(expr * n) {
         SASSERT(!b_internalized(n));
-        //SASSERT(!m_manager.is_not(n));
+        //SASSERT(!m.is_not(n));
         unsigned id = n->get_id();
         bool_var v  = m_b_internalized_stack.size();
 #ifndef _EXTERNAL_RELEASE 
@@ -859,13 +859,13 @@ namespace smt {
             char const * header = "(iff z3@";
             int  id_sz = 6;
             std::cerr.width(id_sz);
-            std::cerr << header << std::left << v << " " << mk_pp(n, m_manager, static_cast<unsigned>(strlen(header)) + id_sz + 1) << ")\n";
+            std::cerr << header << std::left << v << " " << mk_pp(n, m, static_cast<unsigned>(strlen(header)) + id_sz + 1) << ")\n";
         }
         if (m_fparams.m_display_ll_bool_var2expr) {
-            std::cerr << v << " ::=\n" << mk_ll_pp(n, m_manager) << "<END-OF-FORMULA>\n";
+            std::cerr << v << " ::=\n" << mk_ll_pp(n, m) << "<END-OF-FORMULA>\n";
         }
 #endif
-        TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m_manager) << " " << n->get_id() << "\n";);
+        TRACE("mk_bool_var", tout << "creating boolean variable: " << v << " for:\n" << mk_pp(n, m) << " " << n->get_id() << "\n";);
         TRACE("mk_var_bug", tout << "mk_bool: " << v << "\n";);                
         set_bool_var(id, v);
         m_bdata.reserve(v+1);
@@ -909,7 +909,7 @@ namespace smt {
         unsigned n_id         = n->get_id();
         bool_var v            = get_bool_var_of_id(n_id);
         m_bool_var2expr[v]    = nullptr;
-        TRACE("undo_mk_bool_var", tout << "undo_bool: " << v << "\n" << mk_pp(n, m_manager) << "\n" << "m_bdata.size: " << m_bdata.size()
+        TRACE("undo_mk_bool_var", tout << "undo_bool: " << v << "\n" << mk_pp(n, m) << "\n" << "m_bdata.size: " << m_bdata.size()
               << " m_assignment.size: " << m_assignment.size() << "\n";);
         TRACE("mk_var_bug", tout << "undo_mk_bool: " << v << "\n";);
         // bool_var_data & d     = m_bdata[v];
@@ -927,7 +927,7 @@ namespace smt {
        in the egraph.
     */
     enode * context::mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled) {
-        TRACE("mk_enode_detail", tout << mk_pp(n, m_manager) << "\nsuppress_args: " << suppress_args << ", merge_tf: " << 
+        TRACE("mk_enode_detail", tout << mk_pp(n, m) << "\nsuppress_args: " << suppress_args << ", merge_tf: " << 
               merge_tf << ", cgc_enabled: " << cgc_enabled << "\n";);
         SASSERT(!e_internalized(n));
         unsigned id          = n->get_id();
@@ -938,9 +938,9 @@ namespace smt {
             CTRACE("cached_generation", generation != m_generation,
                    tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
         }
-        enode * e           = enode::mk(m_manager, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
+        enode * e           = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
         TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
-        if (n->get_num_args() == 0 && m_manager.is_unique_value(n))
+        if (n->get_num_args() == 0 && m.is_unique_value(n))
             e->mark_as_interpreted();
         TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
         TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);
@@ -980,14 +980,14 @@ namespace smt {
         }
         SASSERT(e_internalized(n));
         m_stats.m_num_mk_enode++;
-        TRACE("mk_enode", tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m_manager) << "\n";
+        TRACE("mk_enode", tout << "created enode: #" << e->get_owner_id() << " for:\n" << mk_pp(n, m) << "\n";
               if (e->get_num_args() > 0) {
                   tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: " 
                        << e->is_cgr() << "\n";
               });
 
-        if (m_manager.has_trace_stream())
-            m_manager.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";        
+        if (m.has_trace_stream())
+            m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";        
 
         return e;
     }
@@ -996,7 +996,7 @@ namespace smt {
         SASSERT(!m_e_internalized_stack.empty());
         m_stats.m_num_del_enode++;
         expr * n              = m_e_internalized_stack.back();
-        TRACE("undo_mk_enode", tout << "undo_enode: #" << n->get_id() << "\n" << mk_pp(n, m_manager) << "\n";);
+        TRACE("undo_mk_enode", tout << "undo_enode: #" << n->get_id() << "\n" << mk_pp(n, m) << "\n";);
         TRACE("mk_var_bug", tout << "undo_mk_enode: " << n->get_id() << "\n";);
         unsigned n_id         = n->get_id();
         SASSERT(is_app(n));
@@ -1012,7 +1012,7 @@ namespace smt {
             SASSERT(m_decl2enodes[decl_id].back() == e);
             m_decl2enodes[decl_id].pop_back();
         }
-        e->del_eh(m_manager);
+        e->del_eh(m);
         SASSERT(m_e_internalized_stack.size() == m_enodes.size());
         m_enodes.pop_back();
         m_e_internalized_stack.pop_back();
@@ -1033,15 +1033,15 @@ namespace smt {
        \brief Return the literal associated with n.
     */
     literal context::get_literal(expr * n) const {
-        if (m_manager.is_not(n)) {
-            CTRACE("get_literal_bug", !b_internalized(to_app(n)->get_arg(0)), tout << mk_ll_pp(n, m_manager) << "\n";);
+        if (m.is_not(n)) {
+            CTRACE("get_literal_bug", !b_internalized(to_app(n)->get_arg(0)), tout << mk_ll_pp(n, m) << "\n";);
             SASSERT(b_internalized(to_app(n)->get_arg(0)));
             return literal(get_bool_var(to_app(n)->get_arg(0)), true);
         }
-        else if (m_manager.is_true(n)) {
+        else if (m.is_true(n)) {
             return true_literal;
         }
-        else if (m_manager.is_false(n)) {
+        else if (m.is_false(n)) {
             return false_literal;
         }
         else {
@@ -1378,7 +1378,7 @@ namespace smt {
             bool save_atoms     = lemma && iscope_lvl > m_base_lvl;
             bool reinit         = save_atoms;
             SASSERT(!lemma || j == 0 || !j->in_region());
-            clause * cls = clause::mk(m_manager, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.c_ptr());
+            clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.c_ptr());
             m_clause_proof.add(*cls);
             if (lemma) {
                 cls->set_activity(activity);
@@ -1455,7 +1455,7 @@ namespace smt {
         justification * js = nullptr;
         TRACE("mk_th_axiom", display_literals_verbose(tout, num_lits, lits) << "\n";);
 
-        if (m_manager.proofs_enabled()) {
+        if (m.proofs_enabled()) {
             js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
         }
         if (m_fparams.m_smtlib_dump_lemmas) {
@@ -1483,20 +1483,20 @@ namespace smt {
             literal l      = lits[i];
             bool_var v     = l.var();
             expr * atom    = m_bool_var2expr[v]; 
-            new_lits.push_back(l.sign() ? m_manager.mk_not(atom) : atom);
+            new_lits.push_back(l.sign() ? m.mk_not(atom) : atom);
         }
         if (root_gate)
-            new_lits.push_back(m_manager.mk_not(root_gate));
+            new_lits.push_back(m.mk_not(root_gate));
         SASSERT(num_lits > 1);
-        expr * fact        = m_manager.mk_or(new_lits.size(), new_lits.c_ptr());
-        return m_manager.mk_def_axiom(fact);
+        expr * fact        = m.mk_or(new_lits.size(), new_lits.c_ptr());
+        return m.mk_def_axiom(fact);
         
     }
 
     void context::mk_gate_clause(unsigned num_lits, literal * lits) {
-        if (m_manager.proofs_enabled()) {
+        if (m.proofs_enabled()) {
             proof * pr = mk_clause_def_axiom(num_lits, lits, nullptr);
-            TRACE("gate_clause", tout << mk_ll_pp(pr, m_manager););
+            TRACE("gate_clause", tout << mk_ll_pp(pr, m););
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }
         else {
@@ -1520,15 +1520,15 @@ namespace smt {
     }
 
     void context::mk_root_clause(unsigned num_lits, literal * lits, proof * pr) {
-        if (m_manager.proofs_enabled()) {
-            SASSERT(m_manager.get_fact(pr));
-            expr * fact = m_manager.get_fact(pr);
-            if (!m_manager.is_or(fact)) {
-                proof * def = mk_clause_def_axiom(num_lits, lits, m_manager.get_fact(pr));
-                TRACE("gate_clause", tout << mk_ll_pp(def, m_manager) << "\n";
-                      tout << mk_ll_pp(pr, m_manager););
+        if (m.proofs_enabled()) {
+            SASSERT(m.get_fact(pr));
+            expr * fact = m.get_fact(pr);
+            if (!m.is_or(fact)) {
+                proof * def = mk_clause_def_axiom(num_lits, lits, m.get_fact(pr));
+                TRACE("gate_clause", tout << mk_ll_pp(def, m) << "\n";
+                      tout << mk_ll_pp(pr, m););
                 proof * prs[2] = { def, pr };
-                pr  = m_manager.mk_unit_resolution(2, prs);
+                pr  = m.mk_unit_resolution(2, prs);
             }
             mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
         }