diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h
index d209ab6b4..924481dd8 100644
--- a/src/ast/expr_substitution.h
+++ b/src/ast/expr_substitution.h
@@ -52,4 +52,37 @@ public:
     void cleanup();
 };
 
+class scoped_expr_substitution {
+    expr_substitution& m_subst;
+    expr_ref_vector    m_trail;
+    unsigned_vector    m_trail_lim;
+public:
+
+    scoped_expr_substitution(expr_substitution& s): m_subst(s), m_trail(s.m()) {}
+    ~scoped_expr_substitution() {}
+
+    void insert(expr * s, expr * def, proof * def_pr = 0, expr_dependency * def_dep = 0) { 
+        if (!m_subst.contains(s)) {
+            m_subst.insert(s, def, def_pr, def_dep); 
+            m_trail.push_back(s);
+        }
+    }
+    void reset() { m_subst.reset(); m_trail.reset(); m_trail_lim.reset(); }
+    void push() { m_trail_lim.push_back(m_trail.size()); }
+    void pop(unsigned n) { 
+        if (n > 0) {
+            unsigned new_sz = m_trail_lim.size() - n;
+            unsigned old_sz = m_trail_lim[new_sz];
+            for (unsigned i = old_sz; i < m_trail.size(); ++i) m_subst.erase(m_trail[i].get());  
+            m_trail.resize(old_sz); 
+            m_trail_lim.resize(new_sz); 
+        }
+    }
+    bool empty() const { return m_subst.empty(); }
+    bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); }
+    bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
+    bool contains(expr * s) { return m_subst.contains(s); }
+    void cleanup() { m_subst.cleanup(); }
+};
+
 #endif
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index c1b99bcae..804fbcbed 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -3,13 +3,16 @@ z3_add_component(rewriter
     arith_rewriter.cpp
     array_rewriter.cpp
     ast_counter.cpp
+    bit2int.cpp
     bool_rewriter.cpp
     bv_bounds.cpp
+    bv_elim2.cpp
     bv_rewriter.cpp
     datatype_rewriter.cpp
     der.cpp
     distribute_forall.cpp
     dl_rewriter.cpp
+    elim_bounds2.cpp
     enum2bv_rewriter.cpp
     expr_replacer.cpp
     expr_safe_replace.cpp
@@ -17,6 +20,7 @@ z3_add_component(rewriter
     fpa_rewriter.cpp
     inj_axiom.cpp
     label_rewriter.cpp
+    maximize_ac_sharing.cpp
     mk_simplified_app.cpp
     pb_rewriter.cpp
     pb2bv_rewriter.cpp
diff --git a/src/ast/simplifier/bit2int.cpp b/src/ast/rewriter/bit2int.cpp
similarity index 87%
rename from src/ast/simplifier/bit2int.cpp
rename to src/ast/rewriter/bit2int.cpp
index 6f7dd1cbe..257740412 100644
--- a/src/ast/simplifier/bit2int.cpp
+++ b/src/ast/rewriter/bit2int.cpp
@@ -19,15 +19,16 @@ Revision History:
 
 --*/
 
-#include "ast/simplifier/bit2int.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/for_each_ast.h"
+#include "ast/rewriter/bit2int.h"
+
 
 #define CHECK(_x_) if (!(_x_)) { UNREACHABLE(); }
 
 bit2int::bit2int(ast_manager & m) : 
-    m_manager(m), m_bv_util(m), m_arith_util(m), m_cache(m), m_bit0(m) {
+    m_manager(m), m_bv_util(m), m_rewriter(m), m_arith_util(m), m_cache(m), m_bit0(m) {
     m_bit0     = m_bv_util.mk_numeral(0,1);
 }
 
@@ -67,7 +68,7 @@ unsigned bit2int::get_numeral_bits(numeral const& k) {
 void bit2int::align_size(expr* e, unsigned sz, expr_ref& result) {
     unsigned sz1 = m_bv_util.get_bv_size(e);
     SASSERT(sz1 <= sz);
-    m_bv_simplifier->mk_zeroext(sz-sz1, e, result);    
+    result = m_rewriter.mk_zero_extend(sz-sz1, e);
 }
 
 void bit2int::align_sizes(expr_ref& a, expr_ref& b) {
@@ -75,11 +76,11 @@ void bit2int::align_sizes(expr_ref& a, expr_ref& b) {
     unsigned sz2 = m_bv_util.get_bv_size(b);
     expr_ref tmp(m_manager);
     if (sz1 > sz2) {
-        m_bv_simplifier->mk_zeroext(sz1-sz2, b, tmp);    
+        tmp = m_rewriter.mk_zero_extend(sz1-sz2, b);    
         b = tmp;
     }
     else if (sz2 > sz1) {
-        m_bv_simplifier->mk_zeroext(sz2-sz1, a, tmp);    
+        tmp = m_rewriter.mk_zero_extend(sz2-sz1, a);    
         a = tmp;
     }
 }
@@ -123,11 +124,11 @@ bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) {
             return true;
         }
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_zeroext(1, tmp1, tmp1);
-        m_bv_simplifier->mk_zeroext(1, tmp2, tmp2);
+        tmp1 = m_rewriter.mk_zero_extend(1, tmp1);
+        tmp2 = m_rewriter.mk_zero_extend(1, tmp2);
         SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
-        m_bv_simplifier->mk_add(tmp1, tmp2, tmp3);
-        m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
+        tmp3 = m_rewriter.mk_bv_add(tmp1, tmp2);
+        result = m_rewriter.mk_bv2int(tmp3);
         return true;
     }
     return false;
@@ -143,14 +144,14 @@ bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) {
         SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
         switch(ty) {
         case lt:
-            m_bv_simplifier->mk_leq_core(false, tmp2, tmp1, tmp3);
+            tmp3 = m_rewriter.mk_ule(tmp2, tmp1);
             result = m_manager.mk_not(tmp3);
             break;
         case le:
-            m_bv_simplifier->mk_leq_core(false,tmp1, tmp2, result);
+            result = m_rewriter.mk_ule(tmp1, tmp2);
             break;
         case eq:
-            result = m_manager.mk_eq(tmp1,tmp2);
+            result = m_manager.mk_eq(tmp1, tmp2);
             break;
         }
         return true;
@@ -167,12 +168,12 @@ bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) {
     if (extract_bv(e1, sz1, sign1, tmp1) &&
         extract_bv(e2, sz2, sign2, tmp2)) {
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_zeroext(m_bv_util.get_bv_size(tmp1), tmp1, tmp1);
-        m_bv_simplifier->mk_zeroext(m_bv_util.get_bv_size(tmp2), tmp2, tmp2);
+        tmp1 = m_rewriter.mk_zero_extend(m_bv_util.get_bv_size(tmp1), tmp1);
+        tmp2 = m_rewriter.mk_zero_extend(m_bv_util.get_bv_size(tmp2), tmp2);
 
         SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
-        m_bv_simplifier->mk_mul(tmp1, tmp2, tmp3);
-        m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
+        tmp3 = m_rewriter.mk_bv_mul(tmp1, tmp2);
+        result = m_rewriter.mk_bv2int(tmp3);
         if (sign1 != sign2) {
             result = m_arith_util.mk_uminus(result);
         }
@@ -187,8 +188,7 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
     numeral k;
     bool is_int;
     todo.push_back(n);
-    m_bv_simplifier->mk_bv2int(m_bit0, m_arith_util.mk_int(), pos);
-    m_bv_simplifier->mk_bv2int(m_bit0, m_arith_util.mk_int(), neg);
+    neg = pos = m_rewriter.mk_bv2int(m_bit0);
         
     while (!todo.empty()) {
         n = todo.back();
@@ -372,8 +372,8 @@ void bit2int::visit(app* n) {
             tmp1 = tmp_p;
             tmp2 = e2bv;
             align_sizes(tmp1, tmp2);
-            m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
-            m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
+            tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
+            result = m_rewriter.mk_bv2int(tmp3);
             cache_result(n, result);
             return;
         }
@@ -382,25 +382,24 @@ void bit2int::visit(app* n) {
         tmp1 = tmp_n;
         tmp2 = e2bv;
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
+        tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
         // e2 - (neg1 mod e2)
         tmp1 = e2bv;
         tmp2 = tmp3;
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_sub(tmp1, tmp2, tmp3);
+        tmp3 = m_rewriter.mk_bv_sub(tmp1, tmp2);
         // pos1 + (e2 - (neg1 mod e2))
         tmp1 = tmp_p;
         tmp2 = tmp3;
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_zeroext(1, tmp1, tmp_p);
-        m_bv_simplifier->mk_zeroext(1, tmp2, tmp_n);
-        m_bv_simplifier->mk_add(tmp_p, tmp_n, tmp1);
+        tmp_p = m_rewriter.mk_zero_extend(1, tmp1);
+        tmp_n = m_rewriter.mk_zero_extend(1, tmp2);
+        tmp1 = m_rewriter.mk_bv_add(tmp_p, tmp_n);
         // (pos1 + (e2 - (neg1 mod e2))) mod e2
         tmp2 = e2bv;
         align_sizes(tmp1, tmp2);
-        m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
-
-        m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
+        tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
+        result = m_rewriter.mk_bv2int(tmp3);
 
         cache_result(n, result);
     }
diff --git a/src/ast/simplifier/bit2int.h b/src/ast/rewriter/bit2int.h
similarity index 90%
rename from src/ast/simplifier/bit2int.h
rename to src/ast/rewriter/bit2int.h
index 84ae1f4a4..fe15d1ec5 100644
--- a/src/ast/simplifier/bit2int.h
+++ b/src/ast/rewriter/bit2int.h
@@ -22,9 +22,7 @@ Revision History:
 #include "ast/bv_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/act_cache.h"
-#include "ast/simplifier/basic_simplifier_plugin.h"
-#include "ast/simplifier/bv_simplifier_plugin.h"
-
+#include "ast/rewriter/bv_rewriter.h"
 
 class bit2int {
 protected:
@@ -60,8 +58,8 @@ protected:
     typedef act_cache expr_map;
     ast_manager &             m_manager;
     bv_util                   m_bv_util;
+    bv_rewriter               m_rewriter;
     arith_util                m_arith_util;
-    bv_simplifier_plugin    * m_bv_simplifier;
 
     expr_map                  m_cache;      // map: ast  -> ast    ref. counters are incremented when inserted here.
     expr_ref                  m_bit0;
@@ -88,7 +86,6 @@ protected:
 
 public:
     bit2int(ast_manager & m);
-    void set_bv_simplifier(bv_simplifier_plugin * p) { m_bv_simplifier = p; }
     void operator()(expr * m, expr_ref & result, proof_ref& p);
 };
 
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 1109251e0..45bd6c264 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -98,11 +98,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_rotate_right(unsigned n, expr * arg, expr_ref & result);
     br_status mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bv_add(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_add(2, args, result); }
+    br_status mk_bv_sub(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_sub(2, args, result); }
+    br_status mk_bv_mul(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_mul(2, args, result); }
     br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result);
-    br_status mk_bv_add(expr * arg1, expr * arg2, expr_ref & result) {
-        expr * args[2] = { arg1, arg2 };
-        return mk_bv_add(2, args, result);
-    }
     br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
@@ -185,6 +184,38 @@ public:
     bool hi_div0() const { return m_hi_div0; }
 
     bv_util & get_util() { return m_util; }
+
+#define MK_BV_BINARY(OP)                         \
+    expr_ref OP(expr* a, expr* b) {              \
+        expr_ref result(m());                    \
+        if (BR_FAILED == OP(a, b, result))       \
+            result = m_util.OP(a, b);            \
+        return result;                           \
+    }                                            \
+    
+    expr_ref mk_zero_extend(unsigned n, expr * arg) {       
+        expr_ref result(m());                   
+        if (BR_FAILED == mk_zero_extend(n, arg, result))    
+            result = m_util.mk_zero_extend(n, arg);         
+        return result;                          
+    }                                           
+
+    MK_BV_BINARY(mk_bv_urem);
+    MK_BV_BINARY(mk_ule);
+    MK_BV_BINARY(mk_bv_add);
+    MK_BV_BINARY(mk_bv_mul);
+    MK_BV_BINARY(mk_bv_sub);
+
+
+    expr_ref mk_bv2int(expr* a) {
+        expr_ref result(m());
+        if (BR_FAILED == mk_bv2int(a, result)) 
+            result = m_util.mk_bv2int(a);
+        return result;        
+    }
+
+
+
 };
 
 #endif
diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt
index b6fe9b1cd..52a44595e 100644
--- a/src/ast/simplifier/CMakeLists.txt
+++ b/src/ast/simplifier/CMakeLists.txt
@@ -5,7 +5,6 @@ z3_add_component(simplifier
     array_simplifier_params.cpp
     array_simplifier_plugin.cpp
     basic_simplifier_plugin.cpp
-    bit2int.cpp
     bv_elim.cpp
     bv_simplifier_params.cpp
     bv_simplifier_plugin.cpp
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 8b25e9263..f8efcbf4b 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -33,7 +33,6 @@ Revision History:
 #include "ast/simplifier/bv_simplifier_plugin.h"
 #include "ast/simplifier/bv_elim.h"
 #include "ast/simplifier/elim_bounds.h"
-#include "ast/simplifier/bit2int.h"
 #include "ast/normal_forms/pull_quant.h"
 #include "ast/normal_forms/nnf.h"
 #include "ast/pattern/pattern_inference.h"
@@ -70,7 +69,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     basic_simplifier_plugin * basic_simp = 0;
     bv_simplifier_plugin * bv_simp = 0;
     setup_simplifier_plugins(m_pre_simplifier, basic_simp, arith_simp, bv_simp);
-    m_bit2int.set_bv_simplifier(bv_simp);
     m_pre_simplifier.enable_presimp();
 }
 
@@ -262,7 +260,7 @@ void asserted_formulas::reduce() {
     INVOKE(m_params.m_propagate_values, propagate_values());
     INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
     INVOKE(m_params.m_nnf_cnf || (m_params.m_mbqi && has_quantifiers()), nnf_cnf());
-    INVOKE(m_params.m_eliminate_and, eliminate_and());
+    INVOKE(/*m_params.m_eliminate_and*/ true, eliminate_and());
     INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees());
     INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers());
     INVOKE(m_params.m_ng_lift_ite != LI_NONE, ng_lift_ite());
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index eaed4e405..fb621000c 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -24,7 +24,7 @@ Revision History:
 #include "ast/simplifier/simplifier.h"
 #include "ast/simplifier/basic_simplifier_plugin.h"
 #include "ast/simplifier/maximise_ac_sharing.h"
-#include "ast/simplifier/bit2int.h"
+#include "ast/rewriter/bit2int.h"
 #include "ast/macros/macro_manager.h"
 #include "ast/macros/macro_finder.h"
 #include "ast/normal_forms/defined_names.h"
diff --git a/src/smt/elim_term_ite.h b/src/smt/elim_term_ite.h
index 94e5e0346..106a9f511 100644
--- a/src/smt/elim_term_ite.h
+++ b/src/smt/elim_term_ite.h
@@ -59,6 +59,7 @@ public:
     }
     virtual ~elim_term_ite_cfg() {}
     vector<justified_expr> const& new_defs() const { return m_new_defs; }
+    void reset() { m_new_defs.reset(); }
     br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
 };
 
