diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index abcc97882..75b4e55f4 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -255,9 +255,9 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
     app * n = to_app(_n);
     quantifier * q = 0;
     func_decl * d  = n->get_decl(); 
-    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m_manager) << "\nd:\n" << d->get_name() << "\n";);
+    TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
     if (m_macro_manager.m_decl2macro.find(d, q)) {
-        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m_manager) << "\n";);
+        TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
         app * head = 0;
         expr * def = 0;
         m_macro_manager.get_head_def(q, d, head, def);
@@ -272,17 +272,17 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
             SASSERT(subst_args[nidx] == 0);
             subst_args[nidx] = n->get_arg(i);
         }
-        var_subst s(m_manager);
+        var_subst s(m);
         s(def, num, subst_args.c_ptr(), r);
-        if (m_manager.proofs_enabled()) {
-            expr_ref instance(m_manager);
+        if (m.proofs_enabled()) {
+            expr_ref instance(m);
             s(q->get_expr(), num, subst_args.c_ptr(), instance);
-            proof * qi_pr = m_manager.mk_quant_inst(m_manager.mk_or(m_manager.mk_not(q), instance), num, subst_args.c_ptr());
+            proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
             proof * q_pr  = 0;
             m_macro_manager.m_decl2macro_pr.find(d, q_pr);
             SASSERT(q_pr != 0);
             proof * prs[2] = { qi_pr, q_pr };
-            p = m_manager.mk_unit_resolution(2, prs);
+            p = m.mk_unit_resolution(2, prs);
         }
         else {
             p = 0;
diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 83362f5b3..b93dd7657 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -116,7 +116,7 @@ void pattern_inference::collect::operator()(expr * n, unsigned num_bindings) {
         n              = e.m_node;
         unsigned delta = e.m_delta;
         TRACE("collect", tout << "processing: " << n->get_id() << " " << delta << " kind: " << n->get_kind() << "\n";);
-        TRACE("collect_info", tout << mk_pp(n, m_manager) << "\n";);
+        TRACE("collect_info", tout << mk_pp(n, m) << "\n";);
         if (visit_children(n, delta)) {
             m_todo.pop_back();
             save_candidate(n, delta);
@@ -170,9 +170,9 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
                 free_vars.insert(idx);
             info * i = 0;
             if (delta == 0)
-                i = alloc(info, m_manager, n, free_vars, 1);
+                i = alloc(info, m, n, free_vars, 1);
             else
-                i = alloc(info, m_manager, m_manager.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
+                i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1);
             save(n, delta, i);
         }
         else {
@@ -189,7 +189,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         }
         
         if (c->get_num_args() == 0) {
-            save(n, delta, alloc(info, m_manager, n, uint_set(), 1));
+            save(n, delta, alloc(info, m, n, uint_set(), 1));
             return;
         }
 
@@ -219,10 +219,10 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
             
         app * new_node = 0;
         if (changed)
-            new_node = m_manager.mk_app(decl, buffer.size(), buffer.c_ptr());
+            new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr());
         else
             new_node = to_app(n);
-        save(n, delta, alloc(info, m_manager, new_node, free_vars, size));
+        save(n, delta, alloc(info, m, new_node, free_vars, size));
         // Remark: arithmetic patterns are only used if they are nested inside other terms.
         // That is, we never consider x + 1 as pattern. On the other hand, f(x+1) can be a pattern
         // if arithmetic is not in the forbidden list.
@@ -235,7 +235,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
         decl_kind k   = c->get_decl_kind();
         if (!free_vars.empty() && 
             (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
-            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m_manager) << "\n";);
+            TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
             m_owner.add_candidate(new_node, free_vars, size);
         }
         return;
@@ -338,7 +338,7 @@ bool pattern_inference::contains_subpattern::operator()(expr * n) {
                     uint_set const & s2 = e->get_data().m_value.m_free_vars;
                     SASSERT(s2.subset_of(s1));
                     if (s1 == s2) {
-                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m_manager) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m_manager) << "\n";);
+                        TRACE("pattern_inference", tout << mk_pp(n, m_owner.m) << "\nis bigger than\n" << mk_pp(to_app(curr), m_owner.m) << "\n";);
                         return true;
                     }
                 }
@@ -411,7 +411,7 @@ void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candid
         expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
         info const & i = e->get_data().m_value;
         if (i.m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(candidate);
+            app * new_pattern = m.mk_pattern(candidate);
             result.push_back(new_pattern);
         }
         else {
@@ -435,7 +435,7 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
     for (unsigned j = 0; j < m_pre_patterns.size(); j++) {
         pre_pattern * curr = m_pre_patterns[j];
         if (curr->m_free_vars.num_elems() == m_num_bindings) {
-            app * new_pattern = m_manager.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
+            app * new_pattern = m.mk_pattern(curr->m_exprs.size(), curr->m_exprs.c_ptr());
             result.push_back(new_pattern);
             if (result.size() >= max_num_patterns)
                 return;
@@ -489,7 +489,7 @@ bool pattern_inference::is_forbidden(app * n) const {
     // occur outside of the quantifier. That is, Z3 will never match this kind of 
     // pattern.
     if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
-        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m_manager) << "\n";);
+        CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }
     if (is_forbidden(decl))
@@ -509,8 +509,8 @@ bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patte
             expr2info::obj_map_entry * e = m_candidates_info.find_core(candidate);
             info const & i = e->get_data().m_value;
             if (i.m_free_vars.num_elems() == m_num_bindings) {
-                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m_manager) << "\n";);
-                app * p = m_manager.mk_pattern(candidate);
+                TRACE("pattern_inference", tout << "found preferred pattern:\n" << mk_pp(candidate, m) << "\n";);
+                app * p = m.mk_pattern(candidate);
                 result.push_back(p);
                 found = true;
             }
@@ -531,11 +531,11 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
     m_collect(n, num_bindings);
 
     TRACE("pattern_inference", 
-          tout << mk_pp(n, m_manager);
+          tout << mk_pp(n, m);
           tout << "\ncandidates:\n";
           unsigned num = m_candidates.size();
           for (unsigned i = 0; i < num; i++) {
-              tout << mk_pp(m_candidates.get(i), m_manager) << "\n";
+              tout << mk_pp(m_candidates.get(i), m) << "\n";
           });
 
     if (!m_candidates.empty()) {
@@ -543,7 +543,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
         filter_looping_patterns(m_tmp1);
         TRACE("pattern_inference",
               tout << "candidates after removing looping-patterns:\n";
-              dump_app_vector(tout, m_tmp1, m_manager););
+              dump_app_vector(tout, m_tmp1, m););
         SASSERT(!m_tmp1.empty());
         if (!has_preferred_patterns(m_tmp1, result)) {
             // continue if there are no preferred patterns
@@ -552,7 +552,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
             SASSERT(!m_tmp2.empty());
             TRACE("pattern_inference",
                   tout << "candidates after removing bigger patterns:\n";
-                  dump_app_vector(tout, m_tmp2, m_manager););
+                  dump_app_vector(tout, m_tmp2, m););
             m_tmp1.reset();
             candidates2unary_patterns(m_tmp2, m_tmp1, result);
             unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns;
