diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 9824884a4..379020331 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -800,52 +800,105 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
-    expr_ref quot(m());
-    if (divides(arg1, arg2, quot)) {
-        result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
-        return BR_REWRITE2;
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
+        result = arg1;
+        return BR_DONE;
+    }
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
+        return BR_FAILED;
+    }
+    if (arg1 == arg2) {
+        expr_ref zero(m_util.mk_int(0), m());
+        result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
+        return BR_REWRITE3;
+    }
+    if (divides(arg1, arg2, result)) {
+        return BR_REWRITE_FULL;
     }
     return BR_FAILED;
 }
 
-bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
-    if (d == n) {
-        quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
+
+// 
+// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
+//
+bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
+    expr_fast_mark1 mark;
+    rational num_r(1), den_r(1);
+    expr* num_e = nullptr, *den_e = nullptr;
+    ptr_buffer<expr> args1, args2;
+    flat_mul(num, args1);
+    flat_mul(den, args2);
+    for (expr * arg : args1) {
+        mark.mark(arg);
+        if (m_util.is_numeral(arg, num_r)) num_e = arg;
+    }
+    for (expr* arg : args2) {
+        if (mark.is_marked(arg)) {
+            result = remove_divisor(arg, num, den);
+            return true;
+        }
+        if (m_util.is_numeral(arg, den_r)) den_e = arg;
+    }
+    rational g = gcd(num_r, den_r);
+    if (!g.is_one()) {
+        SASSERT(g.is_pos());
+        // replace num_e, den_e by their gcd reduction.
+        for (unsigned i = 0; i < args1.size(); ++i) {
+            if (args1[i] == num_e) {
+                args1[i] = m_util.mk_numeral(num_r / g, true);
+                break;
+            }
+        }
+        for (unsigned i = 0; i < args2.size(); ++i) {
+            if (args2[i] == den_e) {
+                args2[i] = m_util.mk_numeral(den_r / g, true);
+                break;
+            }
+        }
+        
+        num = m_util.mk_mul(args1.size(), args1.c_ptr());
+        den = m_util.mk_mul(args2.size(), args2.c_ptr());
+        result = m_util.mk_idiv(num, den);
         return true;
     }
-    if (m_util.is_mul(n)) {
-        expr_ref_vector muls(m());
-        muls.push_back(n);
-        expr* n1, *n2;
-        rational r1, r2;
-        for (unsigned i = 0; i < muls.size(); ++i) {
-            if (m_util.is_mul(muls[i].get(), n1, n2)) {
-                muls[i] = n1;
-                muls.push_back(n2);
-                --i;
-            }
-        }
-        if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
-            for (unsigned i = 0; i < muls.size(); ++i) {
-                if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
-                    muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
-                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
-                    return true;
-                }            
-            }
-        }
-        else {
-            for (unsigned i = 0; i < muls.size(); ++i) {
-                if (d == muls[i].get()) {
-                    muls[i] = muls.back();
-                    muls.pop_back();
-                    quot = m_util.mk_mul(muls.size(), muls.c_ptr());
-                    return true;
-                }            
-            }
+    return false;
+}
+
+expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
+    ptr_buffer<expr> args1, args2;
+    flat_mul(num, args1);
+    flat_mul(den, args2);
+    remove_divisor(arg, args1);
+    remove_divisor(arg, args2);
+    expr_ref zero(m_util.mk_int(0), m());
+    num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr());
+    den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr());
+    return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m());
+}
+
+void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
+    args.push_back(e);
+    for (unsigned i = 0; i < args.size(); ++i) {
+        e = args[i];
+        if (m_util.is_mul(e)) {
+            args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            args[i] = args.back();
+            args.shrink(args.size()-1);
+            --i;
+        }                
+    }
+}
+
+void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (args[i] == d) {
+            args[i] = args.back();
+            args.shrink(args.size()-1);
+            return;
         }
     }
-    return false;
+    UNREACHABLE();
 }
 
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h
index 65fbfb43f..fa8677941 100644
--- a/src/ast/rewriter/arith_rewriter.h
+++ b/src/ast/rewriter/arith_rewriter.h
@@ -95,7 +95,10 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     expr_ref neg_monomial(expr * e) const;
     expr * mk_sin_value(rational const & k);
     app * mk_sqrt(rational const & k);