@@ -70,6 +71,7 @@ public:
         m_cfg(m, dn) 
     {}
     vector<justified_expr> const& new_defs() const { return m_cfg.new_defs(); }
+    void reset() { m_cfg.reset(); }
 };
 
 
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 9267dbeba..fcdea850f 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -46,7 +46,7 @@ void preprocessor_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pull_cheap_ite_trees);
     DISPLAY_PARAM(m_pull_nested_quantifiers);
     DISPLAY_PARAM(m_eliminate_term_ite);
-    DISPLAY_PARAM(m_eliminate_and);
+    //DISPLAY_PARAM(m_eliminate_and);
     DISPLAY_PARAM(m_macro_finder);
     DISPLAY_PARAM(m_propagate_values);
     DISPLAY_PARAM(m_propagate_booleans);
diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h
index c343c55fa..fe759417d 100644
--- a/src/smt/params/preprocessor_params.h
+++ b/src/smt/params/preprocessor_params.h
@@ -39,7 +39,7 @@ struct preprocessor_params : public pattern_inference_params,
     bool            m_pull_cheap_ite_trees;
     bool            m_pull_nested_quantifiers;
     bool            m_eliminate_term_ite;
-    bool            m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
+//    bool            m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
     bool            m_macro_finder;
     bool            m_propagate_values;
     bool            m_propagate_booleans;
@@ -62,7 +62,7 @@ public:
         m_pull_cheap_ite_trees(false),
         m_pull_nested_quantifiers(false),
         m_eliminate_term_ite(false),
-        m_eliminate_and(true),
+       // m_eliminate_and(true),
         m_macro_finder(false),
         m_propagate_values(true),
         m_propagate_booleans(false), // TODO << check peformance