@@ -563,7 +563,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
                 std::stable_sort(m_tmp1.begin(), m_tmp1.end(), m_pattern_weight_lt);
                 TRACE("pattern_inference",
                       tout << "candidates after sorting:\n";
-                      dump_app_vector(tout, m_tmp1, m_manager););
+                      dump_app_vector(tout, m_tmp1, m););
                 candidates2multi_patterns(num_extra_multi_patterns, m_tmp1, result);
             }
         }
@@ -577,7 +577,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
 #include"database.h" // defines g_pattern_database
 
 void pattern_inference::reduce1_quantifier(quantifier * q) {
-    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";);
+    TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
     if (!q->is_forall()) {
         simplifier::reduce1_quantifier(q);
         return;
@@ -587,27 +587,27 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
 
     if (m_params.m_pi_use_database) {
         m_database.initialize(g_pattern_database);
-        app_ref_vector new_patterns(m_manager);
+        app_ref_vector new_patterns(m);
         unsigned new_weight;
         if (m_database.match_quantifier(q, new_patterns, new_weight)) {
 #ifdef Z3DEBUG
-            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); }
+            for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); }
 #endif
-            quantifier_ref new_q(m_manager);
+            quantifier_ref new_q(m);
             if (q->get_num_patterns() > 0) {
                 // just update the weight...
-                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m_manager) << "\n";);
-                new_q = m_manager.update_quantifier_weight(q, new_weight);
+                TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";);
+                new_q = m.update_quantifier_weight(q, new_weight);
             }
             else {
-                quantifier_ref tmp(m_manager);
-                tmp   = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
-                new_q = m_manager.update_quantifier_weight(tmp, new_weight); 
-                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m_manager) << "\n";);
+                quantifier_ref tmp(m);
+                tmp   = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
+                new_q = m.update_quantifier_weight(tmp, new_weight); 
+                TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
             }
             proof * pr = 0;
-            if (m_manager.fine_grain_proofs())
-                pr = m_manager.mk_rewrite(q, new_q);
+            if (m.fine_grain_proofs())
+                pr = m.mk_rewrite(q, new_q);
             cache_result(q, new_q, pr);
             return;
         }
@@ -635,7 +635,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         new_no_patterns.push_back(new_pattern);
     } 
     
-    app_ref_buffer new_patterns(m_manager);
+    app_ref_buffer new_patterns(m);
     
     if (m_params.m_pi_arith == AP_CONSERVATIVE)
         m_forbidden.push_back(m_afid);
@@ -677,26 +677,26 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                     warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>).", 
                                 q->get_qid().str().c_str(), weight);         
                 }
-                // verbose_stream() << mk_pp(q, m_manager) << "\n";
+                // verbose_stream() << mk_pp(q, m) << "\n";
             }
         }
     }
 
-    quantifier_ref new_q(m_manager);
-    new_q = m_manager.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
+    quantifier_ref new_q(m);
+    new_q = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body);
     if (weight != q->get_weight())
-        new_q = m_manager.update_quantifier_weight(new_q, weight);
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs()) {  
+        new_q = m.update_quantifier_weight(new_q, weight);
+    proof_ref pr(m);
+    if (m.fine_grain_proofs()) {  
         if (new_body_pr == 0)
-            new_body_pr = m_manager.mk_reflexivity(new_body);
-        pr = m_manager.mk_quant_intro(q, new_q, new_body_pr);
+            new_body_pr = m.mk_reflexivity(new_body);
+        pr = m.mk_quant_intro(q, new_q, new_body_pr);
     }
     
     if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) {
-        pull_quant pull(m_manager);
-        expr_ref   new_expr(m_manager);
-        proof_ref  new_pr(m_manager);
+        pull_quant pull(m);
+        expr_ref   new_expr(m);
+        proof_ref  new_pr(m);
         pull(new_q, new_expr, new_pr);
         quantifier * new_new_q = to_quantifier(new_expr);
         if (new_new_q != new_q) {
@@ -705,12 +705,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
                 if (m_params.m_pi_warnings) {
                     warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
                 }
-                new_q = m_manager.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
-                if (m_manager.fine_grain_proofs()) {
-                    pr = m_manager.mk_transitivity(pr, new_pr);
-                    pr = m_manager.mk_transitivity(pr, m_manager.mk_quant_intro(new_new_q, new_q, m_manager.mk_reflexivity(new_q->get_expr())));
+                new_q = m.update_quantifier(new_new_q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_new_q->get_expr());
+                if (m.fine_grain_proofs()) {
+                    pr = m.mk_transitivity(pr, new_pr);
+                    pr = m.mk_transitivity(pr, m.mk_quant_intro(new_new_q, new_q, m.mk_reflexivity(new_q->get_expr())));
                 }
-                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m_manager) << "\n";);
+                TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);
             }
         }
     }
@@ -719,7 +719,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
         if (m_params.m_pi_warnings) {
             warning_msg("failed to find a pattern for quantifier (quantifier id: %s)", q->get_qid().str().c_str());
         }
