diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index e855ec262..9eb9bf70c 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -988,6 +988,12 @@ void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
     } 
     UNREACHABLE(); 
 } 
+
+static rational symmod(rational const& a, rational const& b) {
+    rational r = mod(a, b);
+    if (2*r > b) r -= b;
+    return r;
+}
     
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
     set_curr_sort(m().get_sort(arg1));
@@ -1031,6 +1037,10 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
                 change = true;
                 args.push_back(t1);
             }
+            else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) {
+                change = true;
+                args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2));
+            }
             else {
                 args.push_back(arg);
             }
diff --git a/src/tactic/arith/bound_propagator.cpp b/src/tactic/arith/bound_propagator.cpp
index 4ddfe9721..3c4844462 100644
--- a/src/tactic/arith/bound_propagator.cpp
+++ b/src/tactic/arith/bound_propagator.cpp
@@ -84,10 +84,8 @@ bound_propagator::~bound_propagator() {
 }
 
 void bound_propagator::del_constraints_core() {
-    constraint_vector::iterator it  = m_constraints.begin();
-    constraint_vector::iterator end = m_constraints.end();
-    for (; it != end; ++it) {
-        del_constraint(*it);
+    for (auto & c : m_constraints) {
+        del_constraint(c);
     }
     m_constraints.reset();
 }
@@ -98,10 +96,9 @@ void bound_propagator::del_constraints() {
         return;
     del_constraints_core();
     m_constraints.finalize();
-    vector<wlist>::iterator it  = m_watches.begin();
-    vector<wlist>::iterator end = m_watches.end();
-    for (; it != end; ++it)
-        it->finalize();
+    for (auto& wl : m_watches) {
+        wl.finalize();
+    }
 }
 
 void bound_propagator::del_constraint(constraint & c) {
@@ -164,10 +161,8 @@ void bound_propagator::del_var(var x) {
     m_dead[x] = true;
     // mark constraints containing x as dead.
     wlist & wl = m_watches[x];
-    wlist::iterator it  = wl.begin();
-    wlist::iterator end = wl.end();
-    for (; it != end; ++it) {
-        m_constraints[*it].m_dead = true;
+    for (auto c : wl) {
+        m_constraints[c].m_dead = true;
     }
 }
 
@@ -473,10 +468,7 @@ void bound_propagator::propagate() {
         TRACE("bound_propagator_detail", tout << "propagating x" << x << "\n";);
         m_qhead++;
         wlist const & wl = m_watches[x];
-        wlist::const_iterator it  = wl.begin();
-        wlist::const_iterator end = wl.end();
-        for (; it != end; ++it) {
-            unsigned c_idx = *it;
+        for (unsigned c_idx : wl) {
             constraint & c = m_constraints[c_idx];
             // We don't need to visit c if it was already propagated using b.
             // Whenever we visit c we store in c.m_timestamp the current timestamp
@@ -490,10 +482,8 @@ void bound_propagator::propagate() {
         }
     }
 
-    unsigned_vector::iterator it  =  m_to_reset_ts.begin();
-    unsigned_vector::iterator end =  m_to_reset_ts.end();
-    for (; it != end; ++it)
-        m_constraints[*it].m_timestamp = 0;
+    for (unsigned c : m_to_reset_ts) 
+        m_constraints[c].m_timestamp = 0;
 }
 
 bool bound_propagator::propagate(unsigned c_idx) {
@@ -936,10 +926,7 @@ void bound_propagator::display_bounds(std::ostream & out, bool approx, bool prec
 }
 
 void bound_propagator::display_constraints(std::ostream & out) const {
-    constraint_vector::const_iterator it  = m_constraints.begin();
-    constraint_vector::const_iterator end = m_constraints.end();
-    for (; it != end; ++it) {
-        constraint const & c = *it;
+    for (constraint const& c : m_constraints) {
         if (c.m_kind == LINEAR) {
             m_eq_manager.display(out, *(c.m_eq));
             out << "\n";
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 52d43f109..0978f3aa6 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -327,28 +327,53 @@ class solve_eqs_tactic : public tactic {
                 pr = m().mk_rewrite(eq, m().mk_eq(var, def));
             return true;
         }
+
+        bool solve_mod(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
+            rational r1, r2;
+            expr* arg1, *arg2, *arg3, *arg4;
+            if (m_produce_proofs) {
+                return false;
+            }
+            VERIFY(m_a_util.is_mod(lhs, arg1, arg2));
+            if (!m_a_util.is_numeral(arg2, r1) || !r1.is_pos()) {
+                return false;
+            }
+            if (m_a_util.is_mod(rhs, arg3, arg4) && m_a_util.is_numeral(arg4, r2) && r1 == r2) {
+                rhs = arg3;
+            }
+            else if (!m_a_util.is_numeral(rhs, r2) || !r2.is_zero()) {
+                return false;
+            }
+            if (solve_eq(arg1, rhs, eq, var, def, pr)) {
+                def = m_a_util.mk_add(def, m_a_util.mk_mul(m().mk_fresh_const("mod", m_a_util.mk_int()), m_a_util.mk_int(r1)));
+                return true;
+            }
+            return false;
+        }
         
         bool solve_arith(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
             return 
                 (m_a_util.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, def, pr)) ||
-                (m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr));
-#if 0
-            // better done inside of nlsat
-                (m_a_util.is_add(lhs) && solve_nl(to_app(lhs), rhs, eq, var, def, pr)) ||
-                (m_a_util.is_add(rhs) && solve_nl(to_app(rhs), lhs, eq, var, def, pr));
-#endif
+                (m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr)) ||
+                (m_a_util.is_mod(lhs) && solve_mod(lhs, rhs, eq, var, def, pr)) ||
+                (m_a_util.is_mod(rhs) && solve_mod(rhs, lhs, eq, var, def, pr));                 
+        }
+
+                
+        bool solve_eq(expr* arg1, expr* arg2, expr* eq, app_ref& var, expr_ref & def, proof_ref& pr) {
+            if (trivial_solve(arg1, arg2, var, def, pr))
+                return true;
+            if (m_theory_solver) {
+                if (solve_arith(arg1, arg2, eq, var, def, pr))
+                    return true;
+            }
+            return false;
         }
         
         bool solve(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) {
             expr* arg1 = nullptr, *arg2 = nullptr;
             if (m().is_eq(f, arg1, arg2)) {
-                if (trivial_solve(arg1, arg2, var, def, pr))
-                    return true;
-                if (m_theory_solver) {
-                    if (solve_arith(arg1, arg2, f, var, def, pr))
-                        return true;
-                }
-                return false;
+                return solve_eq(arg1, arg2, f, var, def, pr);
             }
                         
 #if 0
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 2872d9454..cd956f3c6 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -54,7 +54,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
     return r;
 }
 
-static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
+static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
     params_ref pull_ite_p = p_ref;
     pull_ite_p.set_bool("pull_cheap_ite", true);
     pull_ite_p.set_bool("local_ctx", true);
@@ -115,7 +115,7 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
 
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
-        mk_qfnia_premable(m, p),
+        mk_qfnia_preamble(m, p),
                 
         or_else(mk_qfnia_sat_solver(m, p),
                 try_for(mk_qfnia_smt_solver(m, p), 2000),