diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 62a6a586e..523d98a93 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -365,7 +365,7 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
 
 format * smt2_pp_environment::pp_string_literal(app * t) {
     std::string s;
-    VERIFY (get_sutil().str.is_const(t, s));
+    VERIFY (get_sutil().str.is_string(t, s));
     std::ostringstream buffer;
     buffer << "\"";
     for (unsigned i = 0; i < s.length(); ++i) {
@@ -424,10 +424,10 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         fs.push_back(mk_unsigned(m, sbits));
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), "_");
     }
-    if (get_sutil().is_seq(s) && !get_sutil().is_string(s)) {
+    if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) {
         ptr_buffer<format> fs;
         fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
-        return mk_seq1(m, fs.begin(), fs.end(), f2f(), "Seq");
+        return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
     }
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); 
 }
@@ -600,7 +600,7 @@ class smt2_printer {
         if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
             f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
         }
-        else if (m_env.get_sutil().str.is_const(c)) {
+        else if (m_env.get_sutil().str.is_string(c)) {
             f = m_env.pp_string_literal(c);
         }
         else if (m_env.get_bvutil().is_numeral(c)) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 00b94e60d..fd370e425 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -29,12 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_PREFIX_OF:
-    case OP_SEQ_SUFFIX_OF:
-    case OP_SEQ_SUBSEQ_OF:
-    case OP_SEQ_EXTRACT:
-    case OP_SEQ_NTH:
-    case OP_SEQ_LENGTH:
 
     case OP_RE_PLUS:
     case OP_RE_STAR:
@@ -47,52 +41,60 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_EMPTY_SET:
     case OP_RE_FULL_SET:
     case OP_RE_EMPTY_SEQ:
-    case OP_RE_OF_SEQ:
     case OP_RE_OF_PRED:
-    case OP_RE_MEMBER:
         return BR_FAILED;
 
     // string specific operators.
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_SEQ_CONCAT: 
-    case _OP_STRING_CONCAT:
         SASSERT(num_args == 2);
         return mk_seq_concat(args[0], args[1], result);
-    case OP_STRING_LENGTH:
+    case OP_SEQ_LENGTH:
         SASSERT(num_args == 1);
         return mk_str_length(args[0], result);
-    case OP_STRING_SUBSTR: 
+    case OP_SEQ_EXTRACT:
         SASSERT(num_args == 3);
         return mk_str_substr(args[0], args[1], args[2], result);
-    case OP_STRING_STRCTN: 
+    case OP_SEQ_CONTAINS: 
         SASSERT(num_args == 2);
         return mk_str_strctn(args[0], args[1], result);
-    case OP_STRING_CHARAT:
+    case OP_SEQ_AT:
         SASSERT(num_args == 2);
-        return mk_str_charat(args[0], args[1], result); 
+        return mk_str_at(args[0], args[1], result); 
     case OP_STRING_STRIDOF: 
         SASSERT(num_args == 3);
         return mk_str_stridof(args[0], args[1], args[2], result);
     case OP_STRING_STRREPL: 
         SASSERT(num_args == 3);
         return mk_str_strrepl(args[0], args[1], args[2], result);
-    case OP_STRING_PREFIX: 
+    case OP_SEQ_PREFIX: 
         SASSERT(num_args == 2);
-        return mk_str_prefix(args[0], args[1], result);
-    case OP_STRING_SUFFIX: 
+        return mk_seq_prefix(args[0], args[1], result);
+    case OP_SEQ_SUFFIX: 
         SASSERT(num_args == 2);
-        return mk_str_suffix(args[0], args[1], result);
+        return mk_seq_suffix(args[0], args[1], result);
     case OP_STRING_ITOS: 
         SASSERT(num_args == 1);
         return mk_str_itos(args[0], result);
     case OP_STRING_STOI: 
         SASSERT(num_args == 1);
         return mk_str_stoi(args[0], result);
-    case OP_STRING_IN_REGEXP: 
-    case OP_STRING_TO_REGEXP: 
+    case OP_SEQ_TO_RE:
+    case OP_SEQ_IN_RE:
     case OP_REGEXP_LOOP: 
         return BR_FAILED;
+    case _OP_STRING_CONCAT:
+    case _OP_STRING_PREFIX:
+    case _OP_STRING_SUFFIX:
+    case _OP_STRING_STRCTN:
+    case _OP_STRING_LENGTH:
+    case _OP_STRING_CHARAT:
+    case _OP_STRING_IN_REGEXP: 
+    case _OP_STRING_TO_REGEXP: 
+    case _OP_STRING_SUBSTR: 
+
+        UNREACHABLE();
     }
     return BR_FAILED;
 }
