From eab5ff1eff64d6732e5b29de816b0772adb894c0 Mon Sep 17 00:00:00 2001
From: Margus Veanes <margus@microsoft.com>
Date: Fri, 26 Jun 2026 06:58:41 +0300
Subject: [PATCH] Fix uninitialized clo/chi read in mk_re_range; drop disabled
 test block

mk_re_range read clo/chi in the singleton/ordering checks before the
is_empty guard, but an early is_empty (from the length checks) leaves
them uninitialized. Initialize to 0 and move the is_empty return ahead
of the singleton check so uninitialized values are never used.

Also remove the disabled if(false) range-complement block in the
seq_rewriter unit test.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 19 +++++++++++--------
 src/test/seq_rewriter.cpp         | 12 ------------
 2 files changed, 11 insertions(+), 20 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index c680f91f74..daa2714e4a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4117,7 +4117,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
  */
 br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
     zstring slo, shi;
-    unsigned clo, chi;
+    unsigned clo = 0, chi = 0;
     expr *lo1, *hi1;
     unsigned len = 0;
     bool is_empty = false;
@@ -4148,20 +4148,23 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
             is_empty = true;
     }
 
-    if (clo > chi)
+    // clo/chi are only meaningful once both bounds were extracted; an early
+    // is_empty (from the length checks) leaves them at their default 0, so the
+    // is_empty return must come before the singleton/ordering checks below.
+    if (!is_empty && clo > chi)
         is_empty = true;
-    // Singleton: re.range "a" "a" → str.to_re "a"
-    if (clo == chi) {
-        result = re().mk_to_re(str().mk_string(zstring(clo)));
-        return BR_DONE;
-    }
-            
+
     if (is_empty) {
         sort* srt = re().mk_re(lo->get_sort());
         result = re().mk_empty(srt);
         return BR_DONE;
     }
 
+    // Singleton: re.range "a" "a" → str.to_re "a"
+    if (clo == chi) {
+        result = re().mk_to_re(str().mk_string(zstring(clo)));
+        return BR_DONE;
+    }
 
     return BR_FAILED;
 }
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index c2e3b9a355..658675fa72 100644
--- a/src/test/seq_rewriter.cpp
+++ b/src/test/seq_rewriter.cpp
@@ -125,18 +125,6 @@ void tst_seq_rewriter() {
     }
 
 
-    // -----------------------------------------------------------------------
-    // 10. Range complement (lo = 0): single range e union [hi+1, max].*
-    // -----------------------------------------------------------------------
-    if (false) {
-        expr_ref lo_str(su.str.mk_string(zstring(0u)), m);
-        expr_ref hi_str(su.str.mk_string(zstring((unsigned)'f')), m);
-        expr_ref e(su.re.mk_complement(su.re.mk_range(lo_str, hi_str)), m);
-        rw(e);
-        std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n";
-        ENSURE(!su.re.is_complement(e));
-    }
-
     // -----------------------------------------------------------------------
     // 11. Downstream: (re.* (re.range "z" "a")) → str.to_re ""
     // -----------------------------------------------------------------------