-    bool divides(expr* d, expr* n, expr_ref& quot);
+    bool divides(expr* d, expr* n, expr_ref& result);
+    expr_ref remove_divisor(expr* arg, expr* num, expr* den);
+    void flat_mul(expr* e, ptr_buffer<expr>& args);
+    void remove_divisor(expr* d, ptr_buffer<expr>& args);
 
 public:
     arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index d31cbc905..ff62dacec 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -865,9 +865,7 @@ namespace smt {
            That is, during execution time, the variables will be already bound
          */
         bool all_args_are_bound_vars(app * n) {
-            unsigned num_args = n->get_num_args();
-            for (unsigned i = 0; i < num_args; i++) {
-                expr * arg = n->get_arg(i);
+            for (expr* arg : *n) {
                 if (!is_var(arg))
                     return false;
                 if (m_vars[to_var(arg)->get_idx()] == -1)
@@ -884,9 +882,7 @@ namespace smt {
             if (n->is_ground()) {
                 return;
             }
-            unsigned num_args = n->get_num_args();
-            for (unsigned i = 0; i < num_args; i++) {
-                expr * arg = n->get_arg(i);
+            for (expr* arg : *n) {
                 if (is_var(arg)) {
                     sz++;
                     unsigned var_id = to_var(arg)->get_idx();
@@ -928,10 +924,7 @@ namespace smt {
             unsigned      first_app_sz;
             unsigned      first_app_num_unbound_vars;
             // generate first the non-BIND operations
-            unsigned_vector::iterator it  = m_todo.begin();
-            unsigned_vector::iterator end = m_todo.end();
-            for (; it != end; ++it) {
-                unsigned reg = *it;
+            for (unsigned reg : m_todo) {
                 expr *  p    = m_registers[reg];
                 SASSERT(!is_quantifier(p));
                 if (is_var(p)) {
@@ -1249,10 +1242,7 @@ namespace smt {
             SASSERT(head->m_next == 0);
             m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
 
-            ptr_vector<instruction>::iterator it  = m_seq.begin();
-            ptr_vector<instruction>::iterator end = m_seq.end();
-            for (; it != end; ++it) {
-                instruction * curr = *it;
+            for (instruction * curr : m_seq) {
                 head->m_next = curr;
                 head = curr;
             }
@@ -1495,10 +1485,8 @@ namespace smt {
             }
             if (num_instr > SIMPLE_SEQ_THRESHOLD || (curr != nullptr && curr->m_opcode == CHOOSE))
                 simple = false;
-            unsigned_vector::iterator it  = m_to_reset.begin();
-            unsigned_vector::iterator end = m_to_reset.end();
-            for (; it != end; ++it)
-                m_registers[*it] = 0;
+            for (unsigned reg : m_to_reset) 
+                m_registers[reg] = 0;
             return weight;
         }
 
@@ -1716,11 +1704,9 @@ namespace smt {
                     m_num_choices++;
                     // set: head -> c1 -> c2 -> c3 -> new_child_head1
                     curr = head;
-                    ptr_vector<instruction>::iterator it1  = m_compatible.begin();
-                    ptr_vector<instruction>::iterator end1 = m_compatible.end();
-                    for (; it1 != end1; ++it1) {
-                        set_next(curr, *it1);
-                        curr = *it1;
+                    for (instruction* instr : m_compatible) {
+                        set_next(curr, instr);
+                        curr = instr;
                     }
                     set_next(curr, new_child_head1);
                     // set: new_child_head1:CHOOSE(new_child_head2) -> i1 -> i2 -> first_child_head
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index af761eecf..a052d1f98 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -508,13 +508,14 @@ namespace smt {
             mk_axiom(eqz, lower, !is_numeral);
             mk_axiom(eqz, upper, !is_numeral);
             rational k;
+            context& ctx = get_context();
+            (void)ctx;
             if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
                 k.is_pos() && k < rational(8)) {
                 rational j(0);
 #if 1
                 literal_buffer lits;
                 expr_ref mod_j(m);
-                context& ctx = get_context();
                 while(j < k) {
                     mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true));
                     ctx.internalize(mod_j, false);
@@ -542,6 +543,31 @@ namespace smt {
                 }
 #endif
             }
+            if (!m_util.is_numeral(divisor)) {
+                //
+                // forall x . (or (= y 0) (= (div (* x y) y) x))
+                // forall x . (=> (= y 0) (= (div (* x y) y) (div 0 0)))
+                // 
+                sort* intS = m_util.mk_int();
+                var_ref v(m.mk_var(0, intS), m);
+                app_ref mul(m_util.mk_mul(divisor, v), m);
+                app_ref div(m_util.mk_idiv(mul, divisor), m);
+                expr_ref divp1(m.mk_pattern(div), m);
+                app_ref mul2(m_util.mk_mul(v, divisor), m);
+                app_ref div2(m_util.mk_idiv(mul2, divisor), m);
+                expr_ref divp2(m.mk_pattern(div2), m);
+                expr_ref fml1(m.mk_or(m.mk_not(eqz), m.mk_eq(div, m_util.mk_idiv(zero, zero))), m);
+                expr_ref fml2(m.mk_or(eqz, m.mk_eq(div, v)), m);
+                symbol name("?x");
+                expr* pats[2] = { divp1, divp2 };
+                expr_ref fml(m);
+                fml = m.mk_forall(1, &intS, &name, fml1, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
+                proof_ref pr(m.mk_asserted(fml), m);
+                ctx.internalize_assertion(fml, pr, 0);
+                fml = m.mk_forall(1, &intS, &name, fml2, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
+                pr = m.mk_asserted(fml);
+                ctx.internalize_assertion(fml, pr, 0);
+            }
         }
     }