diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp
index 960218dff..1bc3ea8b8 100644
--- a/src/smt/theory_array.cpp
+++ b/src/smt/theory_array.cpp
@@ -85,27 +85,9 @@ namespace smt {
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
             register_sort(m.get_sort(n->get_owner()));
-        d->m_is_select = is_select(n);
-        
-        expr* e1, *e2, *e3;
+        d->m_is_select = is_select(n);        
         if (is_store(n))
             d->m_stores.push_back(n);
-        else if (m.is_ite(n->get_owner(), e1, e2, e3)) {
-            ptr_vector<expr> todo;
-            todo.push_back(e2);
-            todo.push_back(e3);
-            while (!todo.empty()) {
-                e1 = todo.back();
-                todo.pop_back();
-                if (is_app(e1) && is_store(to_app(e1))) {
-                    d->m_stores.push_back(ctx.get_enode(e1));
-                }
-                else if (m.is_ite(e1, e1, e2, e3)) {
-                    todo.push_back(e2);
-                    todo.push_back(e3);
-                }
-            }
-        }
         ctx.attach_th_var(n, this, r);
         if (m_params.m_array_laziness <= 1 && is_store(n))
             instantiate_axiom1(n);
diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h
index 9cc833d31..4e45f77f2 100644
--- a/src/smt/theory_array.h
+++ b/src/smt/theory_array.h
@@ -49,7 +49,7 @@ namespace smt {
             var_data():m_prop_upward(false), m_is_array(false), m_is_select(false) {}
         };
         ptr_vector<var_data>            m_var_data;
-        theory_array_params &           m_params;
+        theory_array_params&            m_params;
         theory_array_stats              m_stats;
         th_union_find                   m_find;
         th_trail_stack                  m_trail_stack;
@@ -98,7 +98,7 @@ namespace smt {
         theory_array(ast_manager & m, theory_array_params & params);
         virtual ~theory_array();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), new_ctx->get_fparams()); }
 
         virtual char const * get_name() const { return "array"; }