diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
index 9f7b1662f..87e82d121 100644
--- a/src/ast/rewriter/array_rewriter.cpp
+++ b/src/ast/rewriter/array_rewriter.cpp
@@ -247,6 +247,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         // select(as-array[f], I) --> f(I)
         func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
         result = m().mk_app(f, num_args - 1, args + 1);
+        TRACE("array", tout << mk_pp(args[0], m()) << " " << result << "\n";);
         return BR_REWRITE1;
     }
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 266598467..132af4204 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -164,7 +164,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;
-                return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
+                st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
+                TRACE("model_evaluator", tout << result << "\n";);
+                return st;
             }
             else if (m_model_completion) {
                 sort * s   = f->get_range();
@@ -255,6 +257,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 result = ev(result);
                 m_pinned.push_back(result);
                 m_def_cache.insert(g, result);
+                TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
                 return BR_DONE;
             }
         }
@@ -370,7 +373,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
     }
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
-        TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << "\n";);
+        TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " " 
+              << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
         if (a == b) {
             result = m.mk_true();
             return BR_DONE;
@@ -396,7 +400,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 conj.push_back(m.mk_eq(else1, else2));
             }
             if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
-                TRACE("model_evalator", tout << "argss are unique";);
+                TRACE("model_evaluator", tout << "args are unique " << conj << "\n";);
                 return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
             }
 
@@ -413,8 +417,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             }
             result = mk_and(conj);
             TRACE("model_evaluator", tout << mk_pp(a, m) << " == " << mk_pp(b, m) << " -> " << conj << "\n";
-                  for (auto& s : stores1) tout << "store: " << s << "\n";
-                  );
+                  for (auto& s : stores1) tout << "store: " << s << "\n"; );
             return BR_REWRITE_FULL;
         }
         return m_ar_rw.mk_eq_core(a, b, result);
@@ -454,6 +457,13 @@ struct evaluator_cfg : public default_rewriter_cfg {
         args_eq   ae(arity);
         args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
         args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
+        TRACE("model_evaluator",
+              tout << "arity " << arity << "\n";
+              for (auto& v : stores1) tout << "stores1: " << v << "\n";
+              for (auto& v : stores2) tout << "stores2: " << v << "\n";
+              tout << "else1: " << mk_pp(else1, m) << "\n";
+              tout << "else2: " << mk_pp(else2, m) << "\n";
+              tout << "conj: " << conj << "\n";);
 
         // stores with smaller index take precedence
         for (unsigned i = stores1.size(); i-- > 0; ) {
@@ -463,19 +473,23 @@ struct evaluator_cfg : public default_rewriter_cfg {
         for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
             if (table2.contains(stores2[i].c_ptr())) {
                 // first insertion takes precedence.
+                TRACE("model_evaluator", tout << "duplicate " << stores2[i] << "\n";);
                 continue;
             }
             table2.insert(stores2[i].c_ptr());
             expr * const* args = nullptr;
             expr* val = stores2[i][arity];
             if (table1.find(stores2[i].c_ptr(), args)) {
+                TRACE("model_evaluator", tout << "found value " << stores2[i] << "\n";);
+                table1.remove(args);
                 switch (compare(args[arity], val)) {
-                case l_true: table1.remove(args); break;
+                case l_true: break;
                 case l_false: result = m.mk_false(); return BR_DONE;
                 default: conj.push_back(m.mk_eq(val, args[arity])); break;
                 }
             }
             else {
+                TRACE("model_evaluator", tout << "not found value " << stores2[i] << "\n";);
                 switch (compare(else1, val)) {
                 case l_true: break;
                 case l_false: result = m.mk_false(); return BR_DONE;