diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index a66ddd967..6c2b1c77a 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -389,16 +389,16 @@ public:
     app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }
     app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); }
 
-    app * mk_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
-    app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
-    app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
+    app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); }
+    app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); }
+    app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); }
 
-    app * mk_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
-    app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
-    app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
-    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
-    app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
-    app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
+    app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); }
+    app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); }
+    app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); }
+    app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); }
+    app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); }
+    app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); }
     app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); }
     app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); }
     app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); }
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 4632b6604..b5c79f662 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -784,6 +784,12 @@ bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_si
     return true;
 }
 
+bool bv_recognizers::is_numeral(expr const * n, rational & val) const {
+    unsigned bv_size = 0;
+    return is_numeral(n, val, bv_size);
+}
+
+
 bool bv_recognizers::is_allone(expr const * e) const {
     rational r;
     unsigned bv_size;
@@ -847,7 +853,7 @@ bv_util::bv_util(ast_manager & m):
     m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
 }
 
-app * bv_util::mk_numeral(rational const & val, sort* s) {
+app * bv_util::mk_numeral(rational const & val, sort* s) const {
     if (!is_bv_sort(s)) {
         return 0;
     }
@@ -855,7 +861,7 @@ app * bv_util::mk_numeral(rational const & val, sort* s) {
     return mk_numeral(val, bv_size);
 }
 
-app * bv_util::mk_numeral(rational const & val, unsigned bv_size) {
+app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
     parameter p1(val);
     parameter p[2] = { p1, parameter(static_cast<int>(bv_size)) };
     return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 5e533cd98..a4ea7af80 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -293,6 +293,7 @@ public:
     family_id get_fid() const { return m_afid; }
     family_id get_family_id() const { return get_fid(); }
 
+    bool is_numeral(expr const * n, rational & val) const;
     bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
     bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); }
     bool is_allone(expr const * e) const;
@@ -381,9 +382,9 @@ public:
 
     ast_manager & get_manager() const { return m_manager; }
 
-    app * mk_numeral(rational const & val, sort* s);
-    app * mk_numeral(rational const & val, unsigned bv_size);
-    app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); }
+    app * mk_numeral(rational const & val, sort* s) const;
+    app * mk_numeral(rational const & val, unsigned bv_size) const;
+    app * mk_numeral(uint64 u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui64()), bv_size); }
     sort * mk_sort(unsigned bv_size);
 
     unsigned get_bv_size(sort const * s) const {
diff --git a/src/ast/macros/macro_finder.cpp b/src/ast/macros/macro_finder.cpp
index 285c0e5fb..1d441aee7 100644
--- a/src/ast/macros/macro_finder.cpp
+++ b/src/ast/macros/macro_finder.cpp
@@ -48,14 +48,12 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
 bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
     if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
         return false;
-    arith_simplifier_plugin * as = get_arith_simp();
-    arith_util & autil = as->get_arith_util();
     expr * body        = to_quantifier(n)->get_expr();
     unsigned num_decls = to_quantifier(n)->get_num_decls();
     
-    if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
+    if (!m_autil.is_le(body) && !m_autil.is_ge(body) && !m_manager.is_eq(body))
         return false;
-    if (!as->is_add(to_app(body)->get_arg(0)))
+    if (!m_autil.is_add(to_app(body)->get_arg(0)))
         return false;
     app_ref head(m_manager);
     expr_ref def(m_manager);
@@ -66,10 +64,10 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     
     if (!inv || m_manager.is_eq(body))
         new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
-    else if (as->is_le(body))
-        new_body = autil.mk_ge(head, def);
+    else if (m_autil.is_le(body))
+        new_body = m_autil.mk_ge(head, def);
     else
-        new_body = autil.mk_le(head, def);
+        new_body = m_autil.mk_le(head, def);
 
     quantifier_ref new_q(m_manager); 
     new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
@@ -88,10 +86,9 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
     func_decl * k   = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
     app * k_app     = m_manager.mk_app(k, head->get_num_args(), head->get_args());
     expr_ref_buffer new_rhs_args(m_manager);
-    expr_ref new_rhs2(m_manager);
-    as->mk_add(def, k_app, new_rhs2);
+    expr_ref new_rhs2(m_autil.mk_add(def, k_app), m_manager);
     expr * body1    = m_manager.mk_eq(head, new_rhs2);
-    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, as->mk_numeral(rational(0)));
+    expr * body2    = m_manager.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
     quantifier * q1 = m_manager.update_quantifier(new_q, body1);
     expr * patterns[1] = { m_manager.mk_pattern(k_app) };
     quantifier * q2 = m_manager.update_quantifier(new_q, 1, patterns, body2);
@@ -158,7 +155,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
 macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
     m_manager(m),
     m_macro_manager(mm),
