diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
index 49362940d..8aa961686 100644
--- a/src/ast/justified_expr.h
+++ b/src/ast/justified_expr.h
@@ -21,12 +21,12 @@ public:
     justified_expr& operator=(justified_expr const& other) {
         SASSERT(&m == &other.m);
         if (this != &other) {
+            m.inc_ref(other.get_fml());
+            m.inc_ref(other.get_proof());
             m.dec_ref(m_fml);
             m.dec_ref(m_proof);
             m_fml = other.get_fml();
             m_proof = other.get_proof();
-            m.inc_ref(m_fml);
-            m.inc_ref(m_proof);
         }
         return *this;
     }
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index c1ef61938..b630cdff6 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -26,7 +26,6 @@ void arith_rewriter::updt_local_params(params_ref const & _p) {
     arith_rewriter_params p(_p);
     m_arith_lhs       = p.arith_lhs();
     m_gcd_rounding    = p.gcd_rounding();
-    m_eq2ineq         = p.eq2ineq();
     m_elim_to_real    = p.elim_to_real();
     m_push_to_real    = p.push_to_real();
     m_anum_simp       = p.algebraic_number_evaluator();
@@ -371,7 +370,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
     if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) ||
         (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ)))
         return reduce_power(arg1, arg2, kind, result);
-    br_status st = cancel_monomials(arg1, arg2, m_arith_lhs, new_arg1, new_arg2);
+    br_status st = cancel_monomials(arg1, arg2, true, new_arg1, new_arg2);
     TRACE("mk_le_bug", tout << "st: " << st << " " << new_arg1 << " " << new_arg2 << "\n";);
     if (st != BR_FAILED) {
         arg1 = new_arg1;
@@ -455,11 +454,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
             st = BR_DONE;
         }
     }
