diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index f3b3b7edf..c9cdc6ab3 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -647,12 +647,6 @@ extern "C" {
         else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
             return Z3_RE_SORT;
         }
-        else if (fid == mk_c(c)->get_str_fid() && k == STRING_SORT) {
-        	return Z3_STRING_SORT;
-        }
-        else if (fid == mk_c(c)->get_str_fid() && k == REGEX_SORT) {
-        	return Z3_REGEX_SORT;
-        }
         else {
             return Z3_UNKNOWN_SORT;
         }
@@ -1147,16 +1141,6 @@ extern "C" {
             }
         }
 
-        if (mk_c(c)->get_str_fid() == _d->get_family_id()) {
-        	switch (_d->get_decl_kind()) {
-        	// TODO(z3str2) add others
-        	case OP_STRCAT: return Z3_OP_STR_CONCAT;
-        	case OP_STRLEN: return Z3_OP_STR_LENGTH;
-        	default:
-        		return Z3_OP_UNINTERPRETED;
-        	}
-        }
-
         if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
             case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index fd3d16bd0..bcd3c60f2 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -81,7 +81,6 @@ namespace api {
         m_fpa_util(m()),
         m_dtutil(m()),
         m_sutil(m()),
-		m_strutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_pmanager(m_limit) {
@@ -105,7 +104,6 @@ namespace api {
         m_datalog_fid = m().mk_family_id("datalog_relation");
         m_fpa_fid   = m().mk_family_id("fpa");
         m_seq_fid   = m().mk_family_id("seq");
-        m_str_fid   = m().mk_family_id("str");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
     
         install_tactics(*this);
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 7459bd102..6e34f6d6e 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -26,7 +26,6 @@ Revision History:
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"seq_decl_plugin.h"
-#include"str_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"dl_decl_plugin.h"
 #include"fpa_decl_plugin.h"
@@ -63,8 +62,6 @@ namespace api {
         datatype_util              m_dtutil;
         seq_util                   m_sutil;
 
-        str_util                   m_strutil;
-
         // Support for old solver API
         smt_params                 m_fparams;
         // -------------------------------
@@ -130,7 +127,6 @@ namespace api {
         fpa_util & fpautil() { return m_fpa_util; }
         datatype_util& dtutil() { return m_dtutil; }
         seq_util& sutil() { return m_sutil; }
-        str_util& strutil() { return m_strutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
diff --git a/src/api/api_str.cpp b/src/api/api_str.cpp
deleted file mode 100644
index eb56a839b..000000000
--- a/src/api/api_str.cpp
+++ /dev/null
@@ -1,160 +0,0 @@
-/*++
-Copyright (c) 2016 Microsoft Corporation
-
-Module Name:
-
-    api_str.cpp
-
-Abstract:
-
-    API for strings and regular expressions (Z3str2 implementation).
-
-Author:
-
-    Murphy Berzish (mtrberzi) 2016-10-03.
-
-Revision History:
-
---*/
-#include<iostream>
-#include"z3.h"
-#include"api_log_macros.h"
-#include"api_context.h"
-#include"api_util.h"
-#include"ast_pp.h"
-
-extern "C" {
-
-	Z3_sort Z3_API Z3_mk_str_sort(Z3_context c) {
-		Z3_TRY;
-		LOG_Z3_mk_str_sort(c);
-		RESET_ERROR_CODE();
-		sort * ty = mk_c(c)->strutil().mk_string_sort();
-		mk_c(c)->save_ast_trail(ty);
-		RETURN_Z3(of_sort(ty));
-		Z3_CATCH_RETURN(0);
-	}
-
-	Z3_bool Z3_API Z3_is_str_sort(Z3_context c, Z3_sort s) {
-		Z3_TRY;
-		LOG_Z3_is_str_sort(c, s);
-		RESET_ERROR_CODE();
-		bool result = mk_c(c)->strutil().is_str_sort(to_sort(s));
-		return result?Z3_TRUE:Z3_FALSE;
-		Z3_CATCH_RETURN(Z3_FALSE);
-	}
-
-	Z3_bool Z3_API Z3_is_str(Z3_context c, Z3_ast s) {
-		Z3_TRY;
-		LOG_Z3_is_str(c, s);
-		RESET_ERROR_CODE();
-		bool result = mk_c(c)->strutil().is_string(to_expr(s));
-		return result ? Z3_TRUE : Z3_FALSE;
-		Z3_CATCH_RETURN(Z3_FALSE);
-	}
-
-	Z3_string Z3_API Z3_get_str(Z3_context c, Z3_ast s) {
-		Z3_TRY;
-		LOG_Z3_get_str(c, s);
-		RESET_ERROR_CODE();
-		if (!mk_c(c)->strutil().is_string(to_expr(s))) {
-			SET_ERROR_CODE(Z3_INVALID_ARG);
-			return "";
-		}
-		std::string result = mk_c(c)->strutil().get_string_constant_value(to_expr(s));
-		return mk_c(c)->mk_external_string(result);
-		Z3_CATCH_RETURN("");
-	}
-
-	Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str) {
-		Z3_TRY;
-		LOG_Z3_mk_str(c, str);
-		RESET_ERROR_CODE();
-		std::string s(str);
-		app * a = mk_c(c)->strutil().mk_string(str);
-		mk_c(c)->save_ast_trail(a);
-		RETURN_Z3(of_ast(a));
-		Z3_CATCH_RETURN(0);
-	}
-
-	MK_BINARY(Z3_mk_str_concat, mk_c(c)->get_str_fid(), OP_STRCAT, SKIP);
-	MK_UNARY(Z3_mk_str_length, mk_c(c)->get_str_fid(), OP_STRLEN, SKIP);
-	MK_BINARY(Z3_mk_str_at, mk_c(c)->get_str_fid(), OP_STR_CHARAT, SKIP);
-	// translate prefixof/suffixof to StartsWith/EndsWith
-	Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full) {
-		LOG_Z3_mk_str_prefixof(c, pre, full);
-		Z3_TRY;
-		RESET_ERROR_CODE();
-		expr * args[2] = { to_expr(full), to_expr(pre) }; // reverse args
-		ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_STARTSWITH, 0, 0, 2, args);
-		mk_c(c)->save_ast_trail(a);
-		check_sorts(c, a);
-		RETURN_Z3(of_ast(a));
-		Z3_CATCH_RETURN(0);
-	}
-	Z3_ast Z3_API Z3_mk_str_suffixof(Z3_context c, Z3_ast suf, Z3_ast full) {
-		LOG_Z3_mk_str_suffixof(c, suf, full);
-		Z3_TRY;
-		RESET_ERROR_CODE();
-		expr * args[2] = { to_expr(full), to_expr(suf) }; // reverse args
-		ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_ENDSWITH, 0, 0, 2, args);
-		mk_c(c)->save_ast_trail(a);
-		check_sorts(c, a);
-		RETURN_Z3(of_ast(a));
-		Z3_CATCH_RETURN(0);
-	}
-
-	MK_BINARY(Z3_mk_str_contains, mk_c(c)->get_str_fid(), OP_STR_CONTAINS, SKIP);
-	MK_TERNARY(Z3_mk_str_indexof, mk_c(c)->get_str_fid(), OP_STR_INDEXOF, SKIP);
-	MK_TERNARY(Z3_mk_str_substr, mk_c(c)->get_str_fid(), OP_STR_SUBSTR, SKIP);
-	MK_TERNARY(Z3_mk_str_replace, mk_c(c)->get_str_fid(), OP_STR_REPLACE, SKIP);
-
-	Z3_ast Z3_API Z3_mk_str_to_regex(Z3_context c, Z3_string str) {
-		LOG_Z3_mk_str_to_regex(c, str);
-		Z3_TRY;
-		RESET_ERROR_CODE();
-		std::string s(str);
-		app * a = mk_c(c)->strutil().mk_string(str);
-		mk_c(c)->save_ast_trail(a);
-
-		expr * args[1] = { to_expr(a) };
-		ast * re = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_STR2REGEX, 0, 0, 1, args);
-		mk_c(c)->save_ast_trail(re);
-		check_sorts(c, re);
-		RETURN_Z3(of_ast(re));
-		Z3_CATCH_RETURN(0);
-	}
-
-	MK_BINARY(Z3_mk_str_in_regex, mk_c(c)->get_str_fid(), OP_RE_REGEXIN, SKIP);
-	MK_BINARY(Z3_mk_regex_concat, mk_c(c)->get_str_fid(), OP_RE_REGEXCONCAT, SKIP);
-	MK_BINARY(Z3_mk_regex_union, mk_c(c)->get_str_fid(), OP_RE_REGEXUNION, SKIP);
-	MK_UNARY(Z3_mk_regex_star, mk_c(c)->get_str_fid(), OP_RE_REGEXSTAR, SKIP);
-	MK_UNARY(Z3_mk_regex_plus, mk_c(c)->get_str_fid(), OP_RE_REGEXPLUS, SKIP);
-
-	Z3_ast Z3_API Z3_mk_regex_range(Z3_context c, Z3_string start, Z3_string end) {
-		LOG_Z3_mk_regex_range(c, start, end);
-		Z3_TRY;
-		RESET_ERROR_CODE();
-
-		std::string cStart(start);
-		std::string cEnd(end);
-		if(cStart.length() != 1 || cEnd.length() != 1) {
-			SET_ERROR_CODE(Z3_INVALID_ARG);
-			return 0;
-		}
-
-		app * a1 = mk_c(c)->strutil().mk_string(cStart);
-		mk_c(c)->save_ast_trail(a1);
-		app * a2 = mk_c(c)->strutil().mk_string(cEnd);
-		mk_c(c)->save_ast_trail(a2);
-
-		expr * args[2] = { to_expr(a1), to_expr(a2) };
-		ast * range = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_REGEXCHARRANGE, 0, 0, 2, args);
-		mk_c(c)->save_ast_trail(range);
-		check_sorts(c, range);
-		RETURN_Z3(of_ast(range));
-
-		Z3_CATCH_RETURN(0);
-	}
-
-};
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index aa4701f13..0b8351190 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -165,8 +165,6 @@ typedef enum
     Z3_ROUNDING_MODE_SORT,
     Z3_SEQ_SORT,
     Z3_RE_SORT,
