diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 5de672b1a2..79c542f06b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4155,6 +4155,14 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
     len = min_length(hi).second;
     if (len > 1)
         is_empty = true;
+    // A bound that is provably of length 0 (e.g. the empty string "") can
+    // likewise never be a single character, so the range is empty.  Unlike a
+    // symbolic bound, max_length == 0 is a provable emptiness fact, so this is
+    // sound (it is never true for a model-dependent bound such as a variable).
+    if (max_length(lo) == std::make_pair(true, rational(0)))
+        is_empty = true;
+    if (max_length(hi) == std::make_pair(true, rational(0)))
+        is_empty = true;
 
     // A provable length constraint (a bound can never be a single character)
     // is the only sound way to conclude emptiness for a possibly-symbolic