diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 34290bf74..3f2cd423b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4829,10 +4829,12 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
     unsigned lo_v = 0, hi_v = 0;
     if (re().is_range(a, lo_v, hi_v)) {
         unsigned max_c = u().max_char();
-        sort* srt = a->get_sort();
+        sort *srt = a->get_sort(), *seq_sort;
+        VERIFY(m_util.is_re(a, seq_sort));
         bool has_left = (lo_v > 0);
         bool has_right = (hi_v < max_c);
         auto empty_re = [&]() { return re().mk_empty(srt); };
+        auto len0_re = [&]() { return re().mk_to_re(str().mk_empty(seq_sort)); };
         auto full_re = [&]() { return re().mk_full_seq(srt); };
         if (!has_left && !has_right) {
             // [0, max_c]: complement is empty
@@ -4845,18 +4847,18 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         }
         if (!has_left) {
             // [0, b]: complement is [b+1, max]
-            result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
+            result = re().mk_union(len0_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
             return BR_DONE;
         }
         if (!has_right) {
             // [a, max]: complement is [0, a-1]
-            result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
+            result = re().mk_union(len0_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
             return BR_DONE;
         }
         // General: [a, b] → [0, a-1] ∪ [b+1, max]
         auto left = re().mk_range(srt, 0u, lo_v - 1);
         auto right = re().mk_range(srt, hi_v + 1, max_c);
-        result = re().mk_union(empty_re(), re().mk_concat(re().mk_union(left, right), full_re()));
+        result = re().mk_union(len0_re(), re().mk_concat(re().mk_union(left, right), full_re()));
         return BR_DONE;
     }
     return BR_FAILED;