diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp
index 8dc02cc09..3a0300ae4 100644
--- a/src/ast/rewriter/str_rewriter.cpp
+++ b/src/ast/rewriter/str_rewriter.cpp
@@ -198,6 +198,27 @@ br_status str_rewriter::mk_str_Replace(expr * base, expr * source, expr * target
     }
 }
 
+br_status str_rewriter::mk_re_Str2Reg(expr * str, expr_ref & result) {
+	// the argument to Str2Reg *must* be a string constant
+	// TODO is an assertion error too strict here? this basically crashes the solver
+	VERIFY(m_strutil.is_string(str));
+	return BR_FAILED;
+}
+
+br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result) {
+	// fast path:
+	// (RegexIn E (Str2Reg S)) --> (= E S)
+	if (m_strutil.is_re_Str2Reg(re)) {
+		TRACE("t_str_rw", tout << "RegexIn fast path: " << mk_pp(str, m()) << " in " << mk_pp(re, m()) << std::endl;);
+		expr * regexStr = to_app(re)->get_arg(0);
+		VERIFY(m_strutil.is_string(regexStr));
+		result = m().mk_eq(str, regexStr);
+		return BR_REWRITE_FULL;
+	}
+
+	return BR_FAILED;
+}
+
 br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
 
@@ -229,6 +250,12 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_STR_REPLACE:
         SASSERT(num_args == 3);
         return mk_str_Replace(args[0], args[1], args[2], result);
+    case OP_RE_STR2REGEX:
+    	SASSERT(num_args == 1);
+    	return mk_re_Str2Reg(args[0], result);
+    case OP_RE_REGEXIN:
+    	SASSERT(num_args == 2);
+    	return mk_re_RegexIn(args[0], args[1], result);
     default:
         return BR_FAILED;
     }
diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h
index 69a7c9579..5c0e1167f 100644
--- a/src/ast/rewriter/str_rewriter.h
+++ b/src/ast/rewriter/str_rewriter.h
@@ -49,6 +49,9 @@ public:
     br_status mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result);
     br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result);
 
+    br_status mk_re_Str2Reg(expr * str, expr_ref & result);
+    br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
+
     bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);
     bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
 
diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 526b02f64..7cd03fa16 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -24,6 +24,7 @@ Revision History:
 str_decl_plugin::str_decl_plugin():
     m_strv_sym("String"),
     m_str_decl(0),
+	m_regex_decl(0),
     m_concat_decl(0),
     m_length_decl(0),
     m_charat_decl(0),
@@ -35,6 +36,8 @@ str_decl_plugin::str_decl_plugin():
     m_lastindexof_decl(0),
     m_substr_decl(0),
     m_replace_decl(0),
