diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index d45a4b092..24d69cc0e 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -638,9 +638,13 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     set_curr_sort(m().get_sort(arg1));
     numeral v1, v2;
     bool is_int;
-    if (m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
+    if (m_util.is_numeral(arg2, v2, is_int)) {
         SASSERT(!is_int);
-        if (m_util.is_numeral(arg1, v1, is_int)) {
+        if (v2.is_zero()) {
+            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);
             return BR_DONE;
         }
@@ -691,6 +695,10 @@ 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;
     }
+    if (m_util.is_numeral(arg2, v2, is_int) & v2.is_zero()) {
+        result = m_util.mk_idiv0(arg1);
+        return BR_REWRITE1;
+    }
     return BR_FAILED;
 }
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 583a8dad5..f4a890a2c 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -178,7 +178,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 return BR_DONE;
             }
         }
-        TRACE("model_evaluator", tout << f->get_name() << "\n";);
+        CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
         return st;
     }
 
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 88b0290d5..b5abd966a 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -309,13 +309,16 @@ namespace qe {
                 expr_ref_vector args(m);
                 sort* range = get_array_range(m.get_sort(s));
                 for (unsigned i = 0; i < idxs.size(); ++i) {
-                    app_ref var(m);
-                    var = m.mk_fresh_const("value", range);
-                    vars.push_back(var);
+                    //app_ref var(m);
+                    //var = m.mk_fresh_const("value", range);
+                    //vars.push_back(var);
+                    expr_ref val(m);
                     args.reset();
                     args.push_back(result);
                     args.append(idxs[i].m_values.size(), idxs[i].m_vars);
-                    args.push_back(var);
+                    result = a.mk_select(args.size(), args.c_ptr());
+                    VERIFY(model.eval(result, val));
+                    args.push_back(val);
                     result = a.mk_store(args.size(), args.c_ptr());
                 }
                 expr_safe_replace sub(m);