-        TRACE("pi_failed", tout << mk_pp(q, m_manager) << "\n";);
+        TRACE("pi_failed", tout << mk_pp(q, m) << "\n";);
     }
 
     if (new_patterns.empty() && new_body == q->get_expr()) {
diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index 97897835c..152f7f459 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -38,7 +38,7 @@ Revision History:
    every instance of f(g(X)) is also an instance of f(X).
 */
 class smaller_pattern {
-    ast_manager &    m_manager;
+    ast_manager &    m;
     ptr_vector<expr> m_bindings;
 
     typedef std::pair<expr *, expr *> expr_pair;
@@ -54,7 +54,7 @@ class smaller_pattern {
 public:
 
     smaller_pattern(ast_manager & m):
-        m_manager(m) {
+        m(m) {
     }
 
     bool operator()(unsigned num_bindings, expr * p1, expr * p2);
@@ -135,7 +135,7 @@ class pattern_inference : public simplifier {
                 m_node(n, m), m_free_vars(vars), m_size(sz) {}
         };
         
-        ast_manager &            m_manager;
+        ast_manager &            m;
         pattern_inference &      m_owner;
         family_id                m_afid;
         unsigned                 m_num_bindings;
@@ -150,7 +150,7 @@ class pattern_inference : public simplifier {
         void save_candidate(expr * n, unsigned delta);
         void reset();
     public:
-        collect(ast_manager & m, pattern_inference & o):m_manager(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
+        collect(ast_manager & m, pattern_inference & o):m(m), m_owner(o), m_afid(m.mk_family_id("arith")) {}
         void operator()(expr * n, unsigned num_bindings);
     };
 
diff --git a/src/ast/simplifier/base_simplifier.h b/src/ast/simplifier/base_simplifier.h
index 4afe5c9d7..5ebcdc30e 100644
--- a/src/ast/simplifier/base_simplifier.h
+++ b/src/ast/simplifier/base_simplifier.h
@@ -26,11 +26,14 @@ Notes:
 */
 class base_simplifier {
 protected:
-    ast_manager &                  m_manager;
+    ast_manager &                  m;
     expr_map                       m_cache;
     ptr_vector<expr>               m_todo;
 
-    void cache_result(expr * n, expr * r, proof * p) { m_cache.insert(n, r, p); }
+    void cache_result(expr * n, expr * r, proof * p) { 
+        m_cache.insert(n, r, p); 
+        SASSERT(is_rewrite_proof(n, r, p));
+    }
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.flush(); }
     void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
@@ -44,11 +47,21 @@ protected:
 
 public:
     base_simplifier(ast_manager & m):
-        m_manager(m),
+        m(m),
         m_cache(m, m.fine_grain_proofs()) {
     }
     bool is_cached(expr * n) const {  return m_cache.contains(n); }
-    ast_manager & get_manager() { return m_manager; }
+    ast_manager & get_manager() { return m; }
+
+    bool is_rewrite_proof(expr* n, expr* r, proof* p) {
+        if (p && 
+            !(m.has_fact(p) && 
+              (m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) && 
+              to_app(m.get_fact(p))->get_arg(0) == n && 
+              to_app(m.get_fact(p))->get_arg(1) == r)) return false;
+        
+        return (!m.fine_grain_proofs() || p || (n == r));
+    }
 };
 
 #endif /* _BASE_SIMPLIFIER_H_ */
diff --git a/src/ast/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp
index 5c19a245e..fc4e7534b 100644
--- a/src/ast/simplifier/bv_elim.cpp
+++ b/src/ast/simplifier/bv_elim.cpp
@@ -100,11 +100,11 @@ bool bv_elim_star::visit_quantifier(quantifier* q) {
 }
 
 void bv_elim_star::reduce1_quantifier(quantifier* q) {
-    quantifier_ref r(m_manager);
-    proof_ref pr(m_manager);
+    quantifier_ref r(m);
+    proof_ref pr(m);
     m_bv_elim.elim(q, r);
-    if (m_manager.fine_grain_proofs()) {
-        pr = m_manager.mk_rewrite(q, r.get());
+    if (m.fine_grain_proofs()) {
+        pr = m.mk_rewrite(q, r.get());
     }
     else {
         pr = 0;
diff --git a/src/ast/simplifier/elim_bounds.cpp b/src/ast/simplifier/elim_bounds.cpp
index ce15d9eb1..41ce18549 100644
--- a/src/ast/simplifier/elim_bounds.cpp
+++ b/src/ast/simplifier/elim_bounds.cpp
@@ -203,20 +203,20 @@ void elim_bounds_star::reduce1_quantifier(quantifier * q) {
         cache_result(q, q, 0); 
         return;
     }
-    quantifier_ref new_q(m_manager);
+    quantifier_ref new_q(m);
     expr * new_body = 0;
     proof * new_pr;
     get_cached(q->get_expr(), new_body, new_pr);
-    new_q = m_manager.update_quantifier(q, new_body);
-    expr_ref r(m_manager);
+    new_q = m.update_quantifier(q, new_body);
+    expr_ref r(m);
     m_elim(new_q, r);
     if (q == r.get()) {
         cache_result(q, q, 0);
         return;
     }
-    proof_ref pr(m_manager);
-    if (m_manager.fine_grain_proofs())
-        pr = m_manager.mk_rewrite(q, r); // TODO: improve justification
+    proof_ref pr(m);
+    if (m.fine_grain_proofs())
+        pr = m.mk_rewrite(q, r); // TODO: improve justification
     cache_result(q, r, pr);
 }
 
diff --git a/src/ast/simplifier/pull_ite_tree.cpp b/src/ast/simplifier/pull_ite_tree.cpp
index 080dd5545..05bb3d885 100644
--- a/src/ast/simplifier/pull_ite_tree.cpp
+++ b/src/ast/simplifier/pull_ite_tree.cpp
@@ -187,7 +187,7 @@ pull_ite_tree_star::pull_ite_tree_star(ast_manager & m, simplifier & s):
 
 bool pull_ite_tree_star::get_subst(expr * n, expr_ref & r, proof_ref & p) {
     if (is_app(n) && is_target(to_app(n))) {
-        app_ref tmp(m_manager);
+        app_ref tmp(m);
         m_proc(to_app(n), tmp, p);
         r = tmp;
         return true;
@@ -199,10 +199,10 @@ bool pull_cheap_ite_tree_star::is_target(app * n) const {
     bool r = 
         n->get_num_args() == 2 &&
         n->get_family_id() != null_family_id &&
-        m_manager.is_bool(n) &&
-        (m_manager.is_value(n->get_arg(0)) || m_manager.is_value(n->get_arg(1))) &&
-        (m_manager.is_term_ite(n->get_arg(0)) || m_manager.is_term_ite(n->get_arg(1)));
-    TRACE("pull_ite_target", tout << mk_pp(n, m_manager) << "\nresult: " << r << "\n";);
+        m.is_bool(n) &&
+        (m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) &&
+        (m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1)));
+    TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";);
     return r;
 }
 
diff --git a/src/ast/simplifier/push_app_ite.cpp b/src/ast/simplifier/push_app_ite.cpp
index cec84d1f5..e33f0d094 100644
--- a/src/ast/simplifier/push_app_ite.cpp
+++ b/src/ast/simplifier/push_app_ite.cpp
@@ -34,7 +34,7 @@ push_app_ite::~push_app_ite() {
 
 int push_app_ite::has_ite_arg(unsigned num_args, expr * const * args) {
     for (unsigned i = 0; i < num_args; i++)
-        if (m_manager.is_ite(args[i]))
+        if (m.is_ite(args[i]))
             return i;
     return -1;
 }
@@ -53,10 +53,10 @@ void push_app_ite::apply(func_decl * decl, unsigned num_args, expr * const * arg
     expr ** args_prime      = const_cast<expr**>(args);
     expr * old              = args_prime[ite_arg_idx];
     args_prime[ite_arg_idx] = t;
-    expr_ref t_new(m_manager);
+    expr_ref t_new(m);
     apply(decl, num_args, args_prime, t_new);
     args_prime[ite_arg_idx] = e;
-    expr_ref e_new(m_manager);
+    expr_ref e_new(m);
     apply(decl, num_args, args_prime, e_new);
     args_prime[ite_arg_idx] = old;
     expr * new_args[3] = { c, t_new, e_new };
@@ -67,11 +67,11 @@ void push_app_ite::apply(func_decl * decl, unsigned num_args, expr * const * arg
    \brief Default (conservative) implementation. Return true if there one and only one ite-term argument.
 */
 bool push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * const * args) {
-    if (m_manager.is_ite(decl))
+    if (m.is_ite(decl))
         return false;
     bool found_ite = false;
     for (unsigned i = 0; i < num_args; i++) {
-        if (m_manager.is_ite(args[i]) && !m_manager.is_bool(args[i])) {
+        if (m.is_ite(args[i]) && !m.is_bool(args[i])) {
             if (found_ite) {
                 if (m_conservative)
                     return false;
@@ -83,7 +83,7 @@ bool push_app_ite::is_target(func_decl * decl, unsigned num_args, expr * const *
     }
     CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n";
           tout << decl->get_name();
-          for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m_manager);
+          for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m);
           tout << "\n";);
     return found_ite;
 }
@@ -94,19 +94,19 @@ void push_app_ite::operator()(expr * s, expr_ref & r, proof_ref & p) {
     reduce_core(s);
     get_cached(s, result, result_proof);
     r = result;
-    switch (m_manager.proof_mode()) {
+    switch (m.proof_mode()) {
     case PGM_DISABLED:
-        p = m_manager.mk_undef_proof();
+        p = m.mk_undef_proof();
         break;
     case PGM_COARSE:
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else
-            p = m_manager.mk_rewrite_star(s, result, 0, 0);
+            p = m.mk_rewrite_star(s, result, 0, 0);
         break;
     case PGM_FINE:
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else
             p = result_proof;
         break;
@@ -171,24 +171,24 @@ void push_app_ite::reduce1_app(app * n) {
     m_args.reset();
     
     func_decl * decl = n->get_decl();
-    proof_ref p1(m_manager);
+    proof_ref p1(m);
     get_args(n, m_args, p1);
 
-    expr_ref r(m_manager);
+    expr_ref r(m);
     if (is_target(decl, m_args.size(), m_args.c_ptr()))
         apply(decl, m_args.size(), m_args.c_ptr(), r);
     else
         mk_app(decl, m_args.size(), m_args.c_ptr(), r);
     
-    if (!m_manager.fine_grain_proofs())
+    if (!m.fine_grain_proofs())
         cache_result(n, r, 0);
     else {
-        expr * s = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+        expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
         proof * p;
         if (n == r)
             p = 0;
         else if (r != s) 
-            p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(s, r));
+            p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
         else
             p = p1;
         cache_result(n, r, p);
@@ -200,8 +200,8 @@ void push_app_ite::reduce1_quantifier(quantifier * q) {
     proof * new_body_pr;
     get_cached(q->get_expr(), new_body, new_body_pr);
     
-    quantifier * new_q = m_manager.update_quantifier(q, new_body);
-    proof *      p     = q == new_q ? 0 : m_manager.mk_quant_intro(q, new_q, new_body_pr);   
+    quantifier * new_q = m.update_quantifier(q, new_body);
+    proof *      p     = q == new_q ? 0 : m.mk_quant_intro(q, new_q, new_body_pr);   
     cache_result(q, new_q, p);
 }
 
diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp
index c9f72f4d5..fcd4e91b6 100644
--- a/src/ast/simplifier/simplifier.cpp
+++ b/src/ast/simplifier/simplifier.cpp
@@ -61,16 +61,17 @@ void simplifier::enable_ac_support(bool flag) {
 */
 void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
     m_need_reset = true;
+    expr  * s_orig = s;
     expr  * old_s;
     expr  * result;
     proof * result_proof;
-    switch (m_manager.proof_mode()) {
+    switch (m.proof_mode()) {
     case PGM_DISABLED: // proof generation is disabled.
         reduce_core(s); 
         // after executing reduce_core, the result of the simplification is in the cache
         get_cached(s, result, result_proof);
         r = result;
-        p = m_manager.mk_undef_proof();
+        p = m.mk_undef_proof();
         break;
     case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r.
         m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. 
@@ -78,10 +79,10 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
         get_cached(s, result, result_proof);
         r = result;
         if (result == s)
-            p = m_manager.mk_reflexivity(s);
+            p = m.mk_reflexivity(s);
         else {
             remove_duplicates(m_subst_proofs);
-            p = m_manager.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
+            p = m.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
         }
         break;
     case PGM_FINE: // fine grain proofs... in this mode, every proof step (or most of them) is described.
@@ -90,17 +91,20 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
         // keep simplyfing until no further simplifications are possible.
         while (s != old_s) {
             TRACE("simplifier", tout << "simplification pass... " << s->get_id() << "\n";);
-            TRACE("simplifier_loop", tout << mk_ll_pp(s, m_manager) << "\n";);
+            TRACE("simplifier_loop", tout << mk_ll_pp(s, m) << "\n";);
             reduce_core(s);
             get_cached(s, result, result_proof);
-            if (result_proof != 0)
+            SASSERT(is_rewrite_proof(s, result, result_proof));
+            if (result_proof != 0) {
                 m_proofs.push_back(result_proof);
+            }
             old_s = s;
             s     = result;
         }
         SASSERT(s != 0);
         r = s;
-        p = m_proofs.empty() ? m_manager.mk_reflexivity(s) : m_manager.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
+        p = m_proofs.empty() ? m.mk_reflexivity(s) : m.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
+        SASSERT(is_rewrite_proof(s_orig, r, p));
         break;
     default:
         UNREACHABLE();
@@ -259,9 +263,9 @@ void simplifier::reduce1(expr * n) {
    specific simplifications via plugins.
 */
 void simplifier::reduce1_app(app * n) {
-    expr_ref r(m_manager);
-    proof_ref p(m_manager);
-    TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m_manager) << "\n";);
+    expr_ref r(m);
+    proof_ref p(m);
+    TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m) << "\n";);
     if (get_subst(n, r, p)) {
         TRACE("reduce", tout << "applying substitution...\n";);
         cache_result(n, r, p);
@@ -279,7 +283,7 @@ void simplifier::reduce1_app(app * n) {
 void simplifier::reduce1_app_core(app * n) {
     m_args.reset();
     func_decl * decl = n->get_decl();
-    proof_ref p1(m_manager);
+    proof_ref p1(m);
     // Stores the new arguments of n in m_args.
     // Let n be of the form
     // (decl arg_0 ... arg_{n-1})
@@ -296,23 +300,23 @@ void simplifier::reduce1_app_core(app * n) {
     //   If none of the arguments have been simplified, and n is not a theory symbol,
     //   Then no simplification is possible, and we can cache the result of the simplification of n as n.
     if (has_new_args || decl->get_family_id() != null_family_id) {
-        expr_ref r(m_manager);
-        TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m_manager););
+        expr_ref r(m);
+        TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m););
         // the method mk_app invokes get_subst and plugins to simplify
         // (decl arg_0' ... arg_{n-1}')
         mk_app(decl, m_args.size(), m_args.c_ptr(), r);
-        if (!m_manager.fine_grain_proofs()) {
+        if (!m.fine_grain_proofs()) {
             cache_result(n, r, 0);
         }
         else {
-            expr * s = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+            expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
             proof * p;
             if (n == r)
                 p = 0;
             else if (r != s) 
                 // we use a "theory rewrite generic proof" to justify the step
                 // s = (decl arg_0' ... arg_{n-1}') --> r
-                p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(s, r));
+                p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
             else
                 p = p1;
             cache_result(n, r, p);
@@ -354,11 +358,11 @@ bool is_ac_vector(app * n) {
 }
 
 void simplifier::reduce1_ac_app_core(app * n) {
-    app_ref    n_c(m_manager);
-    proof_ref  p1(m_manager);
+    app_ref    n_c(m);
+    proof_ref  p1(m);
     mk_ac_congruent_term(n, n_c, p1);
-    TRACE("ac", tout << "expr:\n" << mk_pp(n, m_manager) << "\ncongruent term:\n" << mk_pp(n_c, m_manager) << "\n";);
-    expr_ref r(m_manager); 
+    TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";);
+    expr_ref r(m); 
     func_decl * decl = n->get_decl();
     family_id fid    = decl->get_family_id();
     plugin * p       = get_plugin(fid);
@@ -376,7 +380,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
             // done...
         }
         else {
-            r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
+            r = m.mk_app(decl, m_args.size(), m_args.c_ptr());
         }
     }
     else {
@@ -385,7 +389,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
         get_ac_args(n_c, m_args, m_mults);
         TRACE("ac", tout << "AC args:\n";
               for (unsigned i = 0; i < m_args.size(); i++) {
-                  tout << mk_pp(m_args[i], m_manager) << " * " << m_mults[i] << "\n";
+                  tout << mk_pp(m_args[i], m) << " * " << m_mults[i] << "\n";
               });
         if (p != 0 && p->reduce(decl, m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), r)) {
             // done...
@@ -393,12 +397,12 @@ void simplifier::reduce1_ac_app_core(app * n) {
         else {
             ptr_buffer<expr> new_args;
             expand_args(m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), new_args);
-            r = m_manager.mk_app(decl, new_args.size(), new_args.c_ptr());
+            r = m.mk_app(decl, new_args.size(), new_args.c_ptr());
         }
     }
-    TRACE("ac", tout << "AC result:\n" << mk_pp(r, m_manager) << "\n";);
+    TRACE("ac", tout << "AC result:\n" << mk_pp(r, m) << "\n";);
 
-    if (!m_manager.fine_grain_proofs()) {
+    if (!m.fine_grain_proofs()) {
         cache_result(n, r, 0);
     }
     else {
@@ -406,7 +410,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
         if (n == r.get())
             p = 0;
         else if (r.get() != n_c.get()) 
-            p = m_manager.mk_transitivity(p1, m_manager.mk_rewrite(n_c, r));
+            p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r));
         else
             p = p1;
         cache_result(n, r, p);
@@ -416,8 +420,8 @@ void simplifier::reduce1_ac_app_core(app * n) {
 static unsigned g_rewrite_lemma_id = 0;
 
 void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result) {
-    expr_ref arg(m_manager);
-    arg = m_manager.mk_app(decl, num_args, args);
+    expr_ref arg(m);
+    arg = m.mk_app(decl, num_args, args);
     if (arg.get() != result) {
         char buffer[128];
 #ifdef _WINDOWS
@@ -425,11 +429,11 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
 #else
         sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id);
 #endif        
-        ast_smt_pp pp(m_manager);
+        ast_smt_pp pp(m);
         pp.set_benchmark_name("rewrite_lemma");
         pp.set_status("unsat");
-        expr_ref n(m_manager);
-        n = m_manager.mk_not(m_manager.mk_eq(arg.get(), result));
+        expr_ref n(m);
+        n = m.mk_not(m.mk_eq(arg.get(), result));
         std::ofstream out(buffer);
         pp.display(out, n);
         out.close();
@@ -445,14 +449,14 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
 */
 void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) {
     m_need_reset = true;
-    if (m_manager.is_eq(decl)) {
-        sort * s = m_manager.get_sort(args[0]);
+    if (m.is_eq(decl)) {
+        sort * s = m.get_sort(args[0]);
         plugin * p = get_plugin(s->get_family_id());
         if (p != 0 && p->reduce_eq(args[0], args[1], result))
             return;
     }
-    else if (m_manager.is_distinct(decl)) {
-        sort * s = m_manager.get_sort(args[0]);
+    else if (m.is_distinct(decl)) {
+        sort * s = m.get_sort(args[0]);
         plugin * p = get_plugin(s->get_family_id());
         if (p != 0 && p->reduce_distinct(num_args, args, result))
             return;
@@ -464,7 +468,7 @@ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args
         //dump_rewrite_lemma(decl, num_args, args, result.get());
         return;
     }
-    result = m_manager.mk_app(decl, num_args, args);
+    result = m.mk_app(decl, num_args, args);
 }
 
 /**
@@ -484,7 +488,7 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
         get_cached(arg, new_arg, arg_proof);
 
         CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), 
-               tout << mk_ll_pp(arg, m_manager) << "\n---->\n" << mk_ll_pp(new_arg, m_manager) << "\n";
+               tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n";
                tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n";
                tout << arg << " " << new_arg << "\n";);
         
@@ -500,11 +504,11 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
         args.push_back(new_arg);
     }
     if (has_new_args) {
-        r = m_manager.mk_app(n->get_decl(), args.size(), args.c_ptr());
+        r = m.mk_app(n->get_decl(), args.size(), args.c_ptr());
         if (m_use_oeq)
-            p = m_manager.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
+            p = m.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
         else
-            p = m_manager.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
+            p = m.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
     }
     else {
         r = n;
@@ -523,8 +527,8 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
 bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
     bool has_new_args  = false;
     unsigned num       = n->get_num_args();
-    if (m_manager.fine_grain_proofs()) {
-        app_ref r(m_manager);
+    if (m.fine_grain_proofs()) {
+        app_ref r(m);
         mk_congruent_term(n, r, p);
         result.append(r->get_num_args(), r->get_args());
         SASSERT(n->get_num_args() == result.size());
@@ -582,7 +586,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                     new_args.push_back(new_arg);
                     if (arg != new_arg)
                         has_new_arg = true;
-                    if (m_manager.fine_grain_proofs()) {
+                    if (m.fine_grain_proofs()) {
                         proof * pr = 0;
                         m_ac_pr_cache.find(to_app(arg), pr);
                         if (pr != 0)
@@ -601,7 +605,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
                 new_args.push_back(new_arg);
                 if (arg != new_arg)
                     has_new_arg = true;
-                if (m_manager.fine_grain_proofs() && pr != 0)
+                if (m.fine_grain_proofs() && pr != 0)
                     new_arg_prs.push_back(pr);
             }
         }
@@ -610,14 +614,14 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
             todo.pop_back();
             if (!has_new_arg) {
                 m_ac_cache.insert(curr, curr);
-                if (m_manager.fine_grain_proofs()) 
+                if (m.fine_grain_proofs()) 
                     m_ac_pr_cache.insert(curr, 0);
             }
             else {
-                app * new_curr = m_manager.mk_app(f, new_args.size(), new_args.c_ptr());
+                app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
                 m_ac_cache.insert(curr, new_curr);
-                if (m_manager.fine_grain_proofs()) {
-                    proof * p = m_manager.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
+                if (m.fine_grain_proofs()) {
+                    proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
                     m_ac_pr_cache.insert(curr, p);
                 }
             }
@@ -628,7 +632,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
     app *   new_n = 0;
     m_ac_cache.find(n, new_n);
     r = new_n;
-    if (m_manager.fine_grain_proofs()) {
+    if (m.fine_grain_proofs()) {
         proof * new_pr = 0;
         m_ac_pr_cache.find(n, new_pr);
         p = new_pr;
@@ -719,7 +723,7 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
     SASSERT(!sorted_exprs.empty());
     SASSERT(sorted_exprs[sorted_exprs.size()-1] == n);
     
-    TRACE("ac", tout << mk_ll_pp(n, m_manager, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
+    TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
           for (unsigned i = 0; i < sorted_exprs.size(); i++) {
               tout << "#" << sorted_exprs[i]->get_id() << " ";
           }
@@ -754,10 +758,10 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
 void simplifier::reduce1_quantifier(quantifier * q) {
     expr *  new_body;
     proof * new_body_pr;
-    SASSERT(is_well_sorted(m_manager, q));
+    SASSERT(is_well_sorted(m, q));
     get_cached(q->get_expr(), new_body, new_body_pr);
 
-    quantifier_ref q1(m_manager);
+    quantifier_ref q1(m);
     proof * p1 = 0;
     
     if (is_quantifier(new_body) && 
@@ -774,7 +778,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
         names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
 
-        q1 = m_manager.mk_quantifier(q->is_forall(),
+        q1 = m.mk_quantifier(q->is_forall(),
                                      sorts.size(),
                                      sorts.c_ptr(),
                                      names.c_ptr(),
@@ -783,13 +787,13 @@ void simplifier::reduce1_quantifier(quantifier * q) {
                                      q->get_qid(),
                                      q->get_skid(),
                                      0, 0, 0, 0);
-        SASSERT(is_well_sorted(m_manager, q1));
+        SASSERT(is_well_sorted(m, q1));
         
-        if (m_manager.fine_grain_proofs()) {
-            quantifier * q0 = m_manager.update_quantifier(q, new_body);
-            proof * p0 = q == q0 ? 0 : m_manager.mk_quant_intro(q, q0, new_body_pr);
-            p1 = m_manager.mk_pull_quant(q0, q1);
-            p1 = m_manager.mk_transitivity(p0, p1);
+        if (m.fine_grain_proofs()) {
+            quantifier * q0 = m.update_quantifier(q, new_body);
+            proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr);
+            p1 = m.mk_pull_quant(q0, q1);
+            p1 = m.mk_transitivity(p0, p1);
         }
     }
     else {
@@ -802,7 +806,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         unsigned num = q->get_num_patterns();
         for (unsigned i = 0; i < num; i++) {
             get_cached(q->get_pattern(i), new_pattern, new_pattern_pr);
-            if (m_manager.is_pattern(new_pattern)) {
+            if (m.is_pattern(new_pattern)) {
                 new_patterns.push_back(new_pattern);
             }            
         }
@@ -815,7 +819,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
         remove_duplicates(new_patterns);
         remove_duplicates(new_no_patterns);
 
-        q1 = m_manager.mk_quantifier(q->is_forall(),
+        q1 = m.mk_quantifier(q->is_forall(),
                                      q->get_num_decls(),
                                      q->get_decl_sorts(),
                                      q->get_decl_names(),
@@ -827,26 +831,26 @@ void simplifier::reduce1_quantifier(quantifier * q) {
                                      new_patterns.c_ptr(),
                                      new_no_patterns.size(),
                                      new_no_patterns.c_ptr());
-        SASSERT(is_well_sorted(m_manager, q1));
+        SASSERT(is_well_sorted(m, q1));
 
-        TRACE("simplifier", tout << mk_pp(q, m_manager) << "\n" << mk_pp(q1, m_manager) << "\n";);
-        if (m_manager.fine_grain_proofs()) {
+        TRACE("simplifier", tout << mk_pp(q, m) << "\n" << mk_pp(q1, m) << "\n";);
+        if (m.fine_grain_proofs()) {
             if (q != q1 && !new_body_pr) {
-                new_body_pr = m_manager.mk_rewrite(q->get_expr(), new_body);
+                new_body_pr = m.mk_rewrite(q->get_expr(), new_body);
             }
-            p1 = q == q1 ? 0 : m_manager.mk_quant_intro(q, q1, new_body_pr);
+            p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr);
         }
     }
     
-    expr_ref r(m_manager);
-    elim_unused_vars(m_manager, q1, r);
+    expr_ref r(m);
+    elim_unused_vars(m, q1, r);
     
     proof * pr = 0;
-    if (m_manager.fine_grain_proofs()) {
+    if (m.fine_grain_proofs()) {
         proof * p2 = 0;
         if (q1.get() != r.get())
-            p2 = m_manager.mk_elim_unused_vars(q1, r);
-        pr = m_manager.mk_transitivity(p1, p2);
+            p2 = m.mk_elim_unused_vars(q1, r);
+        pr = m.mk_transitivity(p1, p2);
     }
 
     cache_result(q, r, pr);
@@ -892,7 +896,7 @@ bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
         m_subst_map->get(n, _r, _p);
         r = _r;
         p = _p;
-        if (m_manager.coarse_grain_proofs()) 
+        if (m.coarse_grain_proofs()) 
             m_subst_proofs.push_back(p);
         return true;
     }
diff --git a/src/ast/simplifier/simplifier.h b/src/ast/simplifier/simplifier.h
index 7c5bc3102..78e28bea9 100644
--- a/src/ast/simplifier/simplifier.h
+++ b/src/ast/simplifier/simplifier.h
@@ -210,7 +210,7 @@ public:
 
     plugin * get_plugin(family_id fid) const { return m_plugins.get_plugin(fid); }
 
-    ast_manager & get_manager() { return m_manager; }
+    ast_manager & get_manager() { return m; }
 
     void borrow_plugins(simplifier const & s);
     void release_plugins();
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 48fff7f61..7372fdc2c 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2435,7 +2435,6 @@ namespace qe {
             cache_result(q, q, 0); 
             return;
         }
-        ast_manager& m = m_manager;
 
         quantifier_ref new_q(m);
         expr * new_body = 0;
@@ -2461,7 +2460,6 @@ namespace qe {
     }
 
     void expr_quant_elim_star1::reduce_with_assumption(expr* ctx, expr* fml, expr_ref& result) {
-        ast_manager& m = m_manager;
         proof_ref pr(m);
         m_assumption = ctx;
         (*this)(fml, result, pr);
diff --git a/src/smt/elim_term_ite.cpp b/src/smt/elim_term_ite.cpp
index 2e1671f43..74b804c21 100644
--- a/src/smt/elim_term_ite.cpp
+++ b/src/smt/elim_term_ite.cpp
@@ -33,16 +33,16 @@ void elim_term_ite::operator()(expr * n,
     proof * pr2;
     get_cached(n, r2, pr2);
     r = r2;
-    switch (m_manager.proof_mode()) {
+    switch (m.proof_mode()) {
     case PGM_DISABLED:
-        pr = m_manager.mk_undef_proof();
+        pr = m.mk_undef_proof();
         break;
     case PGM_COARSE:
         remove_duplicates(m_coarse_proofs);
-        pr = n == r2 ? m_manager.mk_oeq_reflexivity(n) : m_manager.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
+        pr = n == r2 ? m.mk_oeq_reflexivity(n) : m.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
         break;
     case PGM_FINE:
-        pr = pr2 == 0 ? m_manager.mk_oeq_reflexivity(n) : pr2;
+        pr = pr2 == 0 ? m.mk_oeq_reflexivity(n) : pr2;
         break;
     }
     m_coarse_proofs.reset();
@@ -107,36 +107,36 @@ void elim_term_ite::reduce1_app(app * n) {
     m_args.reset();
     
     func_decl * decl = n->get_decl();
-    proof_ref p1(m_manager);
+    proof_ref p1(m);
     get_args(n, m_args, p1);
-    if (!m_manager.fine_grain_proofs())
+    if (!m.fine_grain_proofs())
         p1 = 0;
 
-    expr_ref r(m_manager);
-    r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
-    if (m_manager.is_term_ite(r)) {
-        expr_ref   new_def(m_manager);
-        proof_ref  new_def_pr(m_manager);
-        app_ref   new_r(m_manager);
-        proof_ref  new_pr(m_manager);
+    expr_ref r(m);
+    r = m.mk_app(decl, m_args.size(), m_args.c_ptr());
+    if (m.is_term_ite(r)) {
+        expr_ref   new_def(m);
+        proof_ref  new_def_pr(m);
+        app_ref   new_r(m);
+        proof_ref  new_pr(m);
         if (m_defined_names.mk_name(r, new_def, new_def_pr, new_r, new_pr)) {
-            CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m_manager) << "\n";);
+            CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m) << "\n";);
             SASSERT(new_def.get() != 0);
             m_new_defs->push_back(new_def);
-            if (m_manager.fine_grain_proofs()) {
+            if (m.fine_grain_proofs()) {
                 m_new_def_proofs->push_back(new_def_pr);
-                new_pr = m_manager.mk_transitivity(p1, new_pr);
+                new_pr = m.mk_transitivity(p1, new_pr);
             }
             else {
                 // [Leo] This looks fishy... why do we add 0 into m_coarse_proofs when fine_grain_proofs are disabled? 
                 new_pr = 0;
-                if (m_manager.proofs_enabled())
+                if (m.proofs_enabled())
                     m_coarse_proofs.push_back(new_pr);
             }
         }
         else {
             SASSERT(new_def.get() == 0);
-            if (!m_manager.fine_grain_proofs())
+            if (!m.fine_grain_proofs())
                 new_pr = 0;
         }
         cache_result(n, new_r, new_pr);
@@ -151,8 +151,8 @@ void elim_term_ite::reduce1_quantifier(quantifier * q) {
     proof * new_body_pr;
     get_cached(q->get_expr(), new_body, new_body_pr);
     
-    quantifier * new_q = m_manager.update_quantifier(q, new_body);
-    proof *      p     = q == new_q ? 0 : m_manager.mk_oeq_quant_intro(q, new_q, new_body_pr);   
+    quantifier * new_q = m.update_quantifier(q, new_body);
+    proof *      p     = q == new_q ? 0 : m.mk_oeq_quant_intro(q, new_q, new_body_pr);   
     cache_result(q, new_q, p);
 }
 
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 99a36c463..1eb7c7de8 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -883,6 +883,8 @@ namespace smt {
         max_min_t max_min(row & r, bool max, bool& has_shared);
         bool max_min(svector<theory_var> const & vars);
 
+        max_min_t max_min_new(theory_var v, bool max, bool& has_shared);
+
         // -----------------------------------
         //
         // Non linear
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d377fb7ad..f4d908a5c 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -905,28 +905,6 @@ namespace smt {
         r1.reset_var_pos(m_var_pos);
     }
 
-    /**
-       \brief Select tightest variable x_i to pivot with x_j. The goal
-       is to select a x_i such that the value of x_j is increased
-       (decreased) if inc = true (inc = false), and the tableau
-       remains feasible. Store the gain in x_j of the pivoting
-       operation in 'gain'. Note the gain can be too much. That is,
-       it may make x_i infeasible. In this case, instead of pivoting
-       we move x_j to its upper bound (lower bound) when inc = true (inc = false).
-       
-       If no x_i imposes a restriction on x_j, then return null_theory_var.
-       That is, x_j is free to move to its upper bound (lower bound).
-
-       Get the equations for x_j:
-
-       x_i1 = coeff_1 * x_j + rest_1
-       ...
-       x_in = coeff_n * x_j + rest_n
-
-       gain_k := (upper_bound(x_ik) - value(x_ik))/coeff_k
-
-
-    */
     template<typename Ext>
     bool theory_arith<Ext>::is_safe_to_leave(theory_var x, bool inc, bool& has_int, bool& shared) {
         
@@ -958,6 +936,29 @@ namespace smt {
         return !was_unsafe || unbounded;
     }
 
+
+    /**
+       \brief Select tightest variable x_i to pivot with x_j. The goal
+       is to select a x_i such that the value of x_j is increased
+       (decreased) if inc = true (inc = false), and the tableau
+       remains feasible. Store the gain in x_j of the pivoting
+       operation in 'gain'. Note the gain can be too much. That is,
+       it may make x_i infeasible. In this case, instead of pivoting
+       we move x_j to its upper bound (lower bound) when inc = true (inc = false).
+       
+       If no x_i imposes a restriction on x_j, then return null_theory_var.
+       That is, x_j is free to move to its upper bound (lower bound).
+
+       Get the equations for x_j:
+
+       x_i1 = coeff_1 * x_j + rest_1
+       ...
+       x_in = coeff_n * x_j + rest_n
+
+       gain_k := (upper_bound(x_ik) - value(x_ik))/coeff_k
+
+    */
+
     template<typename Ext>
     theory_var theory_arith<Ext>::pick_var_to_leave(
         bool has_int, theory_var x_j, bool inc, 
@@ -1458,6 +1459,166 @@ namespace smt {
         return result;
     }
 
+
+#if 0
+    /**
+       \brief Maximize (Minimize) the given temporary row.
+       Return true if succeeded.
+    */
+    template<typename Ext>
+    typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min_new(row & r, bool max, bool& has_shared) {
+        TRACE("max_min", tout << "max_min...\n";);
+        m_stats.m_max_min++;
+        bool skipped_row = false;
+        has_shared = false;
+
+        SASSERT(valid_row_assignment());
+        SASSERT(satisfy_bounds());
+
+        theory_var x_i = null_theory_var;
+        theory_var x_j = null_theory_var;
+        bool inc       = false;
+        numeral a_ij, curr_a_ij, coeff, curr_coeff;
+        inf_numeral gain, curr_gain;
+#ifdef _TRACE
+        unsigned i = 0;
+#endif
+        max_min_t result = BEST_EFFORT;
+        while (true) {
+            x_j = null_theory_var;
+            x_i = null_theory_var;
+            gain.reset();
+            TRACE("opt", tout << "i: " << i << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout); i++;);
+            typename vector<row_entry>::const_iterator it  = r.begin_entries();
+            typename vector<row_entry>::const_iterator end = r.end_entries();
+            for (; it != end; ++it) {  
+                if (it->is_dead()) continue;                                                  
+                theory_var curr_x_j = it->m_var;
+                SASSERT(is_non_base(curr_x_j));
+                curr_coeff    = it->m_coeff;
+                bool curr_inc = curr_coeff.is_pos() ? max : !max; 
+                bool has_int = false;
+                if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j)))
+                    continue; // variable cannot be used for max/min.
+                if (!is_safe_to_leave(curr_x_j, curr_inc, has_int, has_shared)) {
+                    skipped_row = true;
+                    continue;
+                }
+                theory_var curr_x_i = pick_var_to_leave(has_int, curr_x_j, curr_inc, curr_a_ij, curr_gain, skipped_row);
+                if (curr_x_i == null_theory_var) {
+                    TRACE("opt", tout << "unbounded\n";);
+                    // we can increase/decrease curr_x_j as much as we want.
+                    x_i   = null_theory_var; // unbounded
+                    x_j   = curr_x_j;
+                    inc   = curr_inc;
+                    break;
+                }
+                else if (curr_gain > gain) {
+                    x_i   = curr_x_i;
+                    x_j   = curr_x_j;
+                    a_ij  = curr_a_ij;
+                    coeff = curr_coeff;
+                    gain  = curr_gain;
+                    inc   = curr_inc;
+                }
+                else if (curr_gain.is_zero() && (x_i == null_theory_var || curr_x_i < x_i)) {
+                    x_i   = curr_x_i;
+                    x_j   = curr_x_j;
+                    a_ij  = curr_a_ij;
+                    coeff = curr_coeff;
+                    gain  = curr_gain;
+                    inc   = curr_inc;
+                    // continue
+                }
+            }
+
+            TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << gain << "\n";
+                  tout << "skipped row: " << (skipped_row?"yes":"no") << "\n";
+                  display(tout););
+            
+            if (x_j == null_theory_var) {
+                TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
+                SASSERT(valid_row_assignment());
+                SASSERT(satisfy_bounds());
+                result = skipped_row?BEST_EFFORT:OPTIMIZED;
+                break; 
+            }
+            
+            if (x_i == null_theory_var) {
+                // can increase/decrease x_j as much as we want.
+                if (inc && upper(x_j) && !skipped_row) {
+                    update_value(x_j, upper_bound(x_j) - get_value(x_j));
+                    TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
+                    SASSERT(valid_row_assignment());
+                    SASSERT(satisfy_bounds());
+                    SASSERT(satisfy_integrality());
+                    continue;
+                }
+                if (!inc && lower(x_j) && !skipped_row) {
+                    update_value(x_j, lower_bound(x_j) - get_value(x_j));
+                    TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
+                    SASSERT(valid_row_assignment());
+                    SASSERT(satisfy_bounds());
+                    SASSERT(satisfy_integrality());
+                    continue;
+                }
+                result = skipped_row?BEST_EFFORT:UNBOUNDED;
+                break;
+            }
+            
+            if (!is_fixed(x_j) && is_bounded(x_j) && !skipped_row && (upper_bound(x_j) - lower_bound(x_j) <= gain)) {
+                // can increase/decrease x_j up to upper/lower bound.
+                if (inc) {
+                    update_value(x_j, upper_bound(x_j) - get_value(x_j));
+                    TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
+                }
+                else {
+                    update_value(x_j, lower_bound(x_j) - get_value(x_j));
+                    TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
+                }
+                SASSERT(valid_row_assignment());
+                SASSERT(satisfy_bounds());
+                SASSERT(satisfy_integrality());
+                continue;
+            }
+            
+            TRACE("opt", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n";
+                  if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " ";
+                  if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " ";
+                  tout << "value x_i: " << get_value(x_i) << "\n";
+                  if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " ";
+                  if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
+                  tout << "value x_j: " << get_value(x_j) << "\n";
+                  );
+            pivot<true>(x_i, x_j, a_ij, false);
+            
+            
+            SASSERT(is_non_base(x_i));
+            SASSERT(is_base(x_j));
+            
+            bool move_xi_to_lower;
+            if (inc) 
+                move_xi_to_lower = a_ij.is_pos();
+            else
+                move_xi_to_lower = a_ij.is_neg();
+            if (!move_to_bound(x_i, move_xi_to_lower)) {
+                result = BEST_EFFORT;
+                break;
+            }
+        
+            row & r2 = m_rows[get_var_row(x_j)];
+            coeff.neg();
+            add_tmp_row(r, coeff, r2);
+            SASSERT(r.get_idx_of(x_j) == -1);
+            SASSERT(valid_row_assignment());
+            SASSERT(satisfy_bounds());
+            SASSERT(satisfy_integrality());
+        }
+        TRACE("opt", display(tout););
+        return result;
+    }
+#endif
+
     /**
        Move the variable x_i maximally towards its bound as long as 
        bounds of other variables are not violated.