diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 01b671c99..0719ebdfa 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -178,7 +178,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     MK_AC_OP(m_i_mul_decl, "*", OP_MUL, i);
     MK_LEFT_ASSOC_OP(m_i_div_decl, "div", OP_IDIV, i);
     MK_OP(m_i_rem_decl, "rem", OP_REM, i);
-    MK_OP(m_i_mod_decl, "mod", OP_MOD, i);
+    //MK_OP(m_i_mod_decl, "mod", OP_MOD, i);
     MK_UNARY(m_i_uminus_decl, "-", OP_UMINUS, i);
 
     m_to_real_decl = m->mk_func_decl(symbol("to_real"), i, r, func_decl_info(id, OP_TO_REAL));
@@ -215,18 +215,18 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_e = m->mk_const(e_decl);
     m->inc_ref(m_e);
 
-    func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
-    m_0_pw_0_int = m->mk_const(z_pw_z_int);
-    m->inc_ref(m_0_pw_0_int);
+    //func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
+    //m_0_pw_0_int = m->mk_const(z_pw_z_int);
+    //m->inc_ref(m_0_pw_0_int);
 
-    func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
-    m_0_pw_0_real = m->mk_const(z_pw_z_real);
-    m->inc_ref(m_0_pw_0_real);
+    //func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
+    //m_0_pw_0_real = m->mk_const(z_pw_z_real);
+    //m->inc_ref(m_0_pw_0_real);
 
     MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
-    MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
-    MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
-    MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
+    //MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
+    //MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
+    //MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i);
     MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r);
     MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r);
 }
@@ -392,12 +392,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_ATANH:     return m_atanh_decl;
     case OP_PI:        return m_pi->get_decl();
     case OP_E:         return m_e->get_decl();
-    case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
-    case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
+    //case OP_0_PW_0_INT:  return m_0_pw_0_int->get_decl();
+    //case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl();
     case OP_NEG_ROOT:    return m_neg_root_decl;
-    case OP_DIV_0:       return m_div_0_decl;
-    case OP_IDIV_0:      return m_idiv_0_decl;
-    case OP_MOD_0:       return m_mod_0_decl;
+    //case OP_DIV_0:       return m_div_0_decl;
+    //case OP_IDIV_0:      return m_idiv_0_decl;
+    //case OP_MOD_0:       return m_mod_0_decl;
     case OP_U_ASIN:      return m_u_asin_decl;
     case OP_U_ACOS:      return m_u_acos_decl;
     default: return 0;
@@ -489,9 +489,9 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
 static bool is_const_op(decl_kind k) {
     return
         k == OP_PI ||
-        k == OP_E  ||
-        k == OP_0_PW_0_INT ||
-        k == OP_0_PW_0_REAL;
+        k == OP_E;
+        //k == OP_0_PW_0_INT ||
+        //k == OP_0_PW_0_REAL;
 }
 
 func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 6c2b1c77a..0238df3ae 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -70,12 +70,12 @@ enum arith_op_kind {
     OP_PI,
     OP_E,
     // under-specified symbols
-    OP_0_PW_0_INT,    // 0^0 for integers
-    OP_0_PW_0_REAL,   // 0^0 for reals
+    //OP_0_PW_0_INT,    // 0^0 for integers
+    //OP_0_PW_0_REAL,   // 0^0 for reals
     OP_NEG_ROOT,      // x^n when n is even and x is negative
-    OP_DIV_0,         // x/0
-    OP_IDIV_0,        // x div 0
-    OP_MOD_0,         // x mod 0
+    // OP_DIV_0,         // x/0
+    // OP_IDIV_0,        // x div 0
+    // OP_MOD_0,         // x mod 0
     OP_U_ASIN,        // asin(x) for x < -1 or x > 1
     OP_U_ACOS,        // acos(x) for x < -1 or x > 1
     LAST_ARITH_OP
@@ -218,12 +218,12 @@ public:
             return false;
         switch (f->get_decl_kind())
         {
-        case OP_0_PW_0_INT:
-        case OP_0_PW_0_REAL:
+        //case OP_0_PW_0_INT:
+        //case OP_0_PW_0_REAL:
         case OP_NEG_ROOT:
-        case OP_DIV_0:
-        case OP_IDIV_0:
-        case OP_MOD_0:
+        //case OP_DIV_0:
+        //case OP_IDIV_0:
+        //case OP_MOD_0:
         case OP_U_ASIN:
         case OP_U_ACOS:
             return true;
@@ -276,9 +276,9 @@ public:
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }
     bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); }
     bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); }
-    bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
+    //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); }
     bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); }
-    bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
+    //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); }
     bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); }
     bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); }
     bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); }
@@ -425,11 +425,11 @@ public:
     app * mk_pi() { return plugin().mk_pi(); }
     app * mk_e()  { return plugin().mk_e(); }
 