@@ -107,8 +109,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
     expr* c, *d;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         result = m_util.str.mk_string(s1 + s2);
         return BR_DONE;
@@ -117,16 +119,16 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
         result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
         return BR_REWRITE2;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = b;
         return BR_DONE;
     }
-    if (isc2 && s2.length() == 0) {
+    if (m_util.str.is_empty(b)) {
         result = a;
         return BR_DONE;
     }
     if (m_util.str.is_concat(a, c, d) && 
-        m_util.str.is_const(d, s1) && isc2) {
+        m_util.str.is_string(d, s1) && isc2) {
         result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
         return BR_DONE;
     }
@@ -140,7 +142,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     unsigned len = 0;
     size_t j = 0;
     for (unsigned i = 0; i < m_es.size(); ++i) {
-        if (m_util.str.is_const(m_es[i], b)) {
+        if (m_util.str.is_string(m_es[i], b)) {
             len += b.length();
         }
         else {
@@ -169,7 +171,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
 br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s;
     rational pos, len;
-    if (m_util.str.is_const(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
+    if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
         pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
         unsigned _pos = pos.get_unsigned();
         unsigned _len = len.get_unsigned();
@@ -180,17 +182,17 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
 }
 br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
     std::string c, d;
-    if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
+    if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
         result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
         return BR_DONE;
     }
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) {
     std::string c;
     rational r;
-    if (m_util.str.is_const(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
+    if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
         unsigned j = r.get_unsigned();
         if (j < c.length()) {
             char ch = c[j];
@@ -206,8 +208,8 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
 br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2;
     rational r;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
 
     if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
         for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
@@ -224,7 +226,7 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_DONE;
     }
     
-    if (isc2 && s2.length() == 0) {
+    if (m_util.str.is_empty(b)) {
         result = c;
         return BR_DONE;
     }
@@ -234,8 +236,8 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
 
 br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2, s3;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && 
-        m_util.str.is_const(c, s3)) {
+    if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && 
+        m_util.str.is_string(c, s3)) {
         std::ostringstream buffer;
         for (size_t i = 0; i < s1.length(); ) {
             if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
@@ -257,10 +259,10 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         bool prefix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && prefix; ++i) {
@@ -269,17 +271,17 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(prefix);
         return BR_DONE;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = m().mk_true();
         return BR_DONE;
     }
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    bool isc1 = m_util.str.is_const(a, s1);
-    if (isc1 && m_util.str.is_const(b, s2)) {
+    bool isc1 = m_util.str.is_string(a, s1);
+    if (isc1 && m_util.str.is_string(b, s2)) {
         bool suffix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && suffix; ++i) {
             suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
@@ -287,7 +289,7 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(suffix);
         return BR_DONE;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = m().mk_true();
         return BR_DONE;
     }
@@ -304,7 +306,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
 }
 br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     std::string s;
-    if (m_util.str.is_const(a, s)) {
+    if (m_util.str.is_string(a, s)) {
         for (unsigned i = 0; i < s.length(); ++i) {
             if (s[i] == '-') { if (i != 0) return BR_FAILED; }
             else if ('0' <= s[i] && s[i] <= '9') continue;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 2d2909018..4674a7535 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -38,11 +38,11 @@ class seq_rewriter {
     br_status mk_str_length(expr* a, expr_ref& result);
     br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
-    br_status mk_str_charat(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_at(expr* a, expr* b, expr_ref& result);
     br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
-    br_status mk_str_prefix(expr* a, expr* b, expr_ref& result);
-    br_status mk_str_suffix(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);
     br_status mk_str_itos(expr* a, expr_ref& result);
     br_status mk_str_stoi(expr* a, expr_ref& result);
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 5fd8c0df7..b47c4209d 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -161,7 +161,6 @@ void seq_decl_plugin::init() {
     ast_manager& m = *m_manager;
     m_init = true;
     sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
-    sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1));
     sort* strT = m_string;
     parameter paramA(A);
     parameter paramS(strT);
@@ -174,27 +173,27 @@ void seq_decl_plugin::init() {
     sort* u16T = 0;
     sort* u32T = 0;
     sort* seqAseqA[2] = { seqA, seqA };
-    sort* seqAB[2] = { seqA, B };
     sort* seqAreA[2] = { seqA, reA };
     sort* reAreA[2] = { reA, reA };
     sort* AA[2] = { A, A };
-    sort* seqABB[3] = { seqA, B, B };
+    sort* seqAint2T[3] = { seqA, intT, intT };
     sort* str2T[2] = { strT, strT };
     sort* str3T[3] = { strT, strT, strT };
     sort* strTint2T[3] = { strT, intT, intT };
     sort* re2T[2] = { reT, reT };
     sort* strTreT[2] = { strT, reT };
     sort* str2TintT[3] = { strT, strT, intT };
+    sort* seqAintT[2] = { seqA, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",   1, 1, &A, seqA);
     m_sigs[OP_SEQ_EMPTY]     = alloc(psig, m, "seq.empty",  1, 0, 0, seqA); 
     m_sigs[OP_SEQ_CONCAT]    = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA);
-    m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_SUBSEQ_OF] = alloc(psig, m, "seq-subseq-of", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq-extract", 2, 3, seqABB, seqA);
-    m_sigs[OP_SEQ_NTH]       = alloc(psig, m, "seq-nth", 2, 2, seqAB, A);
+    m_sigs[OP_SEQ_PREFIX]    = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_SUFFIX]    = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_CONTAINS]  = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA);
+    m_sigs[OP_SEQ_AT]        = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
     m_sigs[OP_SEQ_LENGTH]    = alloc(psig, m, "seq-length", 1, 1, &seqA, intT);
     m_sigs[OP_RE_PLUS]       = alloc(psig, m, "re.+",    1, 1, &reA, reA);
     m_sigs[OP_RE_STAR]       = alloc(psig, m, "re.*",    1, 1, &reA, reA);
@@ -207,29 +206,29 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_EMPTY_SEQ]      = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
     m_sigs[OP_RE_FULL_SET]       = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
-    m_sigs[OP_RE_OF_SEQ]         = alloc(psig, m, "re-of-seq",  1, 1, &seqA, reA);
+    m_sigs[OP_SEQ_TO_RE]         = alloc(psig, m, "seq.to.re",  1, 1, &seqA, reA);
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
-    m_sigs[OP_RE_MEMBER]         = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
+    m_sigs[OP_SEQ_IN_RE]         = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
     m_sigs[OP_STRING_CONST]      = 0;
-    m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
-    m_sigs[OP_STRING_LENGTH]     = alloc(psig, m, "str.len", 0, 1, &strT, intT);
-    m_sigs[OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
-    m_sigs[OP_STRING_STRCTN]     = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
-    m_sigs[OP_STRING_CHARAT]     = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
     m_sigs[OP_STRING_STRIDOF]    = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[OP_STRING_STRREPL]    = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
-    m_sigs[OP_STRING_PREFIX]     = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
-    m_sigs[OP_STRING_SUFFIX]     = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
-    m_sigs[OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
-    m_sigs[OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
     m_sigs[OP_REGEXP_LOOP]       = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
+    m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
+    m_sigs[_OP_STRING_LENGTH]    = alloc(psig, m, "str.len", 0, 1, &strT, intT);
+    m_sigs[_OP_STRING_STRCTN]    = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_CHARAT]    = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
+    m_sigs[_OP_STRING_PREFIX]    = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_SUFFIX]    = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
+    m_sigs[_OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
+    m_sigs[_OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
     decl_plugin::set_manager(m, id);
-    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, CHAR_SORT, 0, (parameter const*)0));
+    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0));
     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));
@@ -259,9 +258,9 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
             m.raise_exception("invalid regex sort, parameter is not a sort");
         }
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
-    case STRING_SORT:
+    case _STRING_SORT:
         return m_string;
-    case CHAR_SORT:
+    case _CHAR_SORT:
         return m_char;
     default:
         UNREACHABLE();
@@ -269,6 +268,21 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
     }
 }
 
+func_decl* seq_decl_plugin::mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string) {
+    ast_manager& m = *m_manager;
+    sort_ref rng(m);
+    match(*m_sigs[k], arity, domain, range, rng);
+    return m.mk_func_decl(m_sigs[(domain[0] == m_string)?k_string:k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+}
+
+
+func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq) {
+    ast_manager& m = *m_manager;
+    sort_ref rng(m);
+    match(*m_sigs[k], arity, domain, range, rng);
+    return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k_seq));
+}
+
 func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned arity, sort * const * domain, sort * range) {
     init();
@@ -277,10 +291,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     switch(k) {
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_PREFIX_OF:
-    case OP_SEQ_SUFFIX_OF:
-    case OP_SEQ_SUBSEQ_OF:
-    case OP_SEQ_LENGTH:
+        
     case OP_RE_PLUS:
     case OP_RE_STAR:
     case OP_RE_OPTION:
@@ -288,14 +299,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_UNION:
     case OP_RE_EMPTY_SEQ:
     case OP_RE_EMPTY_SET:
-    case OP_RE_OF_SEQ:   
+
     case OP_RE_OF_PRED:
-    case OP_RE_MEMBER:
-        match(*m_sigs[k], arity, domain, range, rng);
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
-    case OP_SEQ_EXTRACT:
-    case OP_SEQ_NTH:
-        // TBD check numeric arguments for being BVs or integers.
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
     case OP_RE_LOOP:
@@ -312,14 +317,10 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
         
     case OP_SEQ_CONCAT: {
-        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
-        
+        match_left_assoc(*m_sigs[k], arity, domain, range, rng);        
         func_decl_info info(m_family_id, k);
         info.set_left_associative();
-        if (rng == m_string) {
-            return m.mk_func_decl(m_sigs[_OP_STRING_CONCAT]->m_name, rng, rng, rng, info);
-        }
-        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
+        return m.mk_func_decl(m_sigs[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info);
     } 
     case OP_RE_CONCAT:  {
         match_left_assoc(*m_sigs[k], arity, domain, range, rng);
@@ -333,19 +334,50 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         info.set_left_associative();
         return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
     }
+    case OP_SEQ_PREFIX:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX);
+    case _OP_STRING_PREFIX:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_PREFIX);
+
+    case OP_SEQ_SUFFIX:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_SUFFIX);
+    case _OP_STRING_SUFFIX:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_SUFFIX);
+
+    case OP_SEQ_LENGTH:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_LENGTH);
+    case _OP_STRING_LENGTH:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_LENGTH);
+
+    case OP_SEQ_CONTAINS:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRCTN);
+    case _OP_STRING_STRCTN:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_CONTAINS);
+
+    case OP_SEQ_TO_RE:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_TO_REGEXP);
+    case _OP_STRING_TO_REGEXP:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE);
+
+    case OP_SEQ_IN_RE:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_IN_REGEXP);
+    case _OP_STRING_IN_REGEXP:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_IN_RE);
+
+    case OP_SEQ_AT:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_CHARAT);
+    case _OP_STRING_CHARAT:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_AT);
+
+    case OP_SEQ_EXTRACT:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_SUBSTR);
+    case _OP_STRING_SUBSTR:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT);
 
