diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp
index 9c7bfd88a..85a478f85 100644
--- a/src/ast/sls/sls_array_plugin.cpp
+++ b/src/ast/sls/sls_array_plugin.cpp
@@ -394,11 +394,16 @@ namespace sls {
         // TODO: adapt to handle "const" arrays and multi-dimensional arrays.
         auto& kv = *m_kv;
         auto n = m_g->find(e)->get_root();
-        expr_ref r(n->get_expr(), m);
+        expr_ref r(n->get_expr(), m), key(m);
+        expr_mark visited;        
         for (auto [k, v] : kv[n]) {
             ptr_vector<expr> args;
+            key = ctx.get_value(k.sel->get_arg(1)->get_expr());
+            if (visited.is_marked(key))
+                continue;
+            visited.mark(key);
             args.push_back(r);
-            args.push_back(k.sel->get_arg(1)->get_expr());
+            args.push_back(key);
             args.push_back(v->get_expr());
             r = a.mk_store(args);
         }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 069acc4d9..664440557 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -89,7 +89,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_fpau(m),
         m_dt(m),
         m_pinned(m) {
-        bool flat = true;
+        bool flat = false;
         m_b_rw.set_flat_and_or(flat);
         m_a_rw.set_flat(flat);
         m_bv_rw.set_flat(flat);