diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index 1634f8df4..8534ffd4a 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -28,6 +28,7 @@ static_features::static_features(ast_manager & m):
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
     m_lfid(m.mk_family_id("label")),
+    m_arrfid(m.mk_family_id("array")),
     m_label_sym("label"),
     m_pattern_sym("pattern"),
     m_expr_list_sym("expr-list") {
@@ -317,6 +318,16 @@ void static_features::update_core(expr * e) {
                 }
             }
         }
+        if (m_arrayutil.is_array(e)) {
+            TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";);
+            sort * ty = to_app(e)->get_decl()->get_range();
+            SASSERT(ty->get_num_parameters() == 2);
+            sort * inx_srt = to_sort(ty->get_parameter(0).get_ast());
+            sort * elm_srt = to_sort(ty->get_parameter(1).get_ast());
+            mark_theory(ty->get_family_id());
+            update_core(inx_srt);
+            update_core(elm_srt);
+        }
         func_decl * d = to_app(e)->get_decl();
         inc_num_apps(d);
         if (d->get_arity() > 0 && !is_marked(d)) {
@@ -351,6 +362,20 @@ void static_features::update_core(expr * e) {
     }
 }
 
+void static_features::update_core(sort * s) {
+    mark_theory(s->get_family_id());
+    if (!m_has_int && m_autil.is_int(s))
+        m_has_int = true;
+    if (!m_has_real && m_autil.is_real(s))
+        m_has_real = true;
+    if (!m_has_bv && m_bvutil.is_bv_sort(s))
+        m_has_bv = true;
+    if (!m_has_fpa && (m_fpautil.is_float(s) || m_fpautil.is_rm(s)))
+        m_has_fpa = true;
+    if (!m_has_arrays && m_arrayutil.is_array(s))
+        m_has_arrays = true;
+}
+
 void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) {
     TRACE("static_features", tout << "processing\n" << mk_pp(e, m_manager) << "\n";);
     if (is_var(e))
diff --git a/src/ast/static_features.h b/src/ast/static_features.h
index d27d026cf..4bdcd6f05 100644
--- a/src/ast/static_features.h
+++ b/src/ast/static_features.h
@@ -35,6 +35,7 @@ struct static_features {
     family_id                m_bfid;
     family_id                m_afid;
     family_id                m_lfid;    
+    family_id                m_arrfid;
     ast_mark                 m_already_visited;
     bool                     m_cnf;
     unsigned                 m_num_exprs;             // 
@@ -148,6 +149,7 @@ struct static_features {
     void inc_theory_eqs(family_id fid) { m_num_theory_eqs.reserve(fid+1, 0); m_num_theory_eqs[fid]++; }
     void inc_num_aliens(family_id fid) { m_num_aliens_per_family.reserve(fid+1, 0); m_num_aliens_per_family[fid]++; }
     void update_core(expr * e);
+    void update_core(sort * s);
     void process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth);
     void process_root(expr * e);
     unsigned get_depth(expr const * e) const { return m_expr2depth.get(e->get_id(), 1); }
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 96f6122cb..e6d21a1e2 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -830,7 +830,10 @@ namespace smt {
               tout << "is_arith: " << is_arith(st) << "\n";
               tout << "has UF: " << st.has_uf() << "\n";
               tout << "has real: " << st.m_has_real << "\n";
-              tout << "has int: " << st.m_has_int << "\n";);
+              tout << "has int: " << st.m_has_int << "\n";
+              tout << "has bv: " << st.m_has_bv << "\n";
+              tout << "has fpa: " << st.m_has_fpa << "\n"; 
+              tout << "has arrays: " << st.m_has_arrays << "\n";);
 
         if (st.num_non_uf_theories() == 0) {
             setup_QF_UF(st);