diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 21af0773a..787648e19 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -256,7 +256,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const {
 
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false),
-                                    m_stringc_sym("String"),
+                                    m_stringc_sym("StringSequence"),
                                     m_charc_sym("Char"),
                                     m_string(0),
                                     m_char(0),
@@ -490,7 +490,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
     m_char = bv.mk_sort(8);
     m->inc_ref(m_char);
     parameter param(m_char);
-    m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
+    m_string = m->mk_sort(symbol("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, &param));
     m->inc_ref(m_string);
     parameter paramS(m_string);
     m_re = m->mk_sort(m_family_id, RE_SORT, 1, &paramS);
@@ -745,7 +745,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     init();
     sort_names.push_back(builtin_name("Seq",   SEQ_SORT));
     sort_names.push_back(builtin_name("RegEx", RE_SORT));
-    sort_names.push_back(builtin_name("String", _STRING_SORT));
+    sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
 }
 
 app* seq_decl_plugin::mk_string(symbol const& s) {
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 733689ac9..a547ab616 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"seq_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"ast_pp.h"
 #include"for_each_expr.h"
 
@@ -31,6 +32,7 @@ struct check_logic::imp {
     bv_util       m_bv_util;
     array_util    m_ar_util;
     seq_util      m_seq_util;
+    str_util      m_str_util;
     bool          m_uf;        // true if the logic supports uninterpreted functions
     bool          m_arrays;    // true if the logic supports arbitrary arrays
     bool          m_bv_arrays; // true if the logic supports only bv arrays
@@ -42,7 +44,7 @@ struct check_logic::imp {
     bool          m_quantifiers; // true if the logic supports quantifiers
     bool          m_unknown_logic;
 
-    imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m) {
+    imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_str_util(m) {
         reset();
     }
 
@@ -432,6 +434,9 @@ struct check_logic::imp {
         else if (fid == m_seq_util.get_family_id()) {
             // nothing to check
         }
+	else if (fid == m_str_util.get_family_id()) {
+       	    // nothing to check
+	}
         else {
             fail("logic does not support theory");
         }