diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index b8d5fe7b5..92ff1de90 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -41,7 +41,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_max_conflicts = p.max_conflicts();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
-    m_string_solver = _p.get_sym("string_solver", m_string_solver);
+    m_string_solver = p.string_solver();
     model_params mp(_p);
     m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index dd94d9473..4d02218bf 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -832,7 +832,6 @@ 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();
@@ -969,15 +968,6 @@ namespace smt {
             return;
         }
 
-        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();
     }