From 7598285dd4b55abb6e3e022da93f8ef16c4131c3 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Wed, 1 Jul 2026 03:27:48 -0700
Subject: [PATCH] Fix unsound collapse of symbolic re.range bounds in
 seq_rewriter

mk_re_range extracts a constant character from each bound and, when
extraction fails, marked the range empty (is_empty = true), collapsing
(re.range lo hi) to the empty regex. For a symbolic bound such as a
String variable `a` in (re.range a "u"), extraction fails even though
`a` may denote a single-character string at solving time. Collapsing to
re.empty is therefore unsound: it turns satisfiable membership
constraints into unsat.

Return BR_FAILED for non-constant bounds instead, leaving the range
node intact for the theory/derivative solver. The sound emptiness
checks for provably non-singleton bounds (min_length > 1, max_length
== 0) and the constant-bound ordering/singleton cases are preserved.

With this fix (simplify (re.range a "u")) yields (re.range a "u")
instead of re.none, and benchmarks that assert satisfiable string
membership over symbolic ranges are no longer reported unsat.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 9e4a6ca72c..314726a684 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4126,13 +4126,20 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
         is_empty = true;
     if (max_length(hi) == std::make_pair(true, rational(0)))
         is_empty = true;
+    // Extract constant character bounds.  A bound that is neither a constant
+    // character nor a provably non-singleton string (the length checks above
+    // already handle the latter) may still denote a singleton string at
+    // solving time, e.g. a String variable such as `a` in (re.range a "u").
+    // In that case the range is symbolic and must be left for the theory
+    // solver: collapsing it to the empty regex here is unsound (it wrongly
+    // turns satisfiable membership constraints into unsat).
     if (!is_empty) {
         if (str().is_string(lo, slo) && slo.length() == 1) 
             clo = slo[0];    
         else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
             ;
         else
-            is_empty = true;
+            return BR_FAILED;
     }
     if (!is_empty) {
         if (str().is_string(hi, shi) && shi.length() == 1)
@@ -4140,7 +4147,7 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
         else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
             ;
         else
-            is_empty = true;
+            return BR_FAILED;
     }
 
     // clo/chi are only meaningful once both bounds were extracted; an early