diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 353fb975f..bf238d8c5 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -573,7 +573,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("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, &param));
+    m_string = m->mk_sort(symbol("String"), 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);