diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index 9f52ea9a5..c8a1adcbe 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -81,6 +81,7 @@ void static_features::reset() {
     m_has_str                              = false;
     m_has_seq_non_str                      = false;
     m_has_arrays                           = false;
+    m_has_ext_arrays                       = false;
     m_arith_k_sum                          .reset();
     m_num_arith_terms                      = 0;
     m_num_arith_eqs                        = 0;
@@ -271,8 +272,11 @@ void static_features::update_core(expr * e) {
         m_has_bv = true;
     if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
         m_has_fpa = true;
-    if (!m_has_arrays && m_arrayutil.is_array(e))
+    if (!m_has_arrays && m_arrayutil.is_array(e)) 
         m_has_arrays = true;
+    if (!m_has_ext_arrays && m_arrayutil.is_array(e) && 
+        !m_arrayutil.is_select(e) && !m_arrayutil.is_store(e)) 
+        m_has_ext_arrays = true;
     if (!m_has_str && m_sequtil.str.is_string_term(e))
         m_has_str = true;
     if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
diff --git a/src/ast/static_features.h b/src/ast/static_features.h
index 5473ba0ff..197947026 100644
--- a/src/ast/static_features.h
+++ b/src/ast/static_features.h
@@ -82,6 +82,7 @@ struct static_features {
     bool                     m_has_str;         // has String-typed terms
     bool                     m_has_seq_non_str; // has non-String-typed Sequence terms
     bool                     m_has_arrays;      //
+    bool                     m_has_ext_arrays;  // does this use extended array theory.
     rational                 m_arith_k_sum;     // sum of the numerals in arith atoms.
     unsigned                 m_num_arith_terms;
     unsigned                 m_num_arith_eqs;   // equalities of the form t = k where k is a numeral
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 83b15fd90..55ea55663 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -576,17 +576,18 @@ namespace smt {
         m_params.m_nnf_cnf             = false;
         m_params.m_propagate_booleans  = true;
         m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params));
-        m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
+        setup_arrays();
     }
 
     void setup::setup_QF_AX() {
+        TRACE("setup", tout << "QF_AX\n";);
         m_params.m_array_mode          = AR_SIMPLE;
         m_params.m_nnf_cnf             = false;
-        m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
+        setup_arrays();
     }
 
     void setup::setup_QF_AX(static_features const & st) {
-        m_params.m_array_mode          = AR_SIMPLE;
+        m_params.m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
         m_params.m_nnf_cnf             = false;
         if (st.m_num_clauses == st.m_num_units) {
             m_params.m_relevancy_lvl       = 0;
@@ -595,7 +596,7 @@ namespace smt {
         else {
             m_params.m_relevancy_lvl       = 2;
         }
-        m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
+        setup_arrays();
     }
 
     void setup::setup_QF_AUFLIA() {
@@ -607,11 +608,11 @@ namespace smt {
         m_params.m_restart_factor      = 1.5;
         m_params.m_phase_selection     = PS_CACHING_CONSERVATIVE2;
         setup_i_arith();
-        m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
+        setup_arrays();
     }
 
     void setup::setup_QF_AUFLIA(static_features const & st) {
-        m_params.m_array_mode          = AR_SIMPLE;
+        m_params.m_array_mode          = st.m_has_ext_arrays ? AR_FULL : AR_SIMPLE;
         if (st.m_has_real)
             throw default_exception("Benchmark has real variables but it is marked as QF_AUFLIA (arrays, uninterpreted functions and linear integer arithmetic).");
         m_params.m_nnf_cnf             = false;
@@ -631,7 +632,7 @@ namespace smt {
         //    m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params));
         // else 
         setup_i_arith();
-        m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params));
+        setup_arrays();
     }
 
     void setup::setup_AUFLIA(bool simple_array) {
@@ -992,17 +993,17 @@ namespace smt {
         }
 
         if (st.num_theories() == 1 && st.m_has_arrays) {
-            setup_QF_AX();
+            setup_QF_AX(st);
             return;
         }
 
-        if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_bv) {
+        if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && !st.m_has_ext_arrays && st.m_has_bv) {
             setup_QF_AUFBV();
             return;
         }
 
         if (st.num_theories() == 2 && st.has_uf() && st.m_has_arrays && st.m_has_int) {
-            setup_QF_AUFLIA();
+            setup_QF_AUFLIA(st);
             return;
         }