-	Z3_STRING_SORT,
-	Z3_REGEX_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 0bff579bc..b1bdf52bd 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -50,7 +50,6 @@ public:
     virtual array_util & get_arutil() = 0;
     virtual fpa_util & get_futil() = 0;
     virtual seq_util & get_sutil() = 0;
-    virtual str_util & get_strutil() = 0;
     virtual datalog::dl_decl_util& get_dlutil() = 0;
     virtual bool uses(symbol const & s) const = 0; 
     virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
@@ -77,17 +76,15 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
     array_util    m_arutil;
     fpa_util      m_futil;
     seq_util      m_sutil;
-    str_util      m_strutil;
     datalog::dl_decl_util m_dlutil;
 public:
-    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_strutil(m), m_dlutil(m) {}
+    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {}
     virtual ast_manager & get_manager() const { return m_manager; }
     virtual arith_util & get_autil() { return m_autil; }
     virtual bv_util & get_bvutil() { return m_bvutil; }
     virtual seq_util & get_sutil() { return m_sutil; }
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
-    virtual str_util & get_strutil() { return m_strutil; }
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const { return false; }
 };
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 75e6a46f1..de6ae6cc3 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -165,7 +165,6 @@ class smt_printer {
     bv_util          m_bvutil;
     seq_util         m_sutil;
     fpa_util         m_futil;
-    str_util         m_strutil;
     family_id        m_basic_fid;
     family_id        m_bv_fid;
     family_id        m_str_fid;
@@ -473,9 +472,6 @@ class smt_printer {
                 m_out << ") bv1[1])";
             }
         }