-    case OP_STRING_LENGTH:
-    case OP_STRING_SUBSTR:
-    case OP_STRING_STRCTN:
-    case OP_STRING_CHARAT:
     case OP_STRING_STRIDOF:
     case OP_STRING_STRREPL:
-    case OP_STRING_PREFIX:
-    case OP_STRING_SUFFIX:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
-    case OP_STRING_IN_REGEXP:
-    case OP_STRING_TO_REGEXP:
     case OP_REGEXP_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
@@ -369,7 +401,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("String", _STRING_SORT));
 }
 
 app* seq_decl_plugin::mk_string(symbol const& s) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index e85d01799..c61e3cc43 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -11,10 +11,12 @@ Abstract:
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2011-14-11
+    Nikolaj Bjorner (nbjorner) 2011-11-14
 
 Revision History:
 
+    Updated to string sequences 2015-12-5
+
 --*/
 #ifndef SEQ_DECL_PLUGIN_H_
 #define SEQ_DECL_PLUGIN_H_
@@ -25,20 +27,22 @@ Revision History:
 enum seq_sort_kind {
     SEQ_SORT,
     RE_SORT,
-    STRING_SORT,
-    CHAR_SORT
+    _STRING_SORT,  // internal only
+    _CHAR_SORT     // internal only
 };
 
 enum seq_op_kind {
     OP_SEQ_UNIT,
     OP_SEQ_EMPTY,
     OP_SEQ_CONCAT,
-    OP_SEQ_PREFIX_OF,
-    OP_SEQ_SUFFIX_OF,
-    OP_SEQ_SUBSEQ_OF,
+    OP_SEQ_PREFIX,
+    OP_SEQ_SUFFIX,
+    OP_SEQ_CONTAINS,
     OP_SEQ_EXTRACT,
-    OP_SEQ_NTH,
+    OP_SEQ_AT,
     OP_SEQ_LENGTH,
+    OP_SEQ_TO_RE,
+    OP_SEQ_IN_RE,
 
     OP_RE_PLUS,
     OP_RE_STAR,
@@ -51,28 +55,26 @@ enum seq_op_kind {
     OP_RE_EMPTY_SET,
     OP_RE_FULL_SET,
     OP_RE_EMPTY_SEQ,
-    OP_RE_OF_SEQ,
     OP_RE_OF_PRED,
-    OP_RE_MEMBER,
 
 
     // string specific operators.
     OP_STRING_CONST,
-    _OP_STRING_CONCAT, 
-    OP_STRING_LENGTH, 
-    OP_STRING_SUBSTR, 
-    OP_STRING_STRCTN, 
-    OP_STRING_CHARAT, 
-    OP_STRING_STRIDOF, 
-    OP_STRING_STRREPL, 
-    OP_STRING_PREFIX, 
-    OP_STRING_SUFFIX, 
+    OP_STRING_STRIDOF, // TBD generalize
+    OP_STRING_STRREPL, // TBD generalize
     OP_STRING_ITOS, 
     OP_STRING_STOI, 
-    OP_STRING_IN_REGEXP, 
-    OP_STRING_TO_REGEXP, 
-    OP_REGEXP_LOOP, 
-    
+    OP_REGEXP_LOOP,    // TBD re-loop: integers as parameters or arguments?
+    // internal only operators. Converted to SEQ variants.
+    _OP_STRING_CONCAT, 
+    _OP_STRING_LENGTH, 
+    _OP_STRING_STRCTN,
+    _OP_STRING_PREFIX, 
+    _OP_STRING_SUFFIX, 
+    _OP_STRING_IN_REGEXP, 
+    _OP_STRING_TO_REGEXP, 
+    _OP_STRING_CHARAT, 
+    _OP_STRING_SUBSTR,      
     LAST_SEQ_OP
 };
 
@@ -110,6 +112,9 @@ class seq_decl_plugin : public decl_plugin {
 
     bool is_sort_param(sort* s, unsigned& idx);
 
+    func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string);
+    func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq);
+
     void init();
 
     virtual void set_manager(ast_manager * m, family_id id);
