diff --git a/.travis.yml b/.travis.yml
index a3ffb221e..9ec6132b6 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -84,7 +84,7 @@ matrix:
     - os: osx
       osx_image: xcode8.3
       # Note: Apple Clang does not support OpenMP
-      env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0
+      env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 DOTNET_BINDINGS=0
 script:
   # Use `travis_wait` when doing LTO builds because this configuration will
   # have long link times during which it will not show any output which
diff --git a/cmake/modules/FindDotNetToolchain.cmake b/cmake/modules/FindDotNetToolchain.cmake
index abc4ff21c..6e8cc7610 100644
--- a/cmake/modules/FindDotNetToolchain.cmake
+++ b/cmake/modules/FindDotNetToolchain.cmake
@@ -33,13 +33,18 @@ if (DOTNET_CSC_EXECUTABLE)
       set(DOTNET_TOOLCHAIN_IS_MONO TRUE)
       set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE)
       message(STATUS ".NET toolchain is Mono")
+    elseif ("${CSC_STD_OUT}" MATCHES "^Turbo[ ]+C#")
+      set(DOTNET_DETERMINED_VENDOR TRUE)
+      set(DOTNET_TOOLCHAIN_IS_MONO TRUE)
+      set(DOTNET_TOOLCHAIN_IS_WINDOWS FALSE)
+      message(STATUS ".NET toolchain is Mono")
     elseif ("${CSC_STD_OUT}" MATCHES "^Microsoft.+Visual[ ]+C#")
       set(DOTNET_DETERMINED_VENDOR TRUE)
       set(DOTNET_TOOLCHAIN_IS_MONO FALSE)
       set(DOTNET_TOOLCHAIN_IS_WINDOWS TRUE)
       message(STATUS ".NET toolchain is Windows native")
     else()
-      message(STATUS ".NET toolchain is unknown")
+      message(STATUS ".NET toolchain is unknown: ${CSC_STD_OUT}")
     endif()
   endif()
 endif()
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/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 688ded834..8af3af277 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -342,10 +342,16 @@ void proto_model::compress() {
    \brief Complete the interpretation fi of f if it is partial.
    If f does not have an interpretation in the given model, then this is a noop.
 */
-void proto_model::complete_partial_func(func_decl * f) {
+void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
     func_interp * fi = get_func_interp(f);
     if (fi && fi->is_partial()) {
-        expr * else_value = fi->get_max_occ_result();
+        expr * else_value;
+        if (use_fresh) {
+            else_value = get_fresh_value(f->get_range());
+        }
+        else {
+            else_value = fi->get_max_occ_result();
+        }
         if (else_value == nullptr)
             else_value = get_some_value(f->get_range());
         fi->set_else(else_value);
@@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) {
 /**
    \brief Set the (else) field of function interpretations...
 */
-void proto_model::complete_partial_funcs() {
+void proto_model::complete_partial_funcs(bool use_fresh) {
     if (m_model_partial)
         return;
 
     // m_func_decls may be "expanded" when we invoke get_some_value.
     // So, we must not use iterators to traverse it.
-    for (unsigned i = 0; i < m_func_decls.size(); i++) {
-        complete_partial_func(m_func_decls[i]);
+    for (unsigned i = 0; i < m_func_decls.size(); ++i) {
+        complete_partial_func(m_func_decls.get(i), use_fresh);
     }
 }
 
diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h
index d92d459e4..04e3a90fe 100644
--- a/src/smt/proto_model/proto_model.h
+++ b/src/smt/proto_model/proto_model.h
@@ -100,8 +100,8 @@ public:
     //
     // Complete partial function interps
     //
-    void complete_partial_func(func_decl * f);
-    void complete_partial_funcs();
+    void complete_partial_func(func_decl * f, bool use_fresh);
+    void complete_partial_funcs(bool use_fresh);
 
     //
     // Create final model object. 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b2adfff8d..48033f9b5 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4364,7 +4364,7 @@ namespace smt {
             m_proto_model = m_model_generator->mk_model();
             m_qmanager->adjust_model(m_proto_model.get());
             TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
-            m_proto_model->complete_partial_funcs();
+            m_proto_model->complete_partial_funcs(false);
             TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
             m_proto_model->cleanup();
             if (m_fparams.m_model_compact)
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 4307d3fdf..73f85faf6 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1028,7 +1028,7 @@ namespace smt {
             void complete_partial_funcs(func_decl_set const & partial_funcs) {
                 for (func_decl * f : partial_funcs) {
                     // Complete the current interpretation
-                    m_model->complete_partial_func(f);
+                    m_model->complete_partial_func(f, true);
 
                     unsigned arity   = f->get_arity();
                     func_interp * fi = m_model->get_func_interp(f);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index af761eecf..cbd41f08c 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,36 @@ namespace smt {
                 }
 #endif
             }
+#if 0
+            // e-matching is too restrictive for multiplication.
+            // also suffers from use-after free so formulas have to be pinned in solver.
+            // 
+            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);
+            }
+#endif
         }
     }
 
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 8cd01d2e9..75bcec13c 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -62,7 +62,7 @@ namespace smt {
             return true;
         }
 
-        expr * get_fresh_value(sort * s) override { NOT_IMPLEMENTED_YET(); }
+        expr * get_fresh_value(sort * s) override { return get_some_value(s); }
         void register_value(expr * n) override { /* Ignore */ }
 
         app * mk_value(mpf const & x) {