-        else if (m_strutil.is_string(n, &str)) {
-            m_out << "\"" << str << "\"";
-        }
         else if (m_manager.is_label(n, pos, names) && names.size() >= 1) {
             if (m_is_smt2) {
                 m_out << "(! ";
@@ -839,7 +835,6 @@ public:
         m_bvutil(m),
         m_sutil(m),
         m_futil(m),
-        m_strutil(m),
         m_logic(logic),
         m_AUFLIRA("AUFLIRA"),
         // It's much easier to read those testcases with that.
diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp
index 886e3f495..b4ff63ede 100644
--- a/src/ast/reg_decl_plugins.cpp
+++ b/src/ast/reg_decl_plugins.cpp
@@ -26,7 +26,6 @@ Revision History:
 #include"seq_decl_plugin.h"
 #include"pb_decl_plugin.h"
 #include"fpa_decl_plugin.h"
-#include"str_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
@@ -53,7 +52,4 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
         m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
     }
-    if (!m.get_plugin(m.mk_family_id(symbol("str")))) {
-        m.register_plugin(symbol("str"), alloc(str_decl_plugin));
-    }
 }
diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp
index 045d06b97..3933e7fdb 100644
--- a/src/ast/rewriter/str_rewriter.cpp
+++ b/src/ast/rewriter/str_rewriter.cpp
@@ -17,6 +17,8 @@ Notes:
 
 --*/
 
+#if 0
+
 #include"str_rewriter.h"
 #include"arith_decl_plugin.h"
 #include"ast_pp.h"
@@ -698,3 +700,4 @@ bool str_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     return true;
 }
 
+#endif /* disable */
diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h
index 0494d4d1b..8d6041a51 100644
--- a/src/ast/rewriter/str_rewriter.h
+++ b/src/ast/rewriter/str_rewriter.h
@@ -17,6 +17,8 @@ Notes:
 
 --*/
 
+#if 0
+
 #include"str_decl_plugin.h"
 #include"arith_decl_plugin.h"
 #include"rewriter_types.h"
@@ -114,3 +116,5 @@ public:
 
     bool matches(std::string input);
 };
+
+#endif /* disable */
diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 80493f3cf..067420f04 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -14,6 +14,9 @@ Author:
 Revision History:
 
 --*/
+
+#if 0
+
 #include<sstream>
 #include"str_decl_plugin.h"
 #include"string_buffer.h"
@@ -494,3 +497,5 @@ std::string str_util::get_std_regex_str(expr * regex) {
         UNREACHABLE(); return "";
     }
 }
+
+#endif /* disable */
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index 3ae034b45..28ecd1e43 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -14,6 +14,9 @@ Author:
 Revision History:
 
 --*/
+
+#if 0
+
 #ifndef _STR_DECL_PLUGIN_H_
 #define _STR_DECL_PLUGIN_H_
 