+	m_re_str2regex_decl(0),
+	m_re_regexin_decl(0),
     m_arith_plugin(0),
     m_arith_fid(0),
     m_int_sort(0){
@@ -46,6 +49,7 @@ str_decl_plugin::~str_decl_plugin(){
 void str_decl_plugin::finalize(void) {
     #define DEC_REF(decl) if (decl) { m_manager->dec_ref(decl); } ((void) 0)
     DEC_REF(m_str_decl);
+    DEC_REF(m_regex_decl);
     DEC_REF(m_concat_decl);
     DEC_REF(m_length_decl);
     DEC_REF(m_charat_decl);
@@ -57,6 +61,8 @@ void str_decl_plugin::finalize(void) {
     DEC_REF(m_lastindexof_decl);
     DEC_REF(m_substr_decl);
     DEC_REF(m_replace_decl);
+    DEC_REF(m_re_str2regex_decl);
+    DEC_REF(m_re_regexin_decl);
     DEC_REF(m_int_sort);
 }
 
@@ -66,6 +72,10 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m->inc_ref(m_str_decl);
     sort * s = m_str_decl;
 
+    m_regex_decl = m->mk_sort(symbol("Regex"), sort_info(id, REGEX_SORT));
+    m->inc_ref(m_regex_decl);
+    sort * re = m_regex_decl;
+
     SASSERT(m_manager->has_plugin(symbol("arith")));
     m_arith_fid = m_manager->mk_family_id("arith");
     m_arith_plugin = static_cast<arith_decl_plugin*>(m_manager->get_plugin(m_arith_fid));
@@ -122,6 +132,13 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
         m_replace_decl = m->mk_func_decl(symbol("Replace"), 3, d, s, func_decl_info(id, OP_STR_REPLACE));
         m_manager->inc_ref(m_replace_decl);
     }
+
+    m_re_str2regex_decl = m->mk_func_decl(symbol("Str2Reg"), s, re, func_decl_info(id, OP_RE_STR2REGEX));
+    m_manager->inc_ref(m_re_str2regex_decl);
+
+    m_re_regexin_decl = m->mk_func_decl(symbol("RegexIn"), s, re, boolT, func_decl_info(id, OP_RE_REGEXIN));
+    m_manager->inc_ref(m_re_regexin_decl);
+
 }
 
 decl_plugin * str_decl_plugin::mk_fresh() {
@@ -131,6 +148,7 @@ decl_plugin * str_decl_plugin::mk_fresh() {
 sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
     switch (k) {
     case STRING_SORT: return m_str_decl;
+    case REGEX_SORT: return m_regex_decl;
     default: return 0;
     }
 }
@@ -148,6 +166,8 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     case OP_STR_LASTINDEXOF: return m_lastindexof_decl;
     case OP_STR_SUBSTR: return m_substr_decl;
     case OP_STR_REPLACE: return m_replace_decl;
+    case OP_RE_STR2REGEX: return m_re_str2regex_decl;
+    case OP_RE_REGEXIN: return m_re_regexin_decl;
     default: return 0;
     }
 }
@@ -213,10 +233,13 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF));
     op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR));
     op_names.push_back(builtin_name("Replace", OP_STR_REPLACE));
+    op_names.push_back(builtin_name("Str2Reg", OP_RE_STR2REGEX));
+    op_names.push_back(builtin_name("RegexIn", OP_RE_REGEXIN));
 }
 
 void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
     sort_names.push_back(builtin_name("String", STRING_SORT));
+    sort_names.push_back(builtin_name("Regex", REGEX_SORT));
 }
 
 bool str_decl_plugin::is_value(app * e) const {
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index ee2432c50..496468e5a 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -23,6 +23,7 @@ Revision History:
 
 enum str_sort_kind {
    STRING_SORT,
+   REGEX_SORT,
 };
 
 enum str_op_kind {
@@ -40,6 +41,9 @@ enum str_op_kind {
     OP_STR_LASTINDEXOF,
     OP_STR_SUBSTR,
     OP_STR_REPLACE,
+	// regular expression operators
+	OP_RE_STR2REGEX,
+	OP_RE_REGEXIN,
     // end
     LAST_STR_OP
 };
@@ -48,6 +52,7 @@ class str_decl_plugin : public decl_plugin {
 protected:
     symbol m_strv_sym;
     sort * m_str_decl;
+    sort * m_regex_decl;
 
     func_decl * m_concat_decl;
     func_decl * m_length_decl;
@@ -62,6 +67,9 @@ protected:
     func_decl * m_substr_decl;
     func_decl * m_replace_decl;
 
+    func_decl * m_re_str2regex_decl;
+    func_decl * m_re_regexin_decl;
+
     arith_decl_plugin * m_arith_plugin;
     family_id           m_arith_fid;
     sort *              m_int_sort;
@@ -103,6 +111,8 @@ public:
     bool is_string(expr const * n, const char ** val) const;
     bool is_string(expr const * n) const;
 
+    bool is_re_Str2Reg(expr const * n) const { return is_app_of(n, get_fid(), OP_RE_STR2REGEX); }
+
     std::string get_string_constant_value(expr const *n) const;
     // TODO
 };