@@ -150,6 +155,7 @@ public:
 
     bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
+    bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
 
     class str {
         seq_util&    u;
@@ -162,45 +168,46 @@ public:
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
         app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
         app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
-        app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
-        app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
-        app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); }
+        app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
+        app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
+        app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
 
-        bool is_const(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
+        bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
         
-        bool is_const(expr const* n, std::string& s) const {
-            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
+        bool is_string(expr const* n, std::string& s) const {
+            return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
         }
-        bool is_const(expr const* n, symbol& s) const {
-            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
+        bool is_string(expr const* n, symbol& s) const {
+            return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
         }
         
+        bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && strcmp(s.bare_str(),"") == 0); }
         bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
-        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_LENGTH); }
-        bool is_substr(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); }
-        bool is_strctn(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_STRCTN); }
-        bool is_charat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CHARAT); }
+        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
+        bool is_extract(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
+        bool is_contains(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
+        bool is_at(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_AT); }
         bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
         bool is_repl(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
-        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_PREFIX); }
-        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUFFIX); }
+        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
+        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
         bool is_itos(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
         bool is_stoi(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STOI); }
-        bool is_in_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IN_REGEXP); }
+        bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
 
         
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);
-        MATCH_TERNARY(is_substr);
-        MATCH_BINARY(is_strctn);
-        MATCH_BINARY(is_charat);
+        MATCH_TERNARY(is_extract);
+        MATCH_BINARY(is_contains);
+        MATCH_BINARY(is_at);
         MATCH_BINARY(is_stridof);
         MATCH_BINARY(is_repl);
         MATCH_BINARY(is_prefix);
         MATCH_BINARY(is_suffix);
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
-        MATCH_BINARY(is_in_regexp);        
+        MATCH_BINARY(is_in_re);        
 
         void get_concat(expr* e, ptr_vector<expr>& es) const;
     };
@@ -212,7 +219,7 @@ public:
     public:
         re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
 
-        bool is_to_regexp(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); }
+        bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
         bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }
         bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
@@ -222,7 +229,7 @@ public:
         bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_RANGE); }
         bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
        
-        MATCH_UNARY(is_to_regexp);
+        MATCH_UNARY(is_to_re);
         MATCH_BINARY(is_concat);
         MATCH_BINARY(is_union);
         MATCH_BINARY(is_inter);
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 03ea3edf8..e8e619bf8 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -71,9 +71,9 @@ namespace smt {
             return 0;
         }
         virtual void register_value(expr* n) {
-            std::string sym;
-            if (u.str.is_const(n, sym)) {
-                m_strings.insert(symbol(sym.c_str()));
+            symbol sym;
+            if (u.str.is_string(n, sym)) {
+                m_strings.insert(sym);
             }
         }
     };