-    app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
-    app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
-    app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
-    app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
-    app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
+ //   app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); }
+ //   app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); }
+ //   app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); }
+ //   app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); }
+ //   app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); }
     app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
     app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
     app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f347a8e49..029e2d90c 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2355,6 +2355,7 @@ quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort *
     SASSERT(num_decls > 0);
     DEBUG_CODE({
             for (unsigned i = 0; i < num_patterns; ++i) {
+                TRACE("ast", tout << i << " " << mk_pp(patterns[i], *this) << "\n";);
                 SASSERT(is_pattern(patterns[i]));
             }});
     unsigned sz               = quantifier::get_obj_size(num_decls, num_patterns, num_no_patterns);
diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index b6ee62322..855cae107 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -213,11 +213,13 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
 struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
     ast_manager& m; 
     macro_manager& mm;
+    expr_dependency_ref m_used_macro_dependencies; 
     expr_ref_vector m_trail;
 
     macro_expander_cfg(ast_manager& m, macro_manager& mm):
         m(m),
         mm(mm),
+        m_used_macro_dependencies(m),
         m_trail(m)
     {}
 
@@ -297,8 +299,10 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
                 p = m.mk_unit_resolution(2, prs);
             }
             else {
-                p = 0;
+                p = 0; 
             }
+            expr_dependency * ed = mm.m_decl2macro_dep.find(d); 
+            m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed); 
             return true;
         }
         return false;
@@ -307,6 +311,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
 
 struct macro_manager::macro_expander_rw : public rewriter_tpl<macro_manager::macro_expander_cfg> {
     macro_expander_cfg m_cfg;
+
     macro_expander_rw(ast_manager& m, macro_manager& mm):
         rewriter_tpl<macro_manager::macro_expander_cfg>(m, m.proofs_enabled(), m_cfg),
         m_cfg(m, mm) 
@@ -319,8 +324,10 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
         // Expand macros with "real" proof production support (NO rewrite*)
         expr_ref old_n(m);
         proof_ref old_pr(m);
+        expr_dependency_ref old_dep(m);
         old_n  = n;
         old_pr = pr;
+        old_dep = dep;
         bool change = false;
         for (;;) {
             macro_expander_rw proc(m, *this);
@@ -328,10 +335,12 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
             TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";);
             proc(old_n, r, n_eq_r_pr);
             new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr);
+            new_dep = m.mk_join(old_dep, proc.m_cfg.m_used_macro_dependencies); 
             if (r.get() == old_n.get())
                 break;
             old_n  = r;
             old_pr = new_pr;
+            old_dep = new_dep;
             change = true;
         }
         // apply th_rewrite to the result.
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 4b00cde45..1f2e9e2e9 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -680,8 +680,9 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     if (m_util.is_numeral(arg2, v2, is_int)) {
         SASSERT(!is_int);
         if (v2.is_zero()) {
-            result = m_util.mk_div0(arg1);
-            return BR_REWRITE1;
+            return BR_FAILED;
+            //result = m_util.mk_div0(arg1);
+            //return BR_REWRITE1;
         }
         else if (m_util.is_numeral(arg1, v1, is_int)) {
             result = m_util.mk_numeral(v1/v2, false);
@@ -735,8 +736,8 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         return BR_DONE;
     }
     if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
-        result = m_util.mk_idiv0(arg1);
-        return BR_REWRITE1;
+        //result = m_util.mk_idiv0(arg1);
+        //return BR_REWRITE1;
     }
     return BR_FAILED;
 }
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 2a6bd2c50..85044af08 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -508,22 +508,22 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
     expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once
     bool     has_multiple = false;
     expr *   prev = 0;
