diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 0c77dfcf2..4efb4b9d7 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -350,7 +350,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         return mk_re_union(args[0], args[1], result);
     case OP_RE_RANGE:
-        return BR_FAILED;    
+        SASSERT(num_args == 2);
+        return mk_re_range(args[0], args[1], result);
     case OP_RE_INTERSECT:
         SASSERT(num_args == 2);
         return mk_re_inter(args[0], args[1], result);
@@ -1313,6 +1314,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+/*
+ * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
+ */
+br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
+    TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
+    zstring str_lo, str_hi;
+    if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
+        if (str_lo.length() == 1 && str_hi.length() == 1) {
+            unsigned int c1 = str_lo[0];
+            unsigned int c2 = str_hi[0];
+            if (c1 > c2) {
+                // exchange c1 and c2
+                unsigned int tmp = c1;
+                c2 = c1;
+                c1 = tmp;
+            }
+            zstring s(c1);
+            expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
+            for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
+                zstring s_ch(ch);
+                expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
+                acc = m_util.re.mk_union(acc, acc2);
+            }
+            result = acc;
+            return BR_REWRITE2;
+        } else {
+            m().raise_exception("string constants in re.range must have length 1");
+        }
+    }
+
+    return BR_FAILED;
+}
+
 /*
    emp+ = emp
    all+ = all
@@ -1342,9 +1376,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
         return BR_DONE;
     }
 
-    return BR_FAILED;
-//  result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
-//  return BR_REWRITE2;
+    //return BR_FAILED;
+    result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
+    return BR_REWRITE2;
 }
 
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index eed08e376..210b2d72c 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -120,6 +120,7 @@ class seq_rewriter {
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
     br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
+    br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
 
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r,