diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp
index c644ecd46..015898a64 100644
--- a/src/ast/rewriter/str_rewriter.cpp
+++ b/src/ast/rewriter/str_rewriter.cpp
@@ -425,6 +425,15 @@ br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result)
 	return BR_FAILED;
 }
 
+br_status str_rewriter::mk_re_RegexStar(expr * re, expr_ref & result) {
+    if (m_strutil.is_re_RegexStar(re)) {
+        result = re;
+        return BR_REWRITE_FULL;
+    } else {
+        return BR_FAILED;
+    }
+}
+
 br_status str_rewriter::mk_re_RegexPlus(expr * re, expr_ref & result) {
     /*
      * Two optimizations are possible if we inspect 're'.
@@ -523,6 +532,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_REGEXPLUS:
         SASSERT(num_args == 1);
         return mk_re_RegexPlus(args[0], result);
+    case OP_RE_REGEXSTAR:
+        SASSERT(num_args == 1);
+        return mk_re_RegexStar(args[0], result);
     case OP_RE_REGEXCHARRANGE:
         SASSERT(num_args == 2);
         return mk_re_RegexCharRange(args[0], args[1], result);
diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h
index c64d086f9..d147e82e8 100644
--- a/src/ast/rewriter/str_rewriter.h
+++ b/src/ast/rewriter/str_rewriter.h
@@ -57,6 +57,7 @@ public:
     br_status mk_re_Str2Reg(expr * str, expr_ref & result);
     br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
     br_status mk_re_RegexPlus(expr * re, expr_ref & result);
+    br_status mk_re_RegexStar(expr * re, expr_ref & result);
     br_status mk_re_RegexCharRange(expr * start, expr * end, expr_ref & result);
 
     bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);