diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 0cb6f7394..f363b58e6 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -308,7 +308,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
             return a.detach();            
         }
         else {
-            TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";);
+            // if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
+            return alloc(eautomaton, sm);
         }
     }
     else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
index b26959e49..8ce201752 100644
--- a/src/smt/theory_str_regex.cpp
+++ b/src/smt/theory_str_regex.cpp
@@ -812,9 +812,11 @@ namespace smt {
             zstring str1, str2;
             u.str.is_string(sub1, str1);
             u.str.is_string(sub2, str2);
-            SASSERT(str1.length() == 1);
-            SASSERT(str2.length() == 1);
-            return 1 + str2[0] - str1[0];
+            if (str1.length() == 1 && str2.length() == 1) {
+                return 1 + str2[0] - str1[0];
+            } else {
+                return 1;
+            }
         } else if (u.re.is_full_char(re) || u.re.is_full_seq(re)) {
             return 1;
         } else {
@@ -964,9 +966,13 @@ namespace smt {
             zstring str1, str2;
             u.str.is_string(sub1, str1);
             u.str.is_string(sub2, str2);
-            SASSERT(str1.length() == 1);
-            SASSERT(str2.length() == 1);
-            lens.insert(1);
+            // re.range is a language of singleton strings if both of its arguments are;
+            // otherwise it is the empty language
+            if (str1.length() == 1 && str2.length() == 1) {
+                lens.insert(1);
+            } else {
+                lens.insert(0);
+            }
         } else if (u.re.is_full_char(re)) {
             lens.insert(1);
         } else if (u.re.is_full_seq(re)) {