-    m_util(mm.get_util()) {
+    m_util(mm.get_util()),
+    m_autil(m) {
 }
 
 macro_finder::~macro_finder() {
diff --git a/src/ast/macros/macro_finder.h b/src/ast/macros/macro_finder.h
index 7f1b27f0e..5807573ae 100644
--- a/src/ast/macros/macro_finder.h
+++ b/src/ast/macros/macro_finder.h
@@ -20,7 +20,6 @@ Revision History:
 #define MACRO_FINDER_H_
 
 #include "ast/macros/macro_manager.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
 
 
 bool is_macro_head(expr * n, unsigned num_decls);
@@ -37,7 +36,7 @@ class macro_finder {
     ast_manager &               m_manager; 
     macro_manager &             m_macro_manager;
     macro_util &                m_util;
-    arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
+    arith_util                  m_autil;
     bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
     bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index bd330a2de..f26a87445 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -28,7 +28,7 @@ Revision History:
 macro_manager::macro_manager(ast_manager & m, simplifier & s):
     m_manager(m),
     m_simplifier(s),
-    m_util(m, s),
+    m_util(m),
     m_decls(m),
     m_macros(m),
     m_macro_prs(m),
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 35f2fbcfb..b7eb9657f 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -29,16 +29,17 @@ Revision History:
 #include "ast/well_sorted.h"
 #include "ast/rewriter/bool_rewriter.h"
 
-macro_util::macro_util(ast_manager & m, simplifier & s):
+macro_util::macro_util(ast_manager & m):
     m_manager(m),
     m_bv(m),
-    m_simplifier(s),
-    m_arith_simp(0),
-    m_bv_simp(0),
+    m_arith(m),
+    m_arith_rw(m),
+    m_bv_rw(m),
     m_forbidden_set(0),
     m_curr_clause(0) {
 }
 
+#if 0
 arith_simplifier_plugin * macro_util::get_arith_simp() const {
     if (m_arith_simp == 0) {
         const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
@@ -54,7 +55,7 @@ bv_simplifier_plugin * macro_util::get_bv_simp() const {
     SASSERT(m_bv_simp != 0);
     return m_bv_simp;
 }
-
+#endif
 
 bool macro_util::is_bv(expr * n) const {
     return m_bv.is_bv(n);
@@ -65,32 +66,41 @@ bool macro_util::is_bv_sort(sort * s) const {
 }
 
 bool macro_util::is_add(expr * n) const {
-    return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n);
+    return m_arith.is_add(n) || m_bv.is_bv_add(n);
 }
 
 bool macro_util::is_times_minus_one(expr * n, expr * & arg) const {
-    return get_arith_simp()->is_times_minus_one(n, arg) || get_bv_simp()->is_times_minus_one(n, arg);
+    return m_arith_rw.is_times_minus_one(n, arg) || m_bv_rw.is_times_minus_one(n, arg);
 }
 
 bool macro_util::is_le(expr * n) const {
-    return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+    return m_arith.is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
 }
 
 bool macro_util::is_le_ge(expr * n) const {
-    return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
+    return m_arith.is_ge(n) || m_arith.is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n);
 }
 
-poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const {
-    if (is_bv_sort(s))
-        return get_bv_simp();
-    else
-        return get_arith_simp();
+bool macro_util::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
+    return m_arith_rw.is_var_plus_ground(n, inv, v, t) || m_bv_rw.is_var_plus_ground(n, inv, v, t);
+}
+
+bool macro_util::is_zero_safe(expr * n) const {
+    if (m_bv_rw.is_bv(n)) {
+        return m_bv.is_zero(n);
+    }
+    else {
+        return m_arith_rw.is_zero(n);
+    }
 }
 
 app * macro_util::mk_zero(sort * s) const {
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
-    ps->set_curr_sort(s);
-    return ps->mk_zero();
+    if (m_bv.is_bv_sort(s)) {
+        return m_bv.mk_numeral(rational(0), s);
+    }
+    else {
+        return m_arith.mk_numeral(rational(0), s);
+    }
 }
 
 void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
@@ -98,7 +108,7 @@ void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const {
         r = m_bv.mk_bv_sub(t1, t2);
     }
     else {
-        get_arith_simp()->mk_sub(t1, t2, r);
+        r = m_arith.mk_sub(t1, t2);
     }
 }
 
@@ -107,18 +117,32 @@ void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const {
         r = m_bv.mk_bv_add(t1, t2);
     }
     else {
-        get_arith_simp()->mk_add(t1, t2, r);
+        r = m_arith.mk_add(t1, t2);
     }
 }
 
 void macro_util::mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const {
-    if (num_args == 0) {
+    switch (num_args) {
+    case 0: 
         r = mk_zero(s);
-        return;
+        break;
+    case 1:
+        r = args[0];
+        break;
+    default:
+        if (m_bv.is_bv_sort(s)) {
+            r = args[0];
+            while (num_args >= 2) {
+                --num_args;
+                ++args;
+                r = m_bv.mk_bv_add(r, args[0]);
+            }
+        }
+        else {
+            r = m_arith.mk_add(num_args, args);
+        }
+        break;
     }
-    poly_simplifier_plugin * ps = get_poly_simp_for(s);
-    ps->set_curr_sort(s);
-    ps->mk_add(num_args, args, r);
 }
 
 /**
@@ -241,13 +265,12 @@ bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) c
 
 bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const {
     // TODO: obsolete... we should move to collect_arith_macro_candidates
-    arith_simplifier_plugin * as = get_arith_simp();
-    if (!m_manager.is_eq(n) && !as->is_le(n) && !as->is_ge(n))
+    if (!m_manager.is_eq(n) && !m_arith.is_le(n) && !m_arith.is_ge(n))
         return false;
     expr * lhs = to_app(n)->get_arg(0);
     expr * rhs = to_app(n)->get_arg(1);
 
-    if (!as->is_numeral(rhs))
+    if (!m_arith.is_numeral(rhs))
         return false;
 
     inv = false;
@@ -272,7 +295,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
             !poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
             h = arg;
         }
-        else if (h == 0 && as->is_times_minus_one(arg, neg_arg) &&
+        else if (h == 0 && m_arith_rw.is_times_minus_one(arg, neg_arg) &&
                  is_macro_head(neg_arg, num_decls) &&
                  !is_forbidden(to_app(neg_arg)->get_decl()) &&
                  !poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
@@ -287,11 +310,11 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
         return false;
     head = to_app(h);
     expr_ref tmp(m_manager);
-    as->mk_add(args.size(), args.c_ptr(), tmp);
+    tmp = m_arith.mk_add(args.size(), args.c_ptr());
     if (inv)
-        as->mk_sub(tmp, rhs, def);
+        def = m_arith.mk_sub(tmp, rhs);
     else
-        as->mk_sub(rhs, tmp, def);
+        def = m_arith.mk_sub(rhs, tmp);
     return true;
 }
 
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index d76f2f0d3..91d96cc5e 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -22,12 +22,8 @@ Revision History:
 
 #include "ast/ast.h"
 #include "util/obj_hashtable.h"
-#include "ast/simplifier/simplifier.h"
-
-class poly_simplifier_plugin;
-class arith_simplifier_plugin;
-class bv_simplifier_plugin;
-class basic_simplifier_plugin;
+#include "ast/rewriter/arith_rewriter.h"
+#include "ast/rewriter/bv_rewriter.h"
 
 class macro_util {
 public:
@@ -63,9 +59,9 @@ public:
 private:
     ast_manager &               m_manager;
     bv_util                     m_bv;
-    simplifier &                m_simplifier;
-    arith_simplifier_plugin *   m_arith_simp;
-    bv_simplifier_plugin    *   m_bv_simp;
+    arith_util                  m_arith;
+    arith_rewriter              m_arith_rw;
+    bv_rewriter                 m_bv_rw;
     obj_hashtable<func_decl> *  m_forbidden_set;
 
     bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
@@ -94,11 +90,9 @@ private:
 
 
 public:
-    macro_util(ast_manager & m, simplifier & s);
+    macro_util(ast_manager & m);
     void set_forbidden_set(obj_hashtable<func_decl> * s) { m_forbidden_set = s; }
 
-    arith_simplifier_plugin * get_arith_simp() const;
-    bv_simplifier_plugin * get_bv_simp() const;
 
     bool is_macro_head(expr * n, unsigned num_decls) const;
     bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
@@ -113,6 +107,8 @@ public:
         return is_arith_macro(n, num_decls, head, def, inv);
     }
 
+    bool is_zero_safe(expr * n) const;
+    bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
     bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
     bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
 
@@ -137,7 +133,6 @@ public:
     void mk_sub(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(expr * t1, expr * t2, expr_ref & r) const;
     void mk_add(unsigned num_args, expr * const * args, sort * s, expr_ref & r) const;
-    poly_simplifier_plugin * get_poly_simp_for(sort * s) const;
 };
 
 #endif
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index b39adde03..822532532 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -22,10 +22,10 @@ Revision History:
 #include "util/uint_set.h"
 #include "ast/rewriter/var_subst.h"
 
-quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s) :
-  m_manager(m),
+quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm) :
+  m_manager(m), 
   m_macro_manager(mm),
-  m_simplifier(s),
+  m_rewriter(m),
   m_new_vars(m),
   m_new_eqs(m),
   m_new_qsorts(m) {
@@ -299,8 +299,8 @@ void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const
         proof_ref pr(m_manager), ps(m_manager);
         proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
         m_macro_manager.expand_macros(exprs[i], p, r, pr);
-        m_simplifier(r, rs, ps);
-        new_exprs.push_back(rs);
+        m_rewriter(r);
+        new_exprs.push_back(r);
         new_prs.push_back(ps);    
     }
 }
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 3a9b6074e..29efe63c7 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -21,8 +21,7 @@ Revision History:
 
 #include<sstream>
 #include "ast/macros/macro_manager.h"
-#include "ast/simplifier/basic_simplifier_plugin.h"
-#include "ast/simplifier/simplifier.h"
+#include "ast/rewriter/th_rewriter.h"
 
 /**
    \brief Finds quasi macros and applies them.
@@ -32,7 +31,7 @@ class quasi_macros {
 
     ast_manager &             m_manager;
     macro_manager &           m_macro_manager;
-    simplifier &              m_simplifier;
+    th_rewriter               m_rewriter;
     occurrences_map           m_occurrences;
     ptr_vector<expr>          m_todo;    
 
@@ -57,7 +56,7 @@ class quasi_macros {
     void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 
 public:
-    quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
+    quasi_macros(ast_manager & m, macro_manager & mm);
     ~quasi_macros();
     
     /**
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index de849dbd7..5d9fb1d66 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -35,7 +35,6 @@ protected:
     
     bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
-    bool is_zero(expr * n) const { return m_util.is_zero(n); }
     bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); }
     void normalize(numeral & c, sort * s) {}
     app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); }
@@ -45,6 +44,7 @@ protected:
     decl_kind power_decl_kind() const { return OP_POWER; }
 public:
     arith_rewriter_core(ast_manager & m):m_util(m) {}
+    bool is_zero(expr * n) const { return m_util.is_zero(n); }
 };
 
 class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 5d38e4b10..5269f25a8 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -39,7 +39,6 @@ protected:
 
     bool is_numeral(expr * n) const { return Config::is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); }
-    bool is_zero(expr * n) const { return Config::is_zero(n); }
     bool is_minus_one(expr * n) const { return Config::is_minus_one(n); }
     void normalize(numeral & c) { Config::normalize(c, m_curr_sort); }
     app * mk_numeral(numeral const & r) { return Config::mk_numeral(r, m_curr_sort); }
@@ -111,6 +110,9 @@ public:
     bool is_mul(expr * n) const { return is_app_of(n, get_fid(), mul_decl_kind()); }
     bool is_add(func_decl * f) const { return is_decl_of(f, get_fid(), add_decl_kind()); }
     bool is_mul(func_decl * f) const { return is_decl_of(f, get_fid(), mul_decl_kind()); }
+    bool is_times_minus_one(expr * n, expr*& r) const;
+    bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
+
 
     br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
         SASSERT(num_args > 0);
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 5e2e39722..a8d115d64 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -931,3 +931,63 @@ expr* poly_rewriter<Config>::merge_muls(expr* x, expr* y) {
     m1[k] = mk_add_app(2, args);
     return mk_mul_app(k+1, m1.c_ptr());
 }
+
+template<typename Config>
+bool poly_rewriter<Config>::is_times_minus_one(expr * n, expr* & r) const {
+    if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
+        r = to_app(n)->get_arg(1);
+        return true;
+    }
+    return false;
+}
+
+/**
+   \brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
+   \c inv = true will contain true if (- v) is found, and false otherwise.
+*/
+template<typename Config>
+bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
+    if (!is_add(n) || is_ground(n))
+        return false;
+    
+    ptr_buffer<expr> args;
+    v = 0;
+    expr * curr = to_app(n);
+    bool stop = false;
+    inv = false;
+    while (!stop) {
+        expr * arg;
+        expr * neg_arg;
+        if (is_add(curr)) {
+            arg  = to_app(curr)->get_arg(0);
+            curr = to_app(curr)->get_arg(1);
+        }
+        else {
+            arg  = curr;
+            stop = true;
+        }
+        if (is_ground(arg)) {
+            TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m()) << "\n";);
+            args.push_back(arg);
+        }
+        else if (is_var(arg)) {
+            if (v != 0)
+                return false; // already found variable
+            v = to_var(arg);
+        }
+        else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
+            if (v != 0)
+                return false; // already found variable
+            v = to_var(neg_arg);
+            inv = true;
+        }
+        else {
+            return false; // non ground term.
+        }
+    }
+    if (v == 0)
+        return false; // did not find variable
+    SASSERT(!args.empty());
+    mk_add(args.size(), args.c_ptr(), t);
+    return true;
+}
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index cbbb9a6bc..2f55cd704 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -410,7 +410,7 @@ void asserted_formulas::apply_quasi_macros() {
     TRACE("before_quasi_macros", display(tout););
     expr_ref_vector  new_exprs(m);
     proof_ref_vector new_prs(m);      
-    quasi_macros proc(m, m_macro_manager, m_simplifier);    
+    quasi_macros proc(m, m_macro_manager);    
     while (proc(m_asserted_formulas.size() - m_asserted_qhead, 
                 m_asserted_formulas.c_ptr() + m_asserted_qhead, 
                 m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 73d1e9f22..2e6a34557 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -23,8 +23,6 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
-#include "ast/simplifier/arith_simplifier_plugin.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
 #include "ast/normal_forms/pull_quant.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/for_each_expr.h"
@@ -392,9 +390,9 @@ namespace smt {
            The idea is to create node objects based on the information produced by the quantifier_analyzer.
         */
         class auf_solver : public evaluator {
-            ast_manager &             m_manager;
-            arith_simplifier_plugin * m_asimp;
-            bv_simplifier_plugin *    m_bvsimp;
+            ast_manager &             m;
+            arith_util                m_arith;
+            bv_util                   m_bv;
             ptr_vector<node>          m_nodes;
             unsigned                  m_next_node_id;
             key2node                  m_uvars;
@@ -466,16 +464,16 @@ namespace smt {
             }
 
         public:
-            auf_solver(ast_manager & m, simplifier & s):
-                m_manager(m),
+            auf_solver(ast_manager & m):
+                m(m),
+                m_arith(m),
+                m_bv(m),
                 m_next_node_id(0),
                 m_context(0),
                 m_ks(m),
                 m_model(0),
                 m_eval_cache_range(m),
                 m_new_constraints(0) {
-                m_asimp  = static_cast<arith_simplifier_plugin*>(s.get_plugin(m.mk_family_id("arith")));
-                m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.mk_family_id("bv")));
             }
 
             virtual ~auf_solver() {
@@ -488,12 +486,8 @@ namespace smt {
                 m_context = ctx;
             }
             
-            ast_manager & get_manager() const { return m_manager; }
-            
-            arith_simplifier_plugin * get_arith_simp() const { return m_asimp; }
-
-            bv_simplifier_plugin * get_bv_simp() const { return m_bvsimp; }
-            
+            ast_manager & get_manager() const { return m; }
+                        
             void reset() {
                 flush_nodes();
                 m_nodes.reset();
@@ -538,7 +532,7 @@ namespace smt {
             void mk_instantiation_sets() {
                 for (node* curr : m_nodes) {
                     if (curr->is_root()) {
-                        curr->mk_instantiation_set(m_manager);
+                        curr->mk_instantiation_set(m);
                     }
                 }
             }
@@ -554,7 +548,7 @@ namespace smt {
                         for (auto const& kv : elems) {
                             expr * n     = kv.m_key;
                             expr * n_val = eval(n, true);
-                            if (!n_val || !m_manager.is_value(n_val))
+                            if (!n_val || !m.is_value(n_val))
                                 to_delete.push_back(n);
                         }
                         for (expr* e : to_delete) {
@@ -568,7 +562,7 @@ namespace smt {
                 display_key2node(out, m_uvars);
                 display_A_f_is(out);           
                 for (node* n : m_nodes) {
-                    n->display(out, m_manager);
+                    n->display(out, m);
                 }
             }
 
@@ -577,14 +571,14 @@ namespace smt {
                 if (m_eval_cache[model_completion].find(n, r)) {
                     return r;
                 }
-                expr_ref tmp(m_manager);
+                expr_ref tmp(m);
                 if (!m_model->eval(n, tmp, model_completion)) {
                     r = 0;
-                    TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";);
+                    TRACE("model_finder", tout << "eval\n" << mk_pp(n, m) << "\n-----> null\n";);
                 }
                 else {
                     r = tmp;
-                    TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
+                    TRACE("model_finder", tout << "eval\n" << mk_pp(n, m) << "\n----->\n" << mk_pp(r, m) << "\n";);
                 }
                 m_eval_cache[model_completion].insert(n, r);
                 m_eval_cache_range.push_back(r);
@@ -636,7 +630,7 @@ namespace smt {
                     SASSERT(t_val != 0);
                     bool found = false;
                     for (expr* v : ex_vals) {
-                        if (!m_manager.are_distinct(t_val, v)) {
+                        if (!m.are_distinct(t_val, v)) {
                             found = true;
                             break;
                         }
@@ -652,7 +646,7 @@ namespace smt {
             bool is_infinite(sort * s) const {
                 // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
                 return 
-                    !m_manager.is_uninterp(s) &&
+                    !m.is_uninterp(s) &&
                     s->is_infinite();
             }
 
@@ -665,7 +659,7 @@ namespace smt {
                 app * r = 0;
                 if (m_sort2k.find(s, r))
                     return r;
-                r = m_manager.mk_fresh_const("k", s);
+                r = m.mk_fresh_const("k", s);
                 m_model->register_aux_decl(r->get_decl());
                 m_sort2k.insert(s, r);
                 m_ks.push_back(r);
@@ -680,7 +674,7 @@ namespace smt {
                Remark: this method uses get_fresh_value, so it may fail.
             */
             expr * get_k_interp(app * k) {
-                sort * s = m_manager.get_sort(k);
+                sort * s = m.get_sort(k);
                 SASSERT(is_infinite(s));
                 func_decl * k_decl = k->get_decl();
                 expr * r = m_model->get_const_interp(k_decl);
@@ -691,7 +685,7 @@ namespace smt {
                     return 0;
                 m_model->register_decl(k_decl, r);
                 SASSERT(m_model->get_const_interp(k_decl) == r);
-                TRACE("model_finder", tout << mk_pp(r, m_manager) << "\n";);
+                TRACE("model_finder", tout << mk_pp(r, m) << "\n";);
                 return r;
             }
 
@@ -701,18 +695,18 @@ namespace smt {
                It invokes get_k_interp that may fail.
             */
             bool assert_k_diseq_exceptions(app * k, ptr_vector<expr> const & exceptions) {
-                TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m_manager) << "\nexceptions:\n";
-                      for (expr * e : exceptions) tout << mk_pp(e, m_manager) << "\n";);
+                TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m) << "\nexceptions:\n";
+                      for (expr * e : exceptions) tout << mk_pp(e, m) << "\n";);
                 expr * k_interp = get_k_interp(k);
                 if (k_interp == 0)
                     return false;
                 for (expr * ex : exceptions) {
                     expr * ex_val = eval(ex, true);
-                    if (!m_manager.are_distinct(k_interp, ex_val)) {
+                    if (!m.are_distinct(k_interp, ex_val)) {
                         SASSERT(m_new_constraints);
                         // This constraint cannot be asserted into m_context during model construction.
                         // We must save it, and assert it during a restart.
-                        m_new_constraints->push_back(m_manager.mk_not(m_manager.mk_eq(k, ex)));
+                        m_new_constraints->push_back(m.mk_not(m.mk_eq(k, ex)));
                     }
                 }
                 return true;
@@ -735,7 +729,7 @@ namespace smt {
                         return;
                     }
                     sort * s = n->get_sort();
-                    TRACE("model_finder", tout << "trying to create k for " << mk_pp(s, m_manager) << ", is_infinite: " << is_infinite(s) << "\n";);
+                    TRACE("model_finder", tout << "trying to create k for " << mk_pp(s, m) << ", is_infinite: " << is_infinite(s) << "\n";);
                     if (is_infinite(s)) {
                         app * k = get_k_for(s);
                         if (assert_k_diseq_exceptions(k, exceptions)) {
@@ -758,28 +752,33 @@ namespace smt {
             void add_mono_exceptions(node * n) {
                 SASSERT(n->is_mono_proj());
                 sort * s = n->get_sort();
-                arith_simplifier_plugin * as = get_arith_simp();
-                bv_simplifier_plugin    * bs = get_bv_simp();
-                bool is_int = as->is_int_sort(s);
-                bool is_bv  = bs->is_bv_sort(s);
-                if (!is_int && !is_bv)
-                    return;
-                poly_simplifier_plugin * ps = as;
-                if (is_bv)
-                    ps = bs;
-                ps->set_curr_sort(s);
-                expr_ref one(m_manager);
-                one = ps->mk_one();
+                arith_rewriter arw(m);
+                bv_rewriter brw(m);
                 ptr_vector<expr> const & exceptions  = n->get_exceptions();
-                for (expr * e : exceptions) {
-                    expr_ref e_plus_1(m_manager);
-                    expr_ref e_minus_1(m_manager);
-                    TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m_manager) << "\none:\n" << mk_ismt2_pp(one, m_manager) << "\n";);
-                    ps->mk_add(e, one, e_plus_1); 
-                    ps->mk_sub(e, one, e_minus_1);
-                    // Note: exceptions come from quantifiers bodies. So, they have generation 0.
-                    n->insert(e_plus_1, 0);
-                    n->insert(e_minus_1, 0);
+                if (m_arith.is_int(s)) {
+                    expr_ref one(m_arith.mk_int(1), m);
+                    for (expr * e : exceptions) {
+                        expr_ref e_plus_1(m_arith.mk_add(e, one), m);
+                        expr_ref e_minus_1(m_arith.mk_sub(e, one), m);
+                        TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
+                        // Note: exceptions come from quantifiers bodies. So, they have generation 0.
+                        n->insert(e_plus_1, 0);
+                        n->insert(e_minus_1, 0);
+                    }
+                }
+                else if (m_bv.is_bv_sort(s)) {
+                    expr_ref one(m_bv.mk_numeral(rational(1), s), m);
+                    for (expr * e : exceptions) {
+                        expr_ref e_plus_1(m_bv.mk_bv_add(e, one), m);
+                        expr_ref e_minus_1(m_bv.mk_bv_sub(e, one), m);
+                        TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";);
+                        // Note: exceptions come from quantifiers bodies. So, they have generation 0.
+                        n->insert(e_plus_1, 0);
+                        n->insert(e_minus_1, 0);
+                    }
+                }
+                else {
+                    return;
                 }
             }
 
@@ -797,16 +796,17 @@ namespace smt {
                 }
                 TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n";
                       for (expr * v : values) {
-                          tout << mk_pp(v, m_manager) << "\n";
+                          tout << mk_pp(v, m) << "\n";
                       });
             }
 
+            template<class T>
             struct numeral_lt {
-                poly_simplifier_plugin * m_p;
-                numeral_lt(poly_simplifier_plugin * p):m_p(p) {}
-                bool operator()(expr * e1, expr * e2) {
+                T& m_util;
+                numeral_lt(T& a): m_util(a) {}
+                bool operator()(expr* e1, expr* e2) {
                     rational v1, v2;
-                    if (m_p->is_numeral(e1, v1) && m_p->is_numeral(e2, v2)) {
+                    if (m_util.is_numeral(e1, v1) && m_util.is_numeral(e2, v1)) {
                         return v1 < v2;
                     }
                     else {
@@ -815,15 +815,16 @@ namespace smt {
                 }
             };
 
+
             struct signed_bv_lt {
-                bv_simplifier_plugin * m_bs;
+                bv_util& m_bv;
                 unsigned               m_bv_size;
-                signed_bv_lt(bv_simplifier_plugin * bs, unsigned sz):m_bs(bs), m_bv_size(sz) {}
+                signed_bv_lt(bv_util& bv, unsigned sz):m_bv(bv), m_bv_size(sz) {}
                 bool operator()(expr * e1, expr * e2) {
                     rational v1, v2;
-                    if (m_bs->is_numeral(e1, v1) && m_bs->is_numeral(e2, v2)) {
-                        v1 = m_bs->norm(v1, m_bv_size, true);
-                        v2 = m_bs->norm(v2, m_bv_size, true);
+                    if (m_bv.is_numeral(e1, v1) && m_bv.is_numeral(e2, v2)) {
+                        v1 = m_bv.norm(v1, m_bv_size, true);
+                        v2 = m_bv.norm(v2, m_bv_size, true);
                         return v1 < v2;
                     }
                     else {
@@ -834,15 +835,14 @@ namespace smt {
 
             void sort_values(node * n, ptr_buffer<expr> & values) {
                 sort * s = n->get_sort();
-                if (get_arith_simp()->is_arith_sort(s)) {
-                    std::sort(values.begin(), values.end(), numeral_lt(get_arith_simp()));
+                if (m_arith.is_int(s) || m_arith.is_real(s)) {
+                    std::sort(values.begin(), values.end(), numeral_lt<arith_util>(m_arith));
                 }
                 else if (!n->is_signed_proj()) {
-                    std::sort(values.begin(), values.end(), numeral_lt(get_bv_simp()));
+                    std::sort(values.begin(), values.end(), numeral_lt<bv_util>(m_bv));
                 }
                 else {
-                    bv_simplifier_plugin * bs = get_bv_simp();
-                    std::sort(values.begin(), values.end(), signed_bv_lt(bs, bs->get_bv_size(s)));
+                    std::sort(values.begin(), values.end(), signed_bv_lt(m_bv, m_bv.get_bv_size(s)));
                }
             }
 
@@ -853,27 +853,25 @@ namespace smt {
                 if (values.empty()) return;
                 sort_values(n, values);
                 sort * s = n->get_sort();
-                arith_simplifier_plugin * as = get_arith_simp();
-                bv_simplifier_plugin    * bs = get_bv_simp();
-                bool is_arith  = as->is_arith_sort(s);
+                bool is_arith  = m_arith.is_int(s) || m_arith.is_real(s);
                 bool is_signed = n->is_signed_proj();
                 unsigned sz = values.size();
                 SASSERT(sz > 0);
-                func_decl * p = m_manager.mk_fresh_func_decl(1, &s, s);
+                func_decl * p = m.mk_fresh_func_decl(1, &s, s);
                 expr * pi     = values[sz - 1];
-                expr_ref var(m_manager);
-                var = m_manager.mk_var(0, s);
+                expr_ref var(m);
+                var = m.mk_var(0, s);
                 for (unsigned i = sz - 1; i >= 1; i--) {
-                    expr_ref c(m_manager);
+                    expr_ref c(m);
                     if (is_arith) 
-                        as->mk_lt(var, values[i], c);
+                        c = m_arith.mk_lt(var, values[i]);
                     else if (!is_signed)
-                        bs->mk_ult(var, values[i], c);
+                        c = m.mk_not(m_bv.mk_ule(values[i], var));
                     else
-                        bs->mk_slt(var, values[i], c);
-                    pi = m_manager.mk_ite(c, values[i-1], pi);
+                        c = m.mk_not(m_bv.mk_sle(values[i], var));
+                    pi = m.mk_ite(c, values[i-1], pi);
                 }
-                func_interp * rpi = alloc(func_interp, m_manager, 1);
+                func_interp * rpi = alloc(func_interp, m, 1);
                 rpi->set_else(pi);
                 m_model->register_aux_decl(p, rpi);
                 n->set_proj(p);
@@ -884,8 +882,8 @@ namespace smt {
                 ptr_buffer<expr> values;
                 get_instantiation_set_values(n, values);
                 sort * s        = n->get_sort();
-                func_decl *   p = m_manager.mk_fresh_func_decl(1, &s, s);
-                func_interp * pi = alloc(func_interp, m_manager, 1);
+                func_decl *   p = m.mk_fresh_func_decl(1, &s, s);
+                func_interp * pi = alloc(func_interp, m, 1);
                 m_model->register_aux_decl(p, pi);
                 if (n->get_else()) {
                     expr * else_val = eval(n->get_else(), true);
@@ -916,7 +914,7 @@ namespace smt {
                     if (!r.contains(f)) {
                         func_interp * fi = m_model->get_func_interp(f);
                         if (fi == 0) {
-                            fi = alloc(func_interp, m_manager, f->get_arity());
+                            fi = alloc(func_interp, m, f->get_arity());
                             m_model->register_decl(f, fi);
                             SASSERT(fi->is_partial());
                         }
@@ -938,7 +936,7 @@ namespace smt {
                 for (node * n : m_root_nodes) {
                     SASSERT(n->is_root());
                     sort * s = n->get_sort();
-                    if (m_manager.is_uninterp(s) && 
+                    if (m.is_uninterp(s) && 
                         // Making all uninterpreted sorts finite.
                         // n->must_avoid_itself() && 
                         !m_model->is_finite(s)) {
@@ -962,7 +960,7 @@ namespace smt {
                         // If these module values "leak" inside the logical context, they may affect satisfiability.
                         // 
                         sort * ns = n->get_sort();
-                        if (m_manager.is_fully_interp(ns)) {
+                        if (m.is_fully_interp(ns)) {
                             n->insert(m_model->get_some_value(ns), 0);
                         }
                         else {
@@ -973,18 +971,18 @@ namespace smt {
                         sort2elems.insert(n->get_sort(), elems.begin()->m_key);
                     }
                 }
-                expr_ref_vector trail(m_manager);
+                expr_ref_vector trail(m);
                 for (unsigned i = 0; i < need_fresh.size(); ++i) {
                     expr * e;
                     node* n = need_fresh[i];
                     sort* s = n->get_sort();
                     if (!sort2elems.find(s, e)) {
-                        e = m_manager.mk_fresh_const("elem", s);
+                        e = m.mk_fresh_const("elem", s);
                         trail.push_back(e);
                         sort2elems.insert(s, e);
                     }
                     n->insert(e, 0);
-                    TRACE("model_finder", tout << "fresh constant: " << mk_pp(e, m_manager) << "\n";);
+                    TRACE("model_finder", tout << "fresh constant: " << mk_pp(e, m) << "\n";);
                 }
             }
 
@@ -1037,13 +1035,13 @@ namespace smt {
                     if (fi->is_constant())
                         continue; // there is no point in using the projection for fi, since fi is the constant function.
                     
-                    expr_ref_vector args(m_manager);
+                    expr_ref_vector args(m);
                     bool has_proj = false;
                     for (unsigned i = 0; i < arity; i++) {
-                        var * v = m_manager.mk_var(i, f->get_domain(i));
+                        var * v = m.mk_var(i, f->get_domain(i));
                         func_decl * pi = get_f_i_proj(f, i);
                         if (pi != 0) {
-                            args.push_back(m_manager.mk_app(pi, v));
+                            args.push_back(m.mk_app(pi, v));
                             has_proj = true;
                         }
                         else {
@@ -1052,11 +1050,11 @@ namespace smt {
                     }
                     if (has_proj) {
                         // f_aux will be assigned to the old interpretation of f.
-                        func_decl *   f_aux  = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range());
-                        func_interp * new_fi = alloc(func_interp, m_manager, arity);
-                        new_fi->set_else(m_manager.mk_app(f_aux, args.size(), args.c_ptr()));
+                        func_decl *   f_aux  = m.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range());
+                        func_interp * new_fi = alloc(func_interp, m, arity);
+                        new_fi->set_else(m.mk_app(f_aux, args.size(), args.c_ptr()));
                         TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" << 
-                              mk_pp(new_fi->get_else(), m_manager) << "\n";);
+                              mk_pp(new_fi->get_else(), m) << "\n";);
                         m_model->reregister_decl(f, new_fi, f_aux);
                     }
                 }
@@ -1256,21 +1254,21 @@ namespace smt {
                 if (A_f_i == S_j) {
                     // there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset
                     // hope for the best...
-                    arith_simplifier_plugin * as = s.get_arith_simp();
-                    bv_simplifier_plugin * bs    = s.get_bv_simp();
                     node * S_j = s.get_uvar(q, m_var_j);
                     enode_vector::const_iterator it  = ctx->begin_enodes_of(m_f);
                     enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
                     for (; it != end; it++) {
                         enode * n = *it;
                         if (ctx->is_relevant(n)) {
+                            arith_util arith(ctx->get_manager());
+                            bv_util bv(ctx->get_manager());
                             enode * e_arg = n->get_arg(m_arg_i);
                             expr * arg    = e_arg->get_owner();
                             expr_ref arg_minus_k(ctx->get_manager());
-                            if (bs->is_bv(arg))
-                                bs->mk_sub(arg, m_offset, arg_minus_k);
+                            if (bv.is_bv(arg))
+                                arg_minus_k = bv.mk_bv_sub(arg, m_offset);
                             else
-                                as->mk_sub(arg, m_offset, arg_minus_k);
+                                arg_minus_k = arith.mk_sub(arg, m_offset);
                             S_j->insert(arg_minus_k, e_arg->get_generation());
                         }
                     }
@@ -1290,20 +1288,20 @@ namespace smt {
 
             template<bool PLUS>
             void copy_instances(node * from, node * to, auf_solver & s) {
-                arith_simplifier_plugin * as = s.get_arith_simp();
-                bv_simplifier_plugin * bs    = s.get_bv_simp();
-                poly_simplifier_plugin * ps  = as;
-                if (bs->is_bv_sort(from->get_sort()))
-                    ps = bs;
                 instantiation_set const * from_s        = from->get_instantiation_set();
                 obj_map<expr, unsigned> const & elems_s = from_s->get_elems();
+
+                arith_util arith(m_offset.get_manager());
+                bv_util bv(m_offset.get_manager());
+                bool is_bv = bv.is_bv_sort(from->get_sort());
+
                 for (auto const& kv : elems_s) {
                     expr * n = kv.m_key;
                     expr_ref n_k(m_offset.get_manager());
                     if (PLUS)
-                        ps->mk_add(n, m_offset, n_k);
+                        n_k = is_bv ? bv.mk_bv_add(n, m_offset) : arith.mk_add(n, m_offset);
                     else
-                        ps->mk_sub(n, m_offset, n_k);
+                        n_k = is_bv ? bv.mk_bv_sub(n, m_offset) : arith.mk_sub(n, m_offset);
                     to->insert(n_k, kv.m_value);
                 }
             }
@@ -1897,11 +1895,8 @@ namespace smt {
                 m_info->insert_qinfo(qi);
             }
 
-            arith_simplifier_plugin * get_arith_simp() const { return m_mutil.get_arith_simp(); }
-            bv_simplifier_plugin * get_bv_simp() const { return m_mutil.get_bv_simp(); }
-
-            bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) const {
-                return get_arith_simp()->is_var_plus_ground(n, inv, v, t) || get_bv_simp()->is_var_plus_ground(n, inv, v, t);
+            bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
+                return m_mutil.is_var_plus_ground(n, inv, v, t);
             }
 
             bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
@@ -1917,10 +1912,7 @@ namespace smt {
             }
 
             bool is_zero(expr * n) const {
-                if (get_bv_simp()->is_bv(n))
-                    return get_bv_simp()->is_zero_safe(n);
-                else 
-                    return get_arith_simp()->is_zero_safe(n);
+                return m_mutil.is_zero_safe(n);
             }
 
             bool is_times_minus_one(expr * n, expr * & arg) const {
@@ -1951,7 +1943,7 @@ namespace smt {
                 m_mutil.mk_add(t1, t2, r);
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
                 inv = false; // true if invert the sign
                 TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
                 if (is_var(lhs) && is_ground(rhs)) {
@@ -1986,12 +1978,12 @@ namespace smt {
                 return false;
             }
 
-            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const {
+            bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) {
                 bool inv;
                 return is_var_and_ground(lhs, rhs, v, t, inv);
             }
             
-            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const {
+            bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
                 if (!is_app(n))
                     return false;
                 if (m_manager.is_eq(n))
@@ -1999,7 +1991,7 @@ namespace smt {
                 return false;
             }
 
-            bool is_var_minus_var(expr * n, var * & v1, var * & v2) const {
+            bool is_var_minus_var(expr * n, var * & v1, var * & v2) {
                 if (!is_add(n))
                     return false;
                 expr * arg1 = to_app(n)->get_arg(0);
@@ -2018,7 +2010,7 @@ namespace smt {
                 return true;
             }
 
-            bool is_var_and_var(expr * lhs, expr * rhs, var * & v1, var * & v2) const {
+            bool is_var_and_var(expr * lhs, expr * rhs, var * & v1, var * & v2) {
                 if (is_var(lhs) && is_var(rhs)) {
                     v1 = to_var(lhs);
                     v2 = to_var(rhs);
@@ -2029,11 +2021,11 @@ namespace smt {
                     (is_var_minus_var(rhs, v1, v2) && is_zero(lhs));
             }
 
-            bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) const {
+            bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) {
                 return m_manager.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
             }
 
-            bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) const {
+            bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) {
                 return is_le_ge(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
             }
 
@@ -2379,10 +2371,10 @@ namespace smt {
             
  
         public:
-            quantifier_analyzer(model_finder& mf, ast_manager & m, simplifier & s):
+            quantifier_analyzer(model_finder& mf, ast_manager & m):
                 m_mf(mf),
                 m_manager(m),
-                m_mutil(m, s),
+                m_mutil(m),
                 m_array_util(m), 
                 m_arith_util(m),
                 m_bv_util(m),
@@ -3152,11 +3144,11 @@ namespace smt {
     //
     // -----------------------------------
     
-    model_finder::model_finder(ast_manager & m, simplifier & s):
+    model_finder::model_finder(ast_manager & m):
         m_manager(m),
         m_context(0),
-        m_analyzer(alloc(quantifier_analyzer, *this, m, s)),
-        m_auf_solver(alloc(auf_solver, m, s)),
+        m_analyzer(alloc(quantifier_analyzer, *this, m)),
+        m_auf_solver(alloc(auf_solver, m)),
         m_dependencies(m),
         m_sm_solver(alloc(simple_macro_solver, m, m_q2info)),
         m_hint_solver(alloc(hint_solver, m, m_q2info)),
diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h
index f02640659..2b79ab265 100644
--- a/src/smt/smt_model_finder.h
+++ b/src/smt/smt_model_finder.h
@@ -48,7 +48,6 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/func_decl_dependencies.h"
-#include "ast/simplifier/simplifier.h"
 #include "smt/proto_model/proto_model.h"
 #include "util/cooperate.h"
 #include "tactic/tactic_exception.h"
@@ -107,7 +106,7 @@ namespace smt {
 
 
     public:
-        model_finder(ast_manager & m, simplifier & s);
+        model_finder(ast_manager & m);
         ~model_finder();
         void set_context(context * ctx);
         
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 84ed7c8cd..6a2f848d9 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -434,7 +434,7 @@ namespace smt {
 
             m_mam           = mk_mam(*m_context);
             m_lazy_mam      = mk_mam(*m_context);
-            m_model_finder  = alloc(model_finder, m, m_context->get_simplifier());
+            m_model_finder  = alloc(model_finder, m);
             m_model_checker = alloc(model_checker, m, *m_fparams, *(m_model_finder.get()));
 
             m_model_finder->set_context(m_context);
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index ab68a2b63..f7312fd2e 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -63,7 +63,7 @@ class quasi_macros_tactic : public tactic {
             simp.register_plugin(bvsimp);
                 
             macro_manager mm(m_manager, simp);
-            quasi_macros qm(m_manager, mm, simp);
+            quasi_macros qm(m_manager, mm);
             bool more = true;
         
             expr_ref_vector forms(m_manager), new_forms(m_manager);