diff --git a/src/model/model.cpp b/src/model/model.cpp
index af30b6179..f7ca7ae9c 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -412,7 +412,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
                         domain.push_back(s);
                     }
                     new_t = fi->get_array_interp(domain);
-                    TRACE("model", tout << new_t << "\n";);
+                    TRACE("model", tout << "array interpretation:" << new_t << "\n";);
                 }
             }
 
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 74b9328e8..70199f2e6 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -900,6 +900,9 @@ namespace smt {
         else if (m_params.m_string_solver == "seq") {
             setup_seq();
         } 
+        else if (m_params.m_string_solver == "empty") {
+            m_context.register_plugin(alloc(smt::theory_seq_empty, m_manager, m_params));
+        }
         else if (m_params.m_string_solver == "auto") {
             if (st.m_has_seq_non_str) {
                 setup_seq();