diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 6aca2f5b4..bf6b09332 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -118,6 +118,14 @@ namespace smt {
                 }
             }
 
+            scoped_trace_stream(theory& th, literal lit): m(th.get_manager()) {
+                if (m.has_trace_stream()) {
+                    literal_vector lits;
+                    lits.push_back(lit);
+                    th.log_axiom_instantiation(lits);
+                }
+            }
+
             scoped_trace_stream(theory& th, std::function<literal(void)>& fn): m(th.get_manager()) {
                 if (m.has_trace_stream()) {
                     literal_vector ls;
diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h
index 95e2d2125..6af1d1f4d 100644
--- a/src/smt/theory_array_base.h
+++ b/src/smt/theory_array_base.h
@@ -62,6 +62,7 @@ namespace smt {
         bool is_select_arg(enode* r);
 
         app * mk_select(unsigned num_args, expr * const * args);
+        app * mk_select(expr_ref_vector const& args) { return mk_select(args.size(), args.c_ptr()); }
         app * mk_store(unsigned num_args, expr * const * args);
         app * mk_default(expr* a);
 
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 8679c4dd9..bfcc40717 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -29,7 +29,8 @@ namespace smt {
 
     theory_array_full::theory_array_full(context& ctx) : 
         theory_array(ctx),
-        m_sort2epsilon(ctx.get_manager()) {}
+        m_sort2epsilon0(ctx.get_manager()),
+        m_sort2epsilon1(ctx.get_manager()) {}
 
     theory_array_full::~theory_array_full() {
         std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
@@ -203,7 +204,6 @@ namespace smt {
         std::for_each(m_var_data_full.begin(), m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.reset();
         m_eqs.reset();
-        m_eqsv.reset();
     }
 
     void theory_array_full::display_var(std::ostream & out, theory_var v) const {
@@ -577,6 +577,23 @@ namespace smt {
 #endif
     }
 
+    bool theory_array_full::has_unitary_domain(app* array_term) {
+        SASSERT(is_array_sort(array_term));
+        sort* s = m.get_sort(array_term);
+        unsigned dim = get_dimension(s);
+        parameter const *  params = s->get_info()->get_parameters();
+        for (unsigned i = 0; i < dim; ++i) {
+            SASSERT(params[i].is_ast());
+            sort* d = to_sort(params[i].get_ast());
+            if (d->is_infinite() || d->is_very_big()) {
+                return false;
+            }
+            if (1 != d->get_num_elements().size())
+                                return false;
+        }
+        return true;        
+    }
+
     bool theory_array_full::has_large_domain(app* array_term) {
         SASSERT(is_array_sort(array_term));
         sort* s = m.get_sort(array_term);
@@ -590,7 +607,7 @@ namespace smt {
                 return true;
             }
             sz *= rational(d->get_num_elements().size(),rational::ui64());
-            if (sz >= rational(1 << 20)) {
+            if (sz >= rational(1 << 14)) {
                 return true;
             }
         }
@@ -677,50 +694,56 @@ namespace smt {
 
         m_stats.m_num_default_store_axiom++;
 
-        app* def1;
-        app* def2;
+        app_ref def1(m), def2(m);
 
         TRACE("array", tout << mk_bounded_pp(store_app, m) << "\n";);
 
-        if (has_large_domain(store_app)) {
-            def2 = mk_default(store_app->get_arg(0));
-        }
-        else {
+        def2 = mk_default(store_app->get_arg(0));
+        bool is_new = false;
+        if (!has_large_domain(store_app) && !has_unitary_domain(store_app)) {
             //
             // let A = store(B, i, v)
             // 
             // Add:
-            //   default(A) = ite(epsilon = i, v, default(B))
+            //   default(A) = ite(epsilon1 = i, v, default(B))
+            //   A[epsilon2] = B[epsilon2]
             // 
-            expr_ref_vector eqs(m);
+            expr_ref_vector eqs(m), args1(m), args2(m);
+            args1.push_back(store_app->get_arg(0));
+            args2.push_back(store_app);
             unsigned num_args = store_app->get_num_args();
             for (unsigned i = 1; i + 1 < num_args; ++i) {
                 sort* srt = m.get_sort(store_app->get_arg(i));
-                app* ep = mk_epsilon(srt);
-                eqs.push_back(m.mk_eq(ep, store_app->get_arg(i)));
+                auto ep = mk_epsilon(srt);
+                eqs.push_back(m.mk_eq(ep.first, store_app->get_arg(i)));
+                args1.push_back(ep.second);
+                args2.push_back(ep.second);
             }
             
-            expr_ref eq(m);
-            eq = mk_and(eqs);
-            expr* defA = mk_default(store_app->get_arg(0));
-            def2 = m.mk_ite(eq, store_app->get_arg(num_args-1), defA); 
+            expr_ref eq(mk_and(eqs), m);
+            def2 = m.mk_ite(eq, store_app->get_arg(num_args-1), def2); 
+            
+            app_ref sel1(m), sel2(m);
+            sel1 = mk_select(args1);
+            sel2 = mk_select(args2);
+            is_new = try_assign_eq(sel1, sel2);
         }
 
         def1 = mk_default(store_app);
         ctx.internalize(def1, false);
         ctx.internalize(def2, false);
-        return try_assign_eq(def1, def2);
+        return try_assign_eq(def1, def2) || is_new;
     }
 
-    app* theory_array_full::mk_epsilon(sort* s) {
-        app* eps = nullptr;
-        if (m_sort2epsilon.find(s, eps)) {
-            return eps;
-        }
-        eps = m.mk_fresh_const("epsilon", s);
-        m_trail_stack.push(
-            ast2ast_trail<theory_array, sort, app>(m_sort2epsilon, s, eps));   
-        return eps;
+    std::pair<app*,app*> theory_array_full::mk_epsilon(sort* s) {
+        app* eps0 = nullptr, *eps1 = nullptr;
+        if (!m_sort2epsilon0.find(s, eps0) || !m_sort2epsilon1.find(s, eps1)) {
+            eps0 = m.mk_fresh_const("epsilon", s);
+            eps1 = m.mk_fresh_const("epsilon", s);
+            m_trail_stack.push(ast2ast_trail<theory_array, sort, app>(m_sort2epsilon0, s, eps0));   
+            m_trail_stack.push(ast2ast_trail<theory_array, sort, app>(m_sort2epsilon1, s, eps1));  
+        } 
+        return std::make_pair(eps0, eps1);
     }
 
     final_check_status theory_array_full::assert_delayed_axioms() {        
@@ -741,13 +764,6 @@ namespace smt {
                 }
             }
         }
-        while (!m_eqsv.empty()) {
-            literal eq = m_eqsv.back();
-            m_eqsv.pop_back();
-            ctx.mark_as_relevant(eq);            
-            assert_axiom(eq);
-            r = FC_CONTINUE;
-        }
         if (r == FC_DONE && m_bapa) {
             r = m_bapa->final_check();
         }
@@ -775,9 +791,7 @@ namespace smt {
     }
 
     bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
-        TRACE("array", 
-              tout << mk_bounded_pp(v1, m) << "\n==\n" 
-              << mk_bounded_pp(v2, m) << "\n";);
+        TRACE("array", tout << mk_bounded_pp(v1, m) << "\n==\n" << mk_bounded_pp(v2, m) << "\n";);
         
         if (m_eqs.contains(v1, v2)) {
             return false;
@@ -785,12 +799,9 @@ namespace smt {
         else {
             m_eqs.insert(v1, v2, true);
             literal eq(mk_eq(v1, v2, true));
-            if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(eq.var()));
+            scoped_trace_stream _sc(*this, eq);
             ctx.mark_as_relevant(eq);            
             assert_axiom(eq);
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-
-            // m_eqsv.push_back(eq);
             return true;
         }
     }
@@ -801,7 +812,6 @@ namespace smt {
         std::for_each(m_var_data_full.begin() + num_old_vars, m_var_data_full.end(), delete_proc<var_data_full>());
         m_var_data_full.shrink(num_old_vars);        
         m_eqs.reset();
-        m_eqsv.reset();
     }
 
     void theory_array_full::collect_statistics(::statistics & st) const {
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 559cf6fed..56e46e352 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -34,9 +34,8 @@ namespace smt {
 
         ptr_vector<var_data_full> m_var_data_full;
 
-        ast2ast_trailmap<sort,app> m_sort2epsilon;
-        obj_pair_map<expr,expr,bool> m_eqs;
-        svector<literal>             m_eqsv;
+        ast2ast_trailmap<sort, app> m_sort2epsilon0, m_sort2epsilon1;
+        obj_pair_map<expr, expr, bool> m_eqs;
         
         static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
         static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
@@ -80,7 +79,8 @@ namespace smt {
         bool instantiate_parent_stores_default(theory_var v);
 
         bool has_large_domain(app* array_term);
-        app* mk_epsilon(sort* s);
+        bool has_unitary_domain(app* array_term);
+        std::pair<app*,app*> mk_epsilon(sort* s);
 
         bool instantiate_select_const_axiom(enode* select, enode* cnst);
         bool instantiate_select_as_array_axiom(enode* select, enode* arr);