diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 90fd3fb22..2483d2370 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -336,7 +336,7 @@ bool operator<(const zstring& lhs, const zstring& rhs) {
 
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false),
-                                    m_stringc_sym("StringSequence"),
+                                    m_stringc_sym("String"),
                                     m_charc_sym("Char"),
                                     m_string(0),
                                     m_char(0),
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 3a4f7f981..78a295e27 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -825,7 +825,9 @@ namespace smt {
     }
 
     void setup::setup_seq() {
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        // TODO proper negotiation of theory_str vs. theory_seq
+        //m_context.register_plugin(alloc(theory_seq, m_manager));
+        setup_str();
     }
 
     void setup::setup_card() {
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 79b6efb8b..1f276125c 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -31,7 +31,7 @@ Revision History:
 namespace smt {
 
 theory_str::theory_str(ast_manager & m, theory_str_params const & params):
-        theory(m.mk_family_id("str")),
+        theory(m.mk_family_id("seq")),
         m_params(params),
         /* Options */
         opt_EagerStringConstantLengthAssertions(true),
@@ -266,7 +266,7 @@ void theory_str::refresh_theory_var(expr * e) {
 theory_var theory_str::mk_var(enode* n) {
     TRACE("t_str_detail", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
     ast_manager & m = get_manager();
-    if (!(is_sort_of(m.get_sort(n->get_owner()), u.get_family_id(), _STRING_SORT))) {
+    if (!(m.get_sort(n->get_owner()) == u.str.mk_string_sort())) {
         return null_theory_var;
     }
     if (is_attached_to_var(n)) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index fc238acbd..5a67f72f1 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -603,7 +603,7 @@ namespace smt {
         theory_str(ast_manager & m, theory_str_params const & params);
         virtual ~theory_str();
 
-        virtual char const * get_name() const { return "strings"; }
+        virtual char const * get_name() const { return "seq"; }
         virtual void display(std::ostream & out) const;
 
         bool overlapping_variables_detected() const { return loopDetected; }