-    bool     ordered      = true;
+    bool     ordered  = true;
     for (unsigned i = 0; i < num_args; i++) {
         expr * arg = args[i];
+
         if (is_numeral(arg, a)) {
             num_coeffs++;
             c += a;
+            ordered = !m_sort_sums || i == 0;
         }
-        else {
-            // arg is not a numeral
-            if (m_sort_sums && ordered) {
-                if (prev != 0 && lt(arg, prev))
-                    ordered = false;
-                prev = arg;
-            }
+        else if (m_sort_sums && ordered) {
+            if (prev != 0 && lt(arg, prev)) 
+                ordered = false;
+            prev = arg;        
         }
 
+
         arg = get_power_product(arg);
         if (visited.is_marked(arg)) {
             multiple.mark(arg);
@@ -535,8 +535,8 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
     }
     normalize(c);
     SASSERT(m_sort_sums || ordered);
-    TRACE("sort_sums", 
-          tout << "ordered: " << ordered << "\n";
+    TRACE("rewriter", 
+          tout << "ordered: " << ordered << " sort sums: " << m_sort_sums << "\n";
           for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";);
 
     if (has_multiple) {
@@ -589,13 +589,14 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
             hoist_cmul(new_args);
         }
         else if (m_sort_sums) {
-            TRACE("sort_sums_bug", tout << "new_args.size(): " << new_args.size() << "\n";);
+            TRACE("rewriter_bug", tout << "new_args.size(): " << new_args.size() << "\n";);
             if (c.is_zero())
                 std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
             else
                 std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
         }
         result = mk_add_app(new_args.size(), new_args.c_ptr());
+        TRACE("rewriter", tout << result << "\n";);
         if (hoist_multiplication(result)) {
             return BR_REWRITE_FULL;
         }
diff --git a/src/ast/rewriter/push_app_ite.cpp b/src/ast/rewriter/push_app_ite.cpp
index 386a4fb27..f3df4d711 100644
--- a/src/ast/rewriter/push_app_ite.cpp
+++ b/src/ast/rewriter/push_app_ite.cpp
@@ -73,6 +73,7 @@ br_status push_app_ite_cfg::reduce_app(func_decl * f, unsigned num, expr * const
     expr_ref e_new(m.mk_app(f, num, args_prime), m);
     args_prime[ite_arg_idx] = old;
     result = m.mk_ite(c, t_new, e_new);
+    TRACE("push_app_ite", tout << result << "\n";);
     if (m.proofs_enabled()) {
         result_pr = m.mk_rewrite(m.mk_app(f, num, args), result);
     }
diff --git a/src/ast/rewriter/push_app_ite.h b/src/ast/rewriter/push_app_ite.h
index e6c6b6fb2..ae06aad30 100644
--- a/src/ast/rewriter/push_app_ite.h
+++ b/src/ast/rewriter/push_app_ite.h
@@ -34,6 +34,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
     virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
     push_app_ite_cfg(ast_manager& m, bool conservative = true): m(m), m_conservative(conservative) {}
+    bool rewrite_patterns() const { return false; }
 };
 
 /**
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 163118d17..c511f00d0 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -496,6 +496,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     expr * const * new_pats;
     expr * const * new_no_pats;
     if (rewrite_patterns()) {
+        TRACE("reduce_quantifier_bug", tout << "rewrite patterns\n";);
         new_pats    = it + 1;
         new_no_pats = new_pats + q->get_num_patterns();
     }
@@ -518,7 +519,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     }
     else {
         expr_ref tmp(m());
-
+        TRACE("reduce_quantifier_bug", tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";);
         if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, m_r, m_pr)) {
             if (fr.m_new_child) {
                 m_r = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/ast/rewriter/rewriter_params.pyg
index 06500086a..18bb29e56 100644
--- a/src/ast/rewriter/rewriter_params.pyg
+++ b/src/ast/rewriter/rewriter_params.pyg
@@ -9,5 +9,6 @@ def_module_params('rewriter',
                           ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
                           ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
                           ("cache_all", BOOL, False, "cache all intermediate results."),
+                          ("rewrite_patterns", BOOL, False, "rewrite patterns."),
                           ("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))
 
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 764fa8eef..a2ca12b24 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -55,6 +55,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     bool                m_push_ite_arith;
     bool                m_push_ite_bv;
     bool                m_ignore_patterns_on_ground_qbody;
+    bool                m_rewrite_patterns;
 
     // substitution support
     expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
@@ -72,6 +73,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_push_ite_arith = p.push_ite_arith();
         m_push_ite_bv    = p.push_ite_bv();
         m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
+        m_rewrite_patterns = p.rewrite_patterns();
     }
 
     void updt_params(params_ref const & p) {
@@ -99,7 +101,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         return false;
     }
 
-    bool rewrite_patterns() const { return false; }
+    bool rewrite_patterns() const { return m_rewrite_patterns; }
 
     bool cache_all_results() const { return m_cache_all; }
 
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 0f2437982..1f9c89f89 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -444,16 +444,12 @@ namespace qe {
             div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {}
             ~div_rewriter_cfg() {}
             br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
-                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) {                    
+                rational r(1);
+                if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && (!a.is_numeral(args[1], r) || r.is_zero())) {                    
                     result = m.mk_fresh_const("div", a.mk_real());
                     m_divs.push_back(div(m, args[0], args[1], to_app(result)));
                     return BR_DONE;
                 }
-                if (is_decl_of(f, a.get_family_id(), OP_DIV_0) && sz == 1 && !a.is_numeral(args[0])) {                    
-                    result = m.mk_fresh_const("div", a.mk_real());
-                    m_divs.push_back(div(m, args[0], m_zero, to_app(result)));
-                    return BR_DONE;
-                }
                 return BR_FAILED;
             }
             vector<div> const& divs() const { return m_divs; }
@@ -507,10 +503,6 @@ namespace qe {
                     m_has_divs = true;
                     return;
                 }
-                if (a.is_div0(n) && s.m_mode == qsat_t) {
-                    m_has_divs = true;
-                    return;
-                }
                 TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";);
                 throw tactic_exception("not NRA");
             }
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 385d1aaa0..41890dd05 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -2,7 +2,7 @@ z3_add_component(smt
   SOURCES
     arith_eq_adapter.cpp
     arith_eq_solver.cpp
-    asserted_formulas_new.cpp
+    asserted_formulas.cpp
     cached_var_subst.cpp
     cost_evaluator.cpp
     dyn_ack.cpp
diff --git a/src/smt/asserted_formulas_new.cpp b/src/smt/asserted_formulas.cpp
similarity index 86%
rename from src/smt/asserted_formulas_new.cpp
rename to src/smt/asserted_formulas.cpp
index 8d16ef2cd..626588ab3 100644
--- a/src/smt/asserted_formulas_new.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation
 
 Module Name:
 
-    asserted_formulas_new.cpp
+    asserted_formulas.cpp
 
 Abstract:
 
@@ -25,9 +25,9 @@ Revision History:
 #include "ast/normal_forms/nnf.h"
 #include "ast/pattern/pattern_inference.h"
 #include "ast/macros/quasi_macros.h"
-#include "smt/asserted_formulas_new.h"
+#include "smt/asserted_formulas.h"
 
-asserted_formulas_new::asserted_formulas_new(ast_manager & m, smt_params & p):
+asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     m(m),
     m_params(p),
     m_rewriter(m),
@@ -60,13 +60,11 @@ asserted_formulas_new::asserted_formulas_new(ast_manager & m, smt_params & p):
 
     m_macro_finder = alloc(macro_finder, m, m_macro_manager);
 
-    params_ref pa;
-    pa.set_bool("arith_lhs", true);
-    m_rewriter.updt_params(pa);
+    set_eliminate_and(false);
 
 }
 
-void asserted_formulas_new::setup() {
+void asserted_formulas::setup() {
     switch (m_params.m_lift_ite) {
     case LI_FULL:
         m_params.m_ng_lift_ite = LI_NONE; 
@@ -84,10 +82,10 @@ void asserted_formulas_new::setup() {
 }
 
 
-asserted_formulas_new::~asserted_formulas_new() {
+asserted_formulas::~asserted_formulas() {
 }
 
-void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
+void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
     if (inconsistent()) {
         return;
     }
@@ -119,16 +117,18 @@ void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector<justifie
     }
 }
 
-void asserted_formulas_new::set_eliminate_and(bool flag) {
+void asserted_formulas::set_eliminate_and(bool flag) {
     params_ref p;
-    p.set_bool("elim_and", true);
+    p.set_bool("elim_and", flag);
     p.set_bool("arith_lhs", true);
+    p.set_bool("sort_sums", true);
+    p.set_bool("rewrite_patterns", true);
     m_rewriter.updt_params(p);
     flush_cache();
 }
 
 
-void asserted_formulas_new::assert_expr(expr * e, proof * _in_pr) {
+void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
     proof_ref  in_pr(_in_pr, m), pr(_in_pr, m);
     expr_ref   r(e, m);
 
@@ -153,17 +153,17 @@ void asserted_formulas_new::assert_expr(expr * e, proof * _in_pr) {
     TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
 }
 
-void asserted_formulas_new::assert_expr(expr * e) {
+void asserted_formulas::assert_expr(expr * e) {
     assert_expr(e, m.mk_asserted(e));
 }
 
-void asserted_formulas_new::get_assertions(ptr_vector<expr> & result) const {
+void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
     for (justified_expr const& je : m_formulas) result.push_back(je.get_fml());
 }
 
-void asserted_formulas_new::push_scope() {
+void asserted_formulas::push_scope() {
     SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
-    TRACE("asserted_formulas_new_scopes", tout << "push:\n"; display(tout););    
+    TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););    
     m_scoped_substitution.push();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
@@ -176,8 +176,8 @@ void asserted_formulas_new::push_scope() {
     commit();
 }
  
-void asserted_formulas_new::pop_scope(unsigned num_scopes) {
-    TRACE("asserted_formulas_new_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
+void asserted_formulas::pop_scope(unsigned num_scopes) {
+    TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
     m_bv_sharing.pop_scope(num_scopes);
     m_macro_manager.pop_scope(num_scopes);
     unsigned new_lvl    = m_scopes.size() - num_scopes;
@@ -189,10 +189,10 @@ void asserted_formulas_new::pop_scope(unsigned num_scopes) {
     m_qhead    = s.m_formulas_lim;
     m_scopes.shrink(new_lvl);
     flush_cache();
-    TRACE("asserted_formulas_new_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
+    TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
 }
 
-void asserted_formulas_new::reset() {
+void asserted_formulas::reset() {
     m_defined_names.reset();
     m_qhead = 0;
     m_formulas.reset();
@@ -202,14 +202,14 @@ void asserted_formulas_new::reset() {
     m_inconsistent = false;
 }
 
-bool asserted_formulas_new::check_well_sorted() const {
+bool asserted_formulas::check_well_sorted() const {
     for (justified_expr const& je : m_formulas) {
         if (!is_well_sorted(m, je.get_fml())) return false; 
     }
     return true;
 }
 
-void asserted_formulas_new::reduce() {
+void asserted_formulas::reduce() {
     if (inconsistent())
         return;
     if (canceled())
@@ -255,7 +255,7 @@ void asserted_formulas_new::reduce() {
 }
 
 
-unsigned asserted_formulas_new::get_formulas_last_level() const {
+unsigned asserted_formulas::get_formulas_last_level() const {
     if (m_scopes.empty()) {
         return 0;
     }
@@ -264,7 +264,7 @@ unsigned asserted_formulas_new::get_formulas_last_level() const {
     }
 }
 
-bool asserted_formulas_new::invoke(simplify_fmls& s) {
+bool asserted_formulas::invoke(simplify_fmls& s) {
     if (!s.should_apply()) return true;
     IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
     s();
@@ -281,7 +281,7 @@ bool asserted_formulas_new::invoke(simplify_fmls& s) {
     }
 }
 
-void asserted_formulas_new::display(std::ostream & out) const {
+void asserted_formulas::display(std::ostream & out) const {
     out << "asserted formulas:\n";
     for (unsigned i = 0; i < m_formulas.size(); i++) {
         if (i == m_qhead)
@@ -291,7 +291,7 @@ void asserted_formulas_new::display(std::ostream & out) const {
     out << "inconsistent: " << inconsistent() << "\n";
 }
 
-void asserted_formulas_new::display_ll(std::ostream & out, ast_mark & pp_visited) const {
+void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
     if (!m_formulas.empty()) {
         for (justified_expr const& f : m_formulas) 
             ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
@@ -302,18 +302,18 @@ void asserted_formulas_new::display_ll(std::ostream & out, ast_mark & pp_visited
     }
 }
 
-void asserted_formulas_new::collect_statistics(statistics & st) const {
+void asserted_formulas::collect_statistics(statistics & st) const {
 }
 
 
-void asserted_formulas_new::swap_asserted_formulas(vector<justified_expr>& formulas) {
+void asserted_formulas::swap_asserted_formulas(vector<justified_expr>& formulas) {
     SASSERT(!inconsistent() || !formulas.empty());
     m_formulas.shrink(m_qhead);
     m_formulas.append(formulas);
 }
 
 
-void asserted_formulas_new::find_macros_core() {
+void asserted_formulas::find_macros_core() {
     vector<justified_expr> new_fmls;
     unsigned sz = m_formulas.size();
     (*m_macro_finder)(sz - m_qhead, m_formulas.c_ptr() + m_qhead, new_fmls);
@@ -321,7 +321,7 @@ void asserted_formulas_new::find_macros_core() {
     reduce_and_solve();
 }
 
-void asserted_formulas_new::apply_quasi_macros() {
+void asserted_formulas::apply_quasi_macros() {
     TRACE("before_quasi_macros", display(tout););
     vector<justified_expr> new_fmls;
     quasi_macros proc(m, m_macro_manager);    
@@ -335,7 +335,7 @@ void asserted_formulas_new::apply_quasi_macros() {
     reduce_and_solve();
 }
 
-void asserted_formulas_new::nnf_cnf() {
+void asserted_formulas::nnf_cnf() {
     nnf              apply_nnf(m, m_defined_names);
     vector<justified_expr> new_fmls;
     expr_ref_vector  push_todo(m);
@@ -379,7 +379,7 @@ void asserted_formulas_new::nnf_cnf() {
     swap_asserted_formulas(new_fmls);
 }
 
-void asserted_formulas_new::simplify_fmls::operator()() {
+void asserted_formulas::simplify_fmls::operator()() {
     vector<justified_expr> new_fmls;
     unsigned sz = af.m_formulas.size();                                
     for (unsigned i = af.m_qhead; i < sz; i++) {                                           
@@ -405,18 +405,18 @@ void asserted_formulas_new::simplify_fmls::operator()() {
 }
 
 
-void asserted_formulas_new::reduce_and_solve() {
+void asserted_formulas::reduce_and_solve() {
     IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
     flush_cache(); // collect garbage
     m_reduce_asserted_formulas();
 }
 
 
-void asserted_formulas_new::commit() {
+void asserted_formulas::commit() {
     commit(m_formulas.size());
 }
 
-void asserted_formulas_new::commit(unsigned new_qhead) {
+void asserted_formulas::commit(unsigned new_qhead) {
     m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead);
     m_expr2depth.reset();
     for (unsigned i = m_qhead; i < new_qhead; ++i) {
@@ -426,7 +426,7 @@ void asserted_formulas_new::commit(unsigned new_qhead) {
     m_qhead = new_qhead;
 }
 
-void asserted_formulas_new::propagate_values() {
+void asserted_formulas::propagate_values() {
     TRACE("propagate_values", tout << "before:\n"; display(tout););
     flush_cache();
 
@@ -463,7 +463,7 @@ void asserted_formulas_new::propagate_values() {
         m_reduce_asserted_formulas();
 }
 
-unsigned asserted_formulas_new::propagate_values(unsigned i) {
+unsigned asserted_formulas::propagate_values(unsigned i) {
     expr * n = m_formulas[i].get_fml();
     expr_ref new_n(m);                                                  
     proof_ref new_pr(m);                                                
@@ -481,7 +481,7 @@ unsigned asserted_formulas_new::propagate_values(unsigned i) {
     return n != new_n ? 1 : 0;
 }
 
-void asserted_formulas_new::update_substitution(expr* n, proof* pr) {
+void asserted_formulas::update_substitution(expr* n, proof* pr) {
     expr* lhs, *rhs, *n1;
     if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
         compute_depth(lhs);
@@ -510,7 +510,7 @@ void asserted_formulas_new::update_substitution(expr* n, proof* pr) {
    \brief implement a Knuth-Bendix ordering on expressions.
 */
 
-bool asserted_formulas_new::is_gt(expr* lhs, expr* rhs) {
+bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
     if (lhs == rhs) {
         return false;
     }
@@ -541,7 +541,7 @@ bool asserted_formulas_new::is_gt(expr* lhs, expr* rhs) {
     return false;
 }
 
-void asserted_formulas_new::compute_depth(expr* e) {
+void asserted_formulas::compute_depth(expr* e) {
     ptr_vector<expr> todo;
     todo.push_back(e);    
     while (!todo.empty()) {
@@ -573,7 +573,7 @@ void asserted_formulas_new::compute_depth(expr* e) {
     }
 }
 
-proof * asserted_formulas_new::get_inconsistency_proof() const {
+proof * asserted_formulas::get_inconsistency_proof() const {
     if (!inconsistent())
         return 0;
     if (!m.proofs_enabled())
@@ -586,7 +586,7 @@ proof * asserted_formulas_new::get_inconsistency_proof() const {
     return 0;
 }
 
-void asserted_formulas_new::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { 
+void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { 
     expr* f = j.get_fml();
     if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) {
         TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);
@@ -597,7 +597,7 @@ void asserted_formulas_new::refine_inj_axiom_fn::simplify(justified_expr const&
 }
 
 
-unsigned asserted_formulas_new::get_total_size() const {
+unsigned asserted_formulas::get_total_size() const {
     expr_mark visited;
     unsigned r  = 0;
     for (justified_expr const& j : m_formulas)
@@ -606,7 +606,7 @@ unsigned asserted_formulas_new::get_total_size() const {
 }
 
 #ifdef Z3DEBUG
-void pp(asserted_formulas_new & f) {
+void pp(asserted_formulas & f) {
     f.display(std::cout);
 }
 #endif
diff --git a/src/smt/asserted_formulas_new.h b/src/smt/asserted_formulas.h
similarity index 88%
rename from src/smt/asserted_formulas_new.h
rename to src/smt/asserted_formulas.h
index 82f18250d..ea00cb71c 100644
--- a/src/smt/asserted_formulas_new.h
+++ b/src/smt/asserted_formulas.h
@@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation
 
 Module Name:
 
-    asserted_formulas_new.h
+    asserted_formulas.h
 
 Abstract:
 
@@ -16,8 +16,8 @@ Author:
 Revision History:
 
 --*/
-#ifndef ASSERTED_FORMULAS_NEW_H_
-#define ASSERTED_FORMULAS_NEW_H_
+#ifndef ASSERTED_FORMULAS_H_
+#define ASSERTED_FORMULAS_H_
 
 #include "util/statistics.h"
 #include "ast/static_features.h"
@@ -41,7 +41,7 @@ Revision History:
 #include "smt/elim_term_ite.h"
 
 
-class asserted_formulas_new {
+class asserted_formulas {
     
     ast_manager &               m;
     smt_params &                m_params;
@@ -66,11 +66,11 @@ class asserted_formulas_new {
 
     class simplify_fmls {
     protected:
-        asserted_formulas_new& af;
+        asserted_formulas& af;
         ast_manager&           m;
         char const*            m_id;
     public:
-        simplify_fmls(asserted_formulas_new& af, char const* id): af(af), m(af.m), m_id(id) {}
+        simplify_fmls(asserted_formulas& af, char const* id): af(af), m(af.m), m_id(id) {}
         char const* id() const { return m_id; }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
         virtual bool should_apply() const { return true;}
@@ -80,13 +80,13 @@ class asserted_formulas_new {
 
     class reduce_asserted_formulas_fn : public simplify_fmls {
     public:
-        reduce_asserted_formulas_fn(asserted_formulas_new& af): simplify_fmls(af, "reduce-asserted") {}
+        reduce_asserted_formulas_fn(asserted_formulas& af): simplify_fmls(af, "reduce-asserted") {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_rewriter(j.get_fml(), n, p); }
     };
 
     class find_macros_fn : public simplify_fmls {
     public:
-        find_macros_fn(asserted_formulas_new& af): simplify_fmls(af, "find-macros") {}
+        find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
         virtual void operator()() { af.find_macros_core(); }
         virtual bool should_apply() const { return af.m_params.m_macro_finder && af.has_quantifiers(); }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
@@ -94,7 +94,7 @@ class asserted_formulas_new {
 
     class apply_quasi_macros_fn : public simplify_fmls {
     public:
-        apply_quasi_macros_fn(asserted_formulas_new& af): simplify_fmls(af, "find-quasi-macros") {}
+        apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
         virtual void operator()() { af.apply_quasi_macros(); }
         virtual bool should_apply() const { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
@@ -102,7 +102,7 @@ class asserted_formulas_new {
 
     class nnf_cnf_fn : public simplify_fmls {
     public:
-        nnf_cnf_fn(asserted_formulas_new& af): simplify_fmls(af, "nnf-cnf") {}
+        nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
         virtual void operator()() { af.nnf_cnf(); }
         virtual bool should_apply() const { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
@@ -110,7 +110,7 @@ class asserted_formulas_new {
 
     class propagate_values_fn : public simplify_fmls {
     public:
-        propagate_values_fn(asserted_formulas_new& af): simplify_fmls(af, "propagate-values") {}
+        propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
         virtual void operator()() { af.propagate_values(); }
         virtual bool should_apply() const { return af.m_params.m_propagate_values; }
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { UNREACHABLE(); }
@@ -119,7 +119,7 @@ class asserted_formulas_new {
     class distribute_forall_fn : public simplify_fmls {
         distribute_forall m_functor;
     public:
-        distribute_forall_fn(asserted_formulas_new& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
+        distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_functor(j.get_fml(), n); }
         virtual bool should_apply() const { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
         virtual void post_op() { af.reduce_and_solve();  TRACE("asserted_formulas", af.display(tout);); }
@@ -128,21 +128,21 @@ class asserted_formulas_new {
     class pattern_inference_fn : public simplify_fmls {
         pattern_inference_rw m_infer;
     public:
-        pattern_inference_fn(asserted_formulas_new& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
+        pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_infer(j.get_fml(), n, p); }
         virtual bool should_apply() const { return af.m_params.m_ematching && af.has_quantifiers(); }
     };
 
     class refine_inj_axiom_fn : public simplify_fmls {
     public:
-        refine_inj_axiom_fn(asserted_formulas_new& af): simplify_fmls(af, "refine-injectivity") {}
+        refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p);
         virtual bool should_apply() const { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
     };
 
     class max_bv_sharing_fn : public simplify_fmls {
     public:
-        max_bv_sharing_fn(asserted_formulas_new& af): simplify_fmls(af, "maximizing-bv-sharing") {}
+        max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { af.m_bv_sharing(j.get_fml(), n, p); }
         virtual bool should_apply() const { return af.m_params.m_max_bv_sharing; }
         virtual void post_op() { af.m_reduce_asserted_formulas(); }
@@ -151,7 +151,7 @@ class asserted_formulas_new {
     class elim_term_ite_fn : public simplify_fmls {
         elim_term_ite_rw m_elim;
     public:
-        elim_term_ite_fn(asserted_formulas_new& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
+        elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { m_elim(j.get_fml(), n, p); }
         virtual bool should_apply() const { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
         virtual void post_op() { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
@@ -161,7 +161,7 @@ class asserted_formulas_new {
     class NAME : public simplify_fmls {                                 \
         FUNCTOR m_functor;                                              \
     public:                                                             \
-        NAME(asserted_formulas_new& af):simplify_fmls(af, MSG), m_functor ARG {} \
+        NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \
         virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
             m_functor(j.get_fml(), n, p);                               \
         }                                                               \
@@ -221,8 +221,8 @@ class asserted_formulas_new {
     bool pull_cheap_ite_trees();
 
 public:
-    asserted_formulas_new(ast_manager & m, smt_params & p);
-    ~asserted_formulas_new();
+    asserted_formulas(ast_manager & m, smt_params & p);
+    ~asserted_formulas();
 
     bool has_quantifiers() const { return m_has_quantifiers; }
     void setup();
@@ -265,5 +265,5 @@ public:
 
 };
 
-#endif /* ASSERTED_FORMULAS_NEW_H_ */
+#endif /* ASSERTED_FORMULAS_H_ */
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7b92bdd28..eef84f773 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -148,8 +148,8 @@ namespace smt {
         dst_ctx.set_logic(src_ctx.m_setup.get_logic());
         dst_ctx.copy_plugins(src_ctx, dst_ctx);
 
-        asserted_formulas_new& src_af = src_ctx.m_asserted_formulas;
-        asserted_formulas_new& dst_af = dst_ctx.m_asserted_formulas;
+        asserted_formulas& src_af = src_ctx.m_asserted_formulas;
+        asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;
 
         // Copy asserted formulas.
         for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index a6a67702a..3cc577b29 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -36,7 +36,7 @@ Revision History:
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
-#include "smt/asserted_formulas_new.h"
+#include "smt/asserted_formulas.h"
 #include "smt/smt_types.h"
 #include "smt/dyn_ack.h"
 #include "ast/ast_smt_pp.h"
@@ -81,7 +81,7 @@ namespace smt {
         params_ref                  m_params;
         setup                       m_setup;
         timer                       m_timer;
-        asserted_formulas_new       m_asserted_formulas;
+        asserted_formulas           m_asserted_formulas;
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 70355502d..16a49961e 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -395,7 +395,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_div(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r(1);
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
@@ -419,7 +420,8 @@ namespace smt {
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_mod(app * n) {
         TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r(1);
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s      = mk_binary_op(n);
         context & ctx     = get_context();
         if (!ctx.relevancy())
@@ -429,7 +431,8 @@ namespace smt {
 
     template<typename Ext>
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
-        if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
+        rational r(1);
+        if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n);
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
         if (!ctx.relevancy()) {
@@ -734,11 +737,6 @@ namespace smt {
             return internalize_div(n);
         else if (m_util.is_idiv(n))
             return internalize_idiv(n);
-        else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) {
-            ctx.internalize(n->get_arg(0), false);
-            enode * e = mk_enode(n);
-            return mk_var(e);
-        }
         else if (m_util.is_mod(n)) 
             return internalize_mod(n);
         else if (m_util.is_rem(n)) 
@@ -1226,7 +1224,8 @@ namespace smt {
         app * rhs      = to_app(n->get_arg(1));
         expr * rhs2;
         if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); }
-        if (!m_util.is_numeral(rhs)) {
+        if (!m_util.is_numeral(rhs)) {        
+            UNREACHABLE();
             throw default_exception("malformed atomic constraint");
         }
         theory_var v   = internalize_term_core(lhs);
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index c7a3d7920..274f89e8b 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -516,7 +516,8 @@ namespace smt {
 
         expr_ref sel1(m), sel2(m);
         sel1 = mk_select(args1.size(), args1.c_ptr());
-        sel2 = ctx.get_rewriter().mk_app(f, args2.size(), args2.c_ptr());
+        sel2 = m.mk_app(f, args2.size(), args2.c_ptr());
+        ctx.get_rewriter()(sel2);
         ctx.internalize(sel1, false);
         ctx.internalize(sel2, false);
         
@@ -537,6 +538,7 @@ namespace smt {
         SASSERT(is_map(mp));
                 
         app* map = mp->get_owner();
+        ast_manager& m = get_manager();
         context& ctx = get_context();
         if (!ctx.add_fingerprint(this, 0, 1, &mp)) {
             return false;
@@ -552,9 +554,9 @@ namespace smt {
             args2.push_back(mk_default(map->get_arg(i)));
         }
 
+        expr_ref def2(m.mk_app(f, args2.size(), args2.c_ptr()), m);
+        ctx.get_rewriter()(def2);
         expr* def1 = mk_default(map);
-        expr_ref def2(get_manager());
-        def2 = ctx.get_rewriter().mk_app(f, args2.size(), args2.c_ptr());
         ctx.internalize(def1, false);
         ctx.internalize(def2, false);
         return try_assign_eq(def1, def2);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0c09d0403..dd044b78a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -293,9 +293,6 @@ namespace smt {
         }
 
         void found_not_handled(expr* n) {
-            if (a.is_div0(n)) {
-                return;
-            }
             m_not_handled = n;
             if (is_app(n) && is_underspecified(to_app(n))) {
                 m_underspecified.push_back(to_app(n));
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 0443a51ed..17a69f93e 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -301,7 +301,7 @@ struct purify_arith_proc {
             if (complete()) {
                 // y != 0 \/ k = div-0(x)
                 push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
-                              EQ(k, u().mk_div0(x))));
+                              EQ(k, u().mk_div(x, mk_real_zero()))));
                 push_cnstr_pr(result_pr);
             }
         }
@@ -349,10 +349,10 @@ struct purify_arith_proc {
             push_cnstr_pr(mod_pr);
 
             if (complete()) {
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x))));
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero))));
                 push_cnstr_pr(result_pr);
 
-                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x))));
+                push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero))));
                 push_cnstr_pr(mod_pr);
             }
         }
@@ -414,7 +414,7 @@ struct purify_arith_proc {
                 // (^ x 0) --> k  |  x != 0 implies k = 1,   x = 0 implies k = 0^0 
                 push_cnstr(OR(EQ(x, zero), EQ(k, one)));
                 push_cnstr_pr(result_pr);
-                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real())));
+                push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, u().mk_power(zero, zero))));
                 push_cnstr_pr(result_pr);
             }
             else if (!is_int) {