-    if (kind == EQ && m_expand_eqs) {
-        result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
-        return BR_REWRITE2;
-    }
-    else if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
+    if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
         a2.neg();
         new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
         switch (kind) {
@@ -500,12 +495,19 @@ br_status arith_rewriter::mk_gt_core(expr * arg1, expr * arg2, expr_ref & result
     return BR_REWRITE2;
 }
 
+bool arith_rewriter::is_arith_term(expr * n) const {
+    return n->get_kind() == AST_APP && to_app(n)->get_family_id() == get_fid();
+}
+
 br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
-    if (m_eq2ineq) {
+    if (m_expand_eqs) {
         result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
         return BR_REWRITE2;
     }
-    return mk_le_ge_eq_core(arg1, arg2, EQ, result);
+    if (m_arith_lhs || is_arith_term(arg1) || is_arith_term(arg2)) {
+        return mk_le_ge_eq_core(arg1, arg2, EQ, result);
+    }
+    return BR_FAILED;
 }
 
 expr_ref arith_rewriter::neg_monomial(expr* e) const {
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 352cb5a6c..f1e4c4396 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -50,12 +50,12 @@ public:
 class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     bool m_arith_lhs;
     bool m_gcd_rounding;
-    bool m_eq2ineq;
     bool m_elim_to_real;
     bool m_push_to_real;
     bool m_anum_simp;
     bool m_elim_rem;
     bool m_expand_eqs;
+    bool m_process_all_eqs;
     unsigned m_max_degree;
 
     void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts);
@@ -83,6 +83,8 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     expr * reduce_power(expr * arg, bool is_eq);
     br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
 
+    bool is_arith_term(expr * n) const;
+
     bool is_pi_multiple(expr * t, rational & k);
     bool is_pi_offset(expr * t, rational & k, expr * & m);
     bool is_2_pi_integer(expr * t);
diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg
index 94ada1b6d..9a6c6c1c0 100644
--- a/src/ast/rewriter/arith_rewriter_params.pyg
+++ b/src/ast/rewriter/arith_rewriter_params.pyg
@@ -6,7 +6,6 @@ def_module_params(module_name='rewriter',
                           ("expand_power", BOOL, False, "expand (^ t k) into (* t ... t) if  1 < k <= max_degree."),
                           ("expand_tan", BOOL, False, "replace (tan x) with (/ (sin x) (cos x))."),
                           ("max_degree", UINT, 64, "max degree of algebraic numbers (and power operators) processed by simplifier."),
-                          ("eq2ineq", BOOL, False, "split arithmetic equalities into two inequalities."),
                           ("sort_sums", BOOL, False, "sort the arguments of + application."),
                           ("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."),
                           ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."),
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 75f931c1d..ce35300ca 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -20,6 +20,7 @@ Notes:
 #include "ast/rewriter/bv_rewriter_params.hpp"
 #include "ast/rewriter/poly_rewriter_def.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_lt.h"
 
 
 void bv_rewriter::updt_local_params(params_ref const & _p) {
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 8cbc7f864..c00464383 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -48,7 +48,6 @@ protected:
     decl_kind power_decl_kind() const { return Config::power_decl_kind(); }
     bool is_power(expr * t) const { return is_app_of(t, get_fid(), power_decl_kind()); }
     expr * get_power_body(expr * t, rational & k);
-    struct mon_pw_lt; // functor used to sort monomial elements when use_power() == true
 
     expr * mk_mul_app(unsigned num_args, expr * const * args);
     expr * mk_mul_app(numeral const & c, expr * arg);
@@ -85,6 +84,14 @@ protected:
     bool is_mul(expr * t, numeral & c, expr * & pp);
     void hoist_cmul(expr_ref_buffer & args);
 
+    class mon_lt {
+        poly_rewriter& rw;
+        int ordinal(expr* e) const;
+    public:
+        mon_lt(poly_rewriter& rw): rw(rw) {}
+        bool operator()(expr* e1, expr * e2) const;
+    };
+
 public:
     poly_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         Config(m),
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 85044af08..8fda040b6 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -18,7 +18,7 @@ Notes:
 --*/
 #include "ast/rewriter/poly_rewriter.h"
 #include "ast/rewriter/poly_rewriter_params.hpp"
-#include "ast/ast_lt.h"
+// include "ast/ast_lt.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -191,21 +191,9 @@ br_status poly_rewriter<Config>::mk_flat_mul_core(unsigned num_args, expr * cons
 }
 
 
-template<typename Config>
-struct poly_rewriter<Config>::mon_pw_lt {
-    poly_rewriter<Config> & m_owner;
-    mon_pw_lt(poly_rewriter<Config> & o):m_owner(o) {}
-    
-    bool operator()(expr * n1, expr * n2) const { 
-        rational k;
-        return lt(m_owner.get_power_body(n1, k), 
-                  m_owner.get_power_body(n2, k));
-    }
-};
-
-
 template<typename Config>
 br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    mon_lt lt(*this);
     SASSERT(num_args >= 2);
     // cheap case
     numeral a;
@@ -320,11 +308,8 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
         if (ordered && num_coeffs == 0 && !use_power())
             return BR_FAILED;
         if (!ordered) {
-            if (use_power())
-                std::sort(new_args.begin(), new_args.end(), mon_pw_lt(*this));
-            else
-                std::sort(new_args.begin(), new_args.end(), ast_to_lt());
-            TRACE("poly_rewriter",
+            std::sort(new_args.begin(), new_args.end(), lt);
+        TRACE("poly_rewriter",
                   tout << "after sorting:\n";
                   for (unsigned i = 0; i < new_args.size(); i++) {
                       if (i > 0)
@@ -498,8 +483,43 @@ void poly_rewriter<Config>::hoist_cmul(expr_ref_buffer & args) {
     args.resize(j);
 }
 
+template<typename Config>
+bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
+    return ordinal(e1) < ordinal(e2);
+}
+
+inline bool is_essentially_var(expr * n, family_id fid) {
+    SASSERT(is_var(n) || is_app(n));
+    return is_var(n) || to_app(n)->get_family_id() != fid;
+}
+
+template<typename Config>
+int poly_rewriter<Config>::mon_lt::ordinal(expr* e) const {
+    rational k;
+    if (is_essentially_var(e, rw.get_fid())) {
+        return e->get_id();
+    }
+    else if (rw.is_mul(e)) {
+        if (rw.is_numeral(to_app(e)->get_arg(0)))
+            return to_app(e)->get_arg(1)->get_id();
+        else
+            return e->get_id();
+    }
+    else if (rw.is_numeral(e)) {
+        return -1;
+    }
+    else if (rw.use_power() && rw.is_power(e) && rw.is_numeral(to_app(e)->get_arg(1), k) && k > rational(1)) {
+        return to_app(e)->get_arg(0)->get_id();
+    }
+    else {
+        return e->get_id();
+    }
+}
+
+
 template<typename Config>
 br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    mon_lt lt(*this);
     SASSERT(num_args >= 2);
     numeral c;
     unsigned num_coeffs = 0;
@@ -591,9 +611,9 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
         else if (m_sort_sums) {
             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());
+                std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), mon_lt(*this));
             else
-                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
+                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), mon_lt(*this));
         }
         result = mk_add_app(new_args.size(), new_args.c_ptr());
         TRACE("rewriter", tout << result << "\n";);
@@ -624,10 +644,10 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
         }
         else if (!ordered) {
             if (c.is_zero())
-                std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
+                std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), lt);
             else 