@@ -211,3 +214,5 @@ public:
 };
 
 #endif /* _STR_DECL_PLUGIN_H_ */
+
+#endif /* disable */
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 02f66fc4d..c75c12689 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -21,7 +21,6 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"seq_decl_plugin.h"
-#include"str_decl_plugin.h"
 #include"pb_decl_plugin.h"
 #include"datatype_decl_plugin.h"
 #include"ast_pp.h"
@@ -35,7 +34,6 @@ struct check_logic::imp {
     bv_util       m_bv_util;
     array_util    m_ar_util;
     seq_util      m_seq_util;
-    str_util      m_str_util;
     datatype_util m_dt_util;
     pb_util       m_pb_util;
     bool          m_uf;        // true if the logic supports uninterpreted functions
@@ -49,7 +47,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), m_str_util(m), m_dt_util(m), m_pb_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_dt_util(m), m_pb_util(m) {
         reset();
     }
 
@@ -444,9 +442,6 @@ 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 if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
             // nothing to check
         }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index dc66f5da9..b387e8810 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -26,7 +26,6 @@ Notes:
 #include"seq_decl_plugin.h"
 #include"pb_decl_plugin.h"
 #include"fpa_decl_plugin.h"
-#include"str_decl_plugin.h"
 #include"ast_pp.h"
 #include"var_subst.h"
 #include"pp.h"
@@ -250,7 +249,6 @@ protected:
     array_util    m_arutil;
     fpa_util      m_futil;
     seq_util      m_sutil;
-    str_util      m_strutil;
 
     datalog::dl_decl_util m_dlutil;
 
@@ -272,7 +270,7 @@ protected:
     }
 
 public:
-    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_strutil(o.m()), m_dlutil(o.m()) {}
+    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {}
     virtual ~pp_env() {}
     virtual ast_manager & get_manager() const { return m_owner.m(); }
     virtual arith_util & get_autil() { return m_autil; }
@@ -280,7 +278,7 @@ public:
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
     virtual seq_util & get_sutil() { return m_sutil; }
