diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 030b244e5..52abb2c45 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -278,6 +278,17 @@ public:
             return is_sort_of(s, m_fid, _STRING_SORT);
         }
 
+        bool is_non_string_sequence(expr const * n) const {
+            if (is_string_term(n))
+                return false;
+
+            sort * s = get_sort(n);
+            if (u.is_seq(s) && !u.is_string(s)) {
+                return true;
+            }
+            return false;
+        }
+
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);
         MATCH_TERNARY(is_extract);
diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp
index 9958b3d50..daf20e095 100644
--- a/src/ast/static_features.cpp
+++ b/src/ast/static_features.cpp
@@ -284,8 +284,9 @@ void static_features::update_core(expr * e) {
         m_has_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.is_seq(e))
+    if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
         m_has_seq_non_str = true;
+    }
     if (is_app(e)) {
         family_id fid = to_app(e)->get_family_id();
         mark_theory(fid);
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index c295801ad..dd94d9473 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -832,6 +832,7 @@ namespace smt {
             m_context.register_plugin(alloc(theory_seq, m_manager));
         } else if (m_params.m_string_solver == "auto") {
             if (st.m_has_seq_non_str) {
+                NOT_IMPLEMENTED_YET();
                 m_context.register_plugin(alloc(theory_seq, m_manager));
             } else {
                 setup_str();
@@ -856,13 +857,15 @@ namespace smt {
     }
 
     void setup::setup_unknown() {
+        static_features st(m_manager);
+        st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
+
         setup_arith();
         setup_arrays();
         setup_bv();
         setup_datatypes();
         setup_dl();
-        // setup_seq()
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        setup_seq(st);
         setup_card();
         setup_fpa();
     }
@@ -966,7 +969,14 @@ namespace smt {
             return;
         }
 
-        // TODO setup_str() by features
+        if (st.num_theories() == 2 && st.m_has_str && !st.m_has_seq_non_str) {
+            setup_QF_S();
+            return;
+        }
+
+        if (st.num_theories() == 2 && st.m_has_seq_non_str) {
+            m_context.register_plugin(alloc(theory_seq, m_manager));
+        }
 
         setup_unknown();
     }