-                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
-        }
+                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), lt);
+    }
         result = mk_add_app(new_args.size(), new_args.c_ptr());        
         if (hoist_multiplication(result)) {
             return BR_REWRITE_FULL;
@@ -681,6 +701,7 @@ br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args,
 template<typename Config>
 br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) {
     set_curr_sort(m().get_sort(lhs));
+    mon_lt lt(*this);
     unsigned lhs_sz;
     expr * const * lhs_monomials = get_monomials(lhs, lhs_sz);
     unsigned rhs_sz;
@@ -831,7 +852,7 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
     if (move) {
         if (m_sort_sums) { 
             // + 1 to skip coefficient
-            std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), ast_to_lt());
+            std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), lt);
         }
         c_at_rhs = true;
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f172e5e93..d1b8f7f78 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -585,10 +585,8 @@ void cmd_context::register_builtin_sorts(decl_plugin * p) {
     svector<builtin_name> names;
     p->get_sort_names(names, m_logic);
     family_id fid = p->get_family_id();
-    svector<builtin_name>::const_iterator it  = names.begin();
-    svector<builtin_name>::const_iterator end = names.end();
-    for (; it != end; ++it) {
-        psort_decl * d = pm().mk_psort_builtin_decl((*it).m_name, fid, (*it).m_kind);
+    for (builtin_name const& n : names) {
+        psort_decl * d = pm().mk_psort_builtin_decl(n.m_name, fid, n.m_kind);
         insert(d);
     }
 }
@@ -597,17 +595,15 @@ void cmd_context::register_builtin_ops(decl_plugin * p) {
     svector<builtin_name> names;
     p->get_op_names(names, m_logic);
     family_id fid = p->get_family_id();
-    svector<builtin_name>::const_iterator it  = names.begin();
-    svector<builtin_name>::const_iterator end = names.end();
-    for (; it != end; ++it) {
-        if (m_builtin_decls.contains((*it).m_name)) {
-            builtin_decl & d = m_builtin_decls.find((*it).m_name);
-            builtin_decl * new_d = alloc(builtin_decl, fid, (*it).m_kind, d.m_next);
+    for (builtin_name const& n : names) {
+        if (m_builtin_decls.contains(n.m_name)) {
+            builtin_decl & d = m_builtin_decls.find(n.m_name);
+            builtin_decl * new_d = alloc(builtin_decl, fid, n.m_kind, d.m_next);
             d.m_next = new_d;
             m_extra_builtin_decls.push_back(new_d);
         }
         else {
-            m_builtin_decls.insert((*it).m_name, builtin_decl(fid, (*it).m_kind));
+            m_builtin_decls.insert(n.m_name, builtin_decl(fid, n.m_kind));
         }
     }
 }
@@ -693,10 +689,8 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
-        svector<family_id>::iterator it  = fids.begin();
-        svector<family_id>::iterator end = fids.end();
-        for (; it != end; ++it) {
-            decl_plugin * p = m_manager->get_plugin(*it);
+        for (family_id fid : fids) {
+            decl_plugin * p = m_manager->get_plugin(fid);
             if (p) {
                 register_builtin_sorts(p);
                 register_builtin_ops(p);
@@ -1148,11 +1142,8 @@ void cmd_context::erase_object_ref(symbol const & s) {
 }
 
 void cmd_context::reset_func_decls() {
-    dictionary<func_decls>::iterator  it  = m_func_decls.begin();
-    dictionary<func_decls>::iterator  end = m_func_decls.end();
-    for (; it != end; ++it) {
-        func_decls fs = (*it).m_value;
-        fs.finalize(m());
+    for (auto & kv : m_func_decls) {
+        kv.m_value.finalize(m());
     }
     m_func_decls.reset();
     m_func_decls_stack.reset();
@@ -1160,10 +1151,8 @@ void cmd_context::reset_func_decls() {
 }
 
 void cmd_context::reset_psort_decls() {
-    dictionary<psort_decl*>::iterator  it  = m_psort_decls.begin();
-    dictionary<psort_decl*>::iterator  end = m_psort_decls.end();
-    for (; it != end; ++it) {
-        psort_decl * p = (*it).m_value;
+    for (auto & kv : m_psort_decls) {
+        psort_decl * p = kv.m_value;
         pm().dec_ref(p);
     }
     m_psort_decls.reset();
@@ -1179,19 +1168,14 @@ void cmd_context::reset_macros() {
 }
 
 void cmd_context::reset_cmds() {
-    dictionary<cmd*>::iterator  it  = m_cmds.begin();
-    dictionary<cmd*>::iterator  end = m_cmds.end();
-    for (; it != end; ++it) {
-        cmd * c = (*it).m_value;
-        c->reset(*this);
+    for (auto& kv : m_cmds) {
+        kv.m_value->reset(*this);
     }
 }
 
 void cmd_context::finalize_cmds() {
-    dictionary<cmd*>::iterator  it  = m_cmds.begin();
-    dictionary<cmd*>::iterator  end = m_cmds.end();
-    for (; it != end; ++it) {
-        cmd * c = (*it).m_value;
+    for (auto& kv : m_cmds) {
+        cmd * c = kv.m_value;
         c->finalize(*this);
         dealloc(c);
     }
@@ -1204,10 +1188,8 @@ void cmd_context::reset_user_tactics() {
 }
 
 void cmd_context::reset_object_refs() {
-    dictionary<object_ref*>::iterator it  = m_object_refs.begin();
-    dictionary<object_ref*>::iterator end = m_object_refs.end();
-    for (; it != end; ++it) {
-        object_ref * r = (*it).m_value;
+    for (auto& kv : m_object_refs) {
+        object_ref * r = kv.m_value;
         r->dec_ref(*this);
     }
     m_object_refs.reset();
@@ -1541,10 +1523,8 @@ void cmd_context::reset_assertions() {
         mk_solver();
     }
     restore_assertions(0);
-    svector<scope>::iterator it  = m_scopes.begin();
-    svector<scope>::iterator end = m_scopes.end();
-    for (; it != end; ++it) {
-        it->m_assertions_lim = 0;
+    for (scope& s : m_scopes) {
+        s.m_assertions_lim = 0;
         if (m_solver) m_solver->push();
     }
 }
@@ -1717,10 +1697,7 @@ void cmd_context::set_solver_factory(solver_factory * f) {
         mk_solver();
         // assert formulas and create scopes in the new solver.
         unsigned lim = 0;
-        svector<scope>::iterator it  = m_scopes.begin();
-        svector<scope>::iterator end = m_scopes.end();
-        for (; it != end; ++it) {
-            scope & s = *it;
+        for (scope& s : m_scopes) {
             for (unsigned i = lim; i < s.m_assertions_lim; i++) {
                 m_solver->assert_expr(m_assertions[i]);
             }
@@ -1757,11 +1734,9 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
 void cmd_context::display_assertions() {
     if (!m_interactive_mode)
         throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
-    std::vector<std::string>::const_iterator it  = m_assertion_strings.begin();
-    std::vector<std::string>::const_iterator end = m_assertion_strings.end();
     regular_stream() << "(";
-    for (bool first = true; it != end; ++it) {
-        std::string const & s = *it;
+    bool first = true;
+    for (std::string const& s : m_assertion_strings) {
         if (first)
             first = false;
         else
@@ -1837,10 +1812,8 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
 }
 
 void cmd_context::dump_assertions(std::ostream & out) const {
-    ptr_vector<expr>::const_iterator it  = m_assertions.begin();
-    ptr_vector<expr>::const_iterator end = m_assertions.end();
-    for (; it != end; ++it) {
-        display(out, *it);
+    for (expr * e : m_assertions) {
+        display(out, e);
         out << std::endl;
     }
 }
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index fb2004c77..7dca13c07 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -120,7 +120,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
 void asserted_formulas::set_eliminate_and(bool flag) {
     params_ref p;
     p.set_bool("elim_and", flag);
-    p.set_bool("arith_lhs", true);
+//    p.set_bool("arith_lhs", true);
     p.set_bool("sort_sums", true);
     p.set_bool("rewrite_patterns", true);
     p.set_bool("expand_eqs", m_params.m_arith_expand_eqs);
@@ -429,7 +429,6 @@ void asserted_formulas::commit(unsigned new_qhead) {
 }
 
 void asserted_formulas::propagate_values() {
-    TRACE("propagate_values", tout << "before:\n"; display(tout););
     flush_cache();
 
     unsigned num_prop = 0;
@@ -466,7 +465,7 @@ void asserted_formulas::propagate_values() {
 }
 
 unsigned asserted_formulas::propagate_values(unsigned i) {
-    expr * n = m_formulas[i].get_fml();
+    expr_ref n(m_formulas[i].get_fml(), m);
     expr_ref new_n(m);                                                  
     proof_ref new_pr(m);                                                
     m_rewriter(n, new_n, new_pr);                                       
@@ -476,6 +475,9 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
     }
     justified_expr j(m, new_n, new_pr);
     m_formulas[i] = j;
+    if (m_formulas[i].get_fml() != new_n) {
+        std::cout << "NOT updated\n";
+    }
     if (m.is_false(j.get_fml())) {
         m_inconsistent = true;
     }