-    virtual str_util & get_strutil() { return m_strutil; }
+
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const {
         return
@@ -561,7 +559,6 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("pb"),       alloc(pb_decl_plugin), logic_has_pb());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
-        register_plugin(symbol("str"),      alloc(str_decl_plugin), logic_has_str());
     }
     else {
         // the manager was created by an external module
@@ -575,7 +572,6 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("datatype"), logic_has_datatype(), fids);
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
-        load_plugin(symbol("str"),     logic_has_str(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
         svector<family_id>::iterator it  = fids.begin();
         svector<family_id>::iterator end = fids.end();
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index fc28fa6e7..cbfcbf1fe 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -23,7 +23,6 @@ Revision History:
 #include"bv_decl_plugin.h"
 #include"arith_decl_plugin.h"
 #include"seq_decl_plugin.h"
-#include"str_decl_plugin.h"
 #include"ast_pp.h"
 #include"well_sorted.h"
 #include"pattern_validation.h"
@@ -68,7 +67,6 @@ namespace smt2 {
         scoped_ptr<bv_util>               m_bv_util;
         scoped_ptr<arith_util>            m_arith_util;
         scoped_ptr<seq_util>              m_seq_util;
-        scoped_ptr<str_util>              m_str_util;
       
         scoped_ptr<pattern_validator>     m_pattern_validator;
         scoped_ptr<var_shifter>           m_var_shifter;
@@ -286,12 +284,6 @@ namespace smt2 {
             return *(m_bv_util.get());
         }
 
-        str_util & strutil() {
-            if (m_str_util.get() == 0)
-                m_str_util = alloc(str_util, m());
-            return *(m_str_util.get());
-        }
-
         pattern_validator & pat_validator() {
             if (m_pattern_validator.get() == 0) {
                 m_pattern_validator = alloc(pattern_validator, m());
@@ -1086,29 +1078,10 @@ namespace smt2 {
             next();
         }
 
-        // sorry, breaking theory_seq for a bit
-	/*
         void parse_string_const() {
             SASSERT(curr() == scanner::STRING_TOKEN);
             expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string())));
             TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
-	    next();
-	}
-	*/
-
-      void parse_string_const() {
-	parse_string();
-      }
-      
-        void parse_string() {
-            SASSERT(curr() == scanner::STRING_TOKEN);
-            char const *original_token = m_scanner.get_string();
-            size_t bufsize = strlen(original_token);
-            char * buf = alloc_svect(char, bufsize + 1);
-            strncpy(buf, original_token, bufsize);
-            buf[bufsize] = '\0';
-            TRACE("parse_string", tout << "new string constant: " << buf << " length=" << bufsize << "\n";);
-            expr_stack().push_back(strutil().mk_string_with_escape_characters(buf));
             next();
         }
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 80781d6aa..1d56c43a4 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -44,7 +44,7 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
         /* Internal setup */
         search_started(false),
         m_autil(m),
-        m_strutil(m),
+        u(m),
         sLevel(0),
         finalCheckProgressIndicator(false),
         m_trail(m),
@@ -70,36 +70,26 @@ theory_str::~theory_str() {
     m_trail_stack.reset();
 }
 
-expr * theory_str::mk_string(std::string str) {
+expr * theory_str::mk_string(zstring const& str) {
     if (m_params.m_StringConstantCache) {
         ++totalCacheAccessCount;
         expr * val;
         if (stringConstantCache.find(str, val)) {
-            // cache hit
-            ++cacheHitCount;
-            TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
-                    << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
-                    << totalCacheAccessCount << " accesses)" << std::endl;);
             return val;
         } else {
-            // cache miss
-            ++cacheMissCount;
-            TRACE("t_str_cache", tout << "cache miss: \"" << str << "\" ("
-                            << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
-                            << totalCacheAccessCount << " accesses)" << std::endl;);
-            val = m_strutil.mk_string(str);
+            val = u.str.mk_string(str);
             m_trail.push_back(val);
             stringConstantCache.insert(str, val);
             return val;
         }
     } else {
-        return m_strutil.mk_string(str);
+        return u.str.mk_string(str);
     }
 }
 
 expr * theory_str::mk_string(const char * str) {
-    std::string valStr(str);
-    return mk_string(valStr);
+    symbol sym(str);
+    return u.str.mk_string(sym);
 }
 
 void theory_str::initialize_charset() {
@@ -210,25 +200,6 @@ void theory_str::assert_implication(expr * premise, expr * conclusion) {
 }
 
 bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
-    /*
-    TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
-    SASSERT(atom->get_family_id() == get_family_id());
-
-    context & ctx = get_context();
-
-    if (ctx.b_internalized(atom))
-        return true;
-
-    unsigned num_args = atom->get_num_args();
-    for (unsigned i = 0; i < num_args; i++)
-        ctx.internalize(atom->get_arg(i), false);
-
-    literal l(ctx.mk_bool_var(atom));
-
-    ctx.set_var_theory(l.var(), get_id());
-
-    return true;
-    */
     return internalize_term(atom);
 }
 
@@ -267,10 +238,9 @@ bool theory_str::internalize_term(app * term) {
     theory_var v = mk_var(e);
     TRACE("t_str_detail", tout << "term has theory var #" << v << std::endl;);
 
-    if (opt_EagerStringConstantLengthAssertions && m_strutil.is_string(term)) {
+    if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) {
         TRACE("t_str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;);
         m_basicstr_axiom_todo.insert(e);
-        TRACE("t_str_axiom_bug", tout << "add " << mk_pp(e->get_owner(), m) << " to m_basicstr_axiom_todo" << std::endl;);
     }
     return true;
 }
@@ -295,7 +265,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()), m_strutil.get_fid(), STRING_SORT))) {
+    if (!(is_sort_of(m.get_sort(n->get_owner()), u.get_family_id(), _STRING_SORT))) {
         return null_theory_var;
     }
     if (is_attached_to_var(n)) {
@@ -413,7 +383,7 @@ void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode)
 void theory_str::check_and_init_cut_var(expr * node) {
     if (cut_var_map.contains(node)) {
         return;
-    } else if (!m_strutil.is_string(node)) {
+    } else if (!u.str.is_string(node)) {
         add_cut_info_one_node(node, -1, node);
     }
 }
@@ -511,7 +481,7 @@ app * theory_str::mk_str_var(std::string name) {
 
 	TRACE("t_str_detail", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;);
 
-	sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
+	sort * string_sort = u.str.mk_string_sort();
 	app * a = m.mk_fresh_const(name.c_str(), string_sort);
 
 	TRACE("t_str_detail", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
@@ -538,7 +508,7 @@ app * theory_str::mk_regex_rep_var() {
 	context & ctx = get_context();
 	ast_manager & m = get_manager();
 
-	sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
+	sort * string_sort = u.str.mk_string_sort();
 	app * a = m.mk_fresh_const("regex", string_sort);
 
 	ctx.internalize(a, false);
@@ -590,7 +560,7 @@ app * theory_str::mk_nonempty_str_var() {
 
     TRACE("t_str_detail", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;);
 
-    sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
+    sort * string_sort = u.str.mk_string_sort();
     app * a = m.mk_fresh_const(name.c_str(), string_sort);
 
     ctx.internalize(a, false);
@@ -642,8 +612,7 @@ app * theory_str::mk_unroll(expr * n, expr * bound) {
 }
 
 app * theory_str::mk_contains(expr * haystack, expr * needle) {
-    expr * args[2] = {haystack, needle};
-    app * contains = get_manager().mk_app(get_id(), OP_STR_CONTAINS, 0, 0, 2, args);
+    app * contains = u.str.mk_contains(haystack, needle); // TODO double-check semantics/argument order
     m_trail.push_back(contains);
     // immediately force internalization so that axiom setup does not fail
     get_context().internalize(contains, false);
@@ -652,8 +621,8 @@ app * theory_str::mk_contains(expr * haystack, expr * needle) {
 }
 
 app * theory_str::mk_indexof(expr * haystack, expr * needle) {
-    expr * args[2] = {haystack, needle};
-    app * indexof = get_manager().mk_app(get_id(), OP_STR_INDEXOF, 0, 0, 2, args);
+    // TODO check meaning of the third argument here
+    app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
     m_trail.push_back(indexof);
     // immediately force internalization so that axiom setup does not fail
     get_context().internalize(indexof, false);
@@ -663,25 +632,23 @@ app * theory_str::mk_indexof(expr * haystack, expr * needle) {
 
 app * theory_str::mk_strlen(expr * e) {
     /*if (m_strutil.is_string(e)) {*/ if (false) {
-        const char * strval = 0;
-        m_strutil.is_string(e, &strval);
-        int len = strlen(strval);
+        zstring strval;
+        u.str.is_string(e, strval);
+        unsigned int len = strval.length();
         return m_autil.mk_numeral(rational(len), true);
     } else {
         if (false) {
             // use cache
             app * lenTerm = NULL;
             if (!length_ast_map.find(e, lenTerm)) {
-                expr * args[1] = {e};
-                lenTerm = get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+                lenTerm = u.str.mk_length(e);
                 length_ast_map.insert(e, lenTerm);
                 m_trail.push_back(lenTerm);
             }
             return lenTerm;
         } else {
             // always regen
-            expr * args[1] = {e};
-            return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
+            return u.str.mk_length(e);
         }
     }
 }
@@ -699,24 +666,22 @@ expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
     expr * v1 = get_eqc_value(n1, n1HasEqcValue);
     expr * v2 = get_eqc_value(n2, n2HasEqcValue);
     if (n1HasEqcValue && n2HasEqcValue) {
-        const char * n1_str_tmp;
-        m_strutil.is_string(v1, & n1_str_tmp);
-        std::string n1_str(n1_str_tmp);
-        const char * n2_str_tmp;
-        m_strutil.is_string(v2, & n2_str_tmp);
-        std::string n2_str(n2_str_tmp);
-        std::string result = n1_str + n2_str;
+        zstring n1_str;
+        u.str.is_string(v1, n1_str);
+        zstring n2_str;
+        u.str.is_string(v2, n2_str);
+        zstring result = n1_str + n2_str;
         return mk_string(result);
     } else if (n1HasEqcValue && !n2HasEqcValue) {
-        const char * n1_str_tmp;
-        m_strutil.is_string(v1, & n1_str_tmp);
-        if (strcmp(n1_str_tmp, "") == 0) {
+        zstring n1_str;
+        u.str.is_string(v1, n1_str);
+        if (n1_str.empty()) {
             return n2;
         }
     } else if (!n1HasEqcValue && n2HasEqcValue) {
-        const char * n2_str_tmp;
-        m_strutil.is_string(v2, & n2_str_tmp);
-        if (strcmp(n2_str_tmp, "") == 0) {
+        zstring n2_str;
+        u.str.is_string(v2, n2_str);
+        if (n2_str.empty()) {
             return n1;
         }
     }
@@ -735,38 +700,42 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
 	if (n1HasEqcValue && n2HasEqcValue) {
 	    return mk_concat_const_str(n1, n2);
 	} else if (n1HasEqcValue && !n2HasEqcValue) {
-	    bool n2_isConcatFunc = is_concat(to_app(n2));
-	    if (m_strutil.get_string_constant_value(n1) == "") {
+	    bool n2_isConcatFunc = u.str.is_concat(to_app(n2));
+	    zstring n1_str;
+	    u.str.is_string(n1, n1_str);
+	    if (n1_str.empty()) {
 	        return n2;
 	    }
 	    if (n2_isConcatFunc) {
 	        expr * n2_arg0 = to_app(n2)->get_arg(0);
 	        expr * n2_arg1 = to_app(n2)->get_arg(1);
-	        if (m_strutil.is_string(n2_arg0)) {
+	        if (u.str.is_string(n2_arg0)) {
 	            n1 = mk_concat_const_str(n1, n2_arg0); // n1 will be a constant
 	            n2 = n2_arg1;
 	        }
 	    }
 	} else if (!n1HasEqcValue && n2HasEqcValue) {
-	    if (m_strutil.get_string_constant_value(n2) == "") {
+	    zstring n2_str;
+	    u.str.is_string(n2, n2_str);
+	    if (n2_str.empty()) {
 	        return n1;
 	    }
 
-	    if (is_concat(to_app(n1))) {
+	    if (u.str.is_concat(to_app(n1))) {
 	        expr * n1_arg0 = to_app(n1)->get_arg(0);
 	        expr * n1_arg1 = to_app(n1)->get_arg(1);
-	        if (m_strutil.is_string(n1_arg1)) {
+	        if (u.str.is_string(n1_arg1)) {
 	            n1 = n1_arg0;
 	            n2 = mk_concat_const_str(n1_arg1, n2); // n2 will be a constant
 	        }
 	    }
 	} else {
-	    if (is_concat(to_app(n1)) && is_concat(to_app(n2))) {
+	    if (u.str.is_concat(to_app(n1)) && u.str.is_concat(to_app(n2))) {
 	        expr * n1_arg0 = to_app(n1)->get_arg(0);
 	        expr * n1_arg1 = to_app(n1)->get_arg(1);
 	        expr * n2_arg0 = to_app(n2)->get_arg(0);
 	        expr * n2_arg1 = to_app(n2)->get_arg(1);
-	        if (m_strutil.is_string(n1_arg1) && m_strutil.is_string(n2_arg0)) {
+	        if (u.str.is_string(n1_arg1) && u.str.is_string(n2_arg0)) {
 	            expr * tmpN1 = n1_arg0;
 	            expr * tmpN2 = mk_concat_const_str(n1_arg1, n2_arg0);
 	            n1 = mk_concat(tmpN1, tmpN2);
@@ -784,8 +753,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
 	expr * concatAst = NULL;
 
 	if (!concat_astNode_map.find(n1, n2, concatAst)) {
-	    expr * args[2] = {n1, n2};
-	    concatAst = m.mk_app(get_id(), OP_STRCAT, 0, 0, 2, args);
+	    concatAst = u.str.mk_concat(n1, n2);
 	    m_trail.push_back(concatAst);
 	    concat_astNode_map.insert(n1, n2, concatAst);
 
@@ -841,25 +809,30 @@ void theory_str::propagate() {
 
         for (unsigned i = 0; i < m_library_aware_axiom_todo.size(); ++i) {
         	enode * e = m_library_aware_axiom_todo[i];
-        	if (is_str_to_int(e)) {
+        	app * a = e->get_owner();
+        	if (u.str.is_stoi(a)) {
         		instantiate_axiom_str_to_int(e);
-        	} else if (is_int_to_str(e)) {
+        	} else if (u.str.is_itos(a)) {
         	    instantiate_axiom_int_to_str(e);
-        	} else if (is_CharAt(e)) {
+        	} else if (u.str.is_at(a)) {
         	    instantiate_axiom_CharAt(e);
+        	    /* TODO NEXT: StartsWith/EndsWith -> prefixof/suffixof
         	} else if (is_StartsWith(e)) {
         	    instantiate_axiom_StartsWith(e);
         	} else if (is_EndsWith(e)) {
         	    instantiate_axiom_EndsWith(e);
-        	} else if (is_Contains(e)) {
+        	    */
+        	} else if (u.str.is_contains(a)) {
         	    instantiate_axiom_Contains(e);
-        	} else if (is_Indexof(e)) {
+        	} else if (u.str.is_index(a)) {
         	    instantiate_axiom_Indexof(e);
+        	    /* TODO NEXT: Indexof2/Lastindexof rewrite?
         	} else if (is_Indexof2(e)) {
         	    instantiate_axiom_Indexof2(e);
         	} else if (is_LastIndexof(e)) {
         	    instantiate_axiom_LastIndexof(e);
-        	} else if (is_Substr(e)) {
+        	    */
+        	} else if (u.str.is_substr(a)) {
         	    instantiate_axiom_Substr(e);
         	} else if (is_Replace(e)) {
         	    instantiate_axiom_Replace(e);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 6b1ce9023..63f5d3cfc 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -27,32 +27,13 @@ Revision History:
 #include<set>
 #include<stack>
 #include<vector>
-#include"str_rewriter.h"
+#include<map>
+#include"seq_decl_plugin.h"
 #include"union_find.h"
+#include"theory_seq_empty.h"
 
 namespace smt {
 
-    class str_value_factory : public value_factory {
-        str_util m_util;
-    public:
-        str_value_factory(ast_manager & m, family_id fid) :
-            value_factory(m, fid),
-            m_util(m) {}
-        virtual ~str_value_factory() {}
-        virtual expr * get_some_value(sort * s) {
-            return m_util.mk_string("some value");
-        }
-        virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
-            v1 = m_util.mk_string("value 1");
-            v2 = m_util.mk_string("value 2");
-            return true;
-        }
-        virtual expr * get_fresh_value(sort * s) {
-            return m_util.mk_fresh_string();
-        }
-        virtual void register_value(expr * n) { /* Ignore */ }
-    };
-
     // rather than modify obj_pair_map I inherit from it and add my own helper methods
     class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
     public:
@@ -110,12 +91,12 @@ namespace smt {
         typedef union_find<theory_str> th_union_find;
 
         typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
-        struct str_hash_proc {
-            unsigned operator()(std::string const & s) const {
-            	return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17);
+        struct zstring_hash_proc {
+            unsigned operator()(zstring const & s) const {
+            	return string_hash(s.encode().c_str(), static_cast<unsigned>(s.length()), 17);
             }
         };
-        typedef map<std::string, expr*, str_hash_proc, default_eq<std::string> > string_map;
+        typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
 
     protected:
         theory_str_params const & m_params;
@@ -188,14 +169,14 @@ namespace smt {
 
         bool search_started;
         arith_util m_autil;
-        str_util m_strutil;
+        seq_util u;
         int sLevel;
 
         bool finalCheckProgressIndicator;
 
         expr_ref_vector m_trail; // trail for generated terms
 
-        str_value_factory * m_factory;
+        seq_factory * m_factory;
 
         // terms we couldn't go through set_up_axioms() with because they weren't internalized
         expr_ref_vector m_delayed_axiom_setup_terms;
@@ -259,7 +240,7 @@ namespace smt {
         std::map<std::pair<expr*, std::string>, expr*> regex_in_bool_map;
         std::map<expr*, std::set<std::string> > regex_in_var_reg_str_map;
 
-        std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+        // std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
 
         char * char_set;
         std::map<char, int> charSetLookupTable;
@@ -327,7 +308,7 @@ namespace smt {
         void assert_implication(expr * premise, expr * conclusion);
         expr * rewrite_implication(expr * premise, expr * conclusion);
 
-        expr * mk_string(std::string str);
+        expr * mk_string(zstring const& str);
         expr * mk_string(const char * str);
 
         app * mk_strlen(expr * e);
@@ -359,48 +340,6 @@ namespace smt {
         app * mk_unroll_test_var();
         void add_nonempty_constraint(expr * s);
 
-        bool is_concat(app const * a) const { return a->is_app_of(get_id(), OP_STRCAT); }
-        bool is_concat(enode const * n) const { return is_concat(n->get_owner()); }
-        bool is_string(app const * a) const { return a->is_app_of(get_id(), OP_STR); }
-        bool is_string(enode const * n) const { return is_string(n->get_owner()); }
-        bool is_strlen(app const * a) const { return a->is_app_of(get_id(), OP_STRLEN); }
-        bool is_strlen(enode const * n) const { return is_strlen(n->get_owner()); }
-        bool is_CharAt(app const * a) const { return a->is_app_of(get_id(), OP_STR_CHARAT); }
-        bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); }
-        bool is_StartsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_STARTSWITH); }
-        bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); }
-        bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); }
-        bool is_EndsWith(enode const * n) const { return is_EndsWith(n->get_owner()); }
-        bool is_Contains(app const * a) const { return a->is_app_of(get_id(), OP_STR_CONTAINS); }
-        bool is_Contains(enode const * n) const { return is_Contains(n->get_owner()); }
-        bool is_Indexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF); }
-        bool is_Indexof(enode const * n) const { return is_Indexof(n->get_owner()); }
-        bool is_Indexof2(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF2); }
-        bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); }
-        bool is_LastIndexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_LASTINDEXOF); }
-        bool is_LastIndexof(enode const * n) const { return is_LastIndexof(n->get_owner()); }
-        bool is_Substr(app const * a) const { return a->is_app_of(get_id(), OP_STR_SUBSTR); }
-        bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); }
-        bool is_Replace(app const * a) const { return a->is_app_of(get_id(), OP_STR_REPLACE); }
-        bool is_Replace(enode const * n) const { return is_Replace(n->get_owner()); }
-        bool is_str_to_int(app const * a) const { return a->is_app_of(get_id(), OP_STR_STR2INT); }
-		bool is_str_to_int(enode const * n) const { return is_str_to_int(n->get_owner()); }
-		bool is_int_to_str(app const * a) const { return a->is_app_of(get_id(), OP_STR_INT2STR); }
-        bool is_int_to_str(enode const * n) const { return is_int_to_str(n->get_owner()); }
-
-        bool is_RegexIn(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXIN); }
-        bool is_RegexIn(enode const * n) const { return is_RegexIn(n->get_owner()); }
-        bool is_RegexConcat(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXCONCAT); }
-        bool is_RegexConcat(enode const * n) const { return is_RegexConcat(n->get_owner()); }
-        bool is_RegexStar(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXSTAR); }
-        bool is_RegexStar(enode const * n) const { return is_RegexStar(n->get_owner()); }
-        bool is_RegexUnion(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXUNION); }
-        bool is_RegexUnion(enode const * n) const { return is_RegexUnion(n->get_owner()); }
-        bool is_Str2Reg(app const * a) const { return a->is_app_of(get_id(), OP_RE_STR2REGEX); }
-		bool is_Str2Reg(enode const * n) const { return is_Str2Reg(n->get_owner()); }
-		bool is_Unroll(app const * a) const { return a->is_app_of(get_id(), OP_RE_UNROLL); }
-		bool is_Unroll(enode const * n) const { return is_Unroll(n->get_owner()); }
-
         void instantiate_concat_axiom(enode * cat);
         void try_eval_concat(enode * cat);
         void instantiate_basic_string_axioms(enode * str);