Fix unsound empty collapse of symbolic-bound re.range

`re.range(lo, hi)` was being collapsed to the empty language whenever a
bound was not a ground single character. This is unsound: for a symbolic
bound whose value is a single character (e.g. `re.range("-", y)` with
`|y| = 1`), the range is non-empty, yet the solver returned `unsat` for
satisfiable formulas.

The regression was introduced by the derivative refactor #9965, which
dropped the symbolic-bound handling that the previous Antimirov
derivative had for ranges.

Two coordinated changes restore both soundness and completeness:

* seq_rewriter::mk_re_range: return BR_FAILED (leaving the range for the
  theory solver) instead of collapsing to `re.empty` when a bound is not
  a ground single character. The sound checks (length bounds, constant
  ordering, singleton) are preserved.

* seq::derive::derive_range: handle non-ground bounds by emitting the
  length-one constraint together with the character-order comparison,
  i.e. for a non-ground bound b, `|b| = 1 ∧ ... b[0] ...`, mirroring the
  pre-#9965 Antimirov derivative. This lets the derivative-based theory
  solver decide membership instead of producing a stuck derivative
  (which yielded `unknown`).

Validated by rebuilding z3 and re-running the affected benchmarks: all
re.range regression inputs now match their expected results.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/ast/rewriter/seq_derive.cpp

@@ -398,7 +398,9 @@ namespace seq {
 
         // Extract character values from unit strings
         expr_ref c_lo(m), c_hi(m);
-        if (u().str.is_unit_string(lo, c_lo) && u().str.is_unit_string(hi, c_hi)) {
+        bool lo_unit = u().str.is_unit_string(lo, c_lo);
+        bool hi_unit = u().str.is_unit_string(hi, c_hi);
+        if (lo_unit && hi_unit) {
             // Build range condition, simplifying trivial bounds
             unsigned lo_val = 0, hi_val = 0;
             bool lo_trivial = m_util.is_const_char(c_lo, lo_val) && lo_val == 0;
@@ -418,6 +420,38 @@ namespace seq {
             return mk_ite(in_range, eps, empty);
         }
 
+        // Symbolic (non-ground) bound(s): a non-literal bound denotes a single
+        // character only when its length is 1. Encode that length constraint
+        // explicitly together with the character-order comparison so the theory
+        // solver can still decide membership instead of producing a stuck
+        // derivative. (Collapsing such a range to ∅ here would be unsound: e.g.
+        // re.range("-", y) with |y| = 1 is non-empty.)
+        expr_ref one(m_autil.mk_int(1), m);
+        expr_ref zero(m_autil.mk_int(0), m);
+        if (!u().str.is_string(lo) && hi_unit) {
+            // lo non-ground, hi unit: |lo| = 1 ∧ lo[0] ≤ ele ≤ c_hi
+            expr_ref lo_len1(m.mk_eq(u().str.mk_length(lo), one), m);
+            expr_ref lo_0(u().str.mk_nth_i(lo, zero), m);
+            expr_ref in_range(m.mk_and(lo_len1, m.mk_and(m_util.mk_le(lo_0, m_ele), m_util.mk_le(m_ele, c_hi))), m);
+            return mk_ite(in_range, eps, empty);
+        }
+        if (!u().str.is_string(hi) && lo_unit) {
+            // hi non-ground, lo unit: |hi| = 1 ∧ c_lo ≤ ele ≤ hi[0]
+            expr_ref hi_len1(m.mk_eq(u().str.mk_length(hi), one), m);
+            expr_ref hi_0(u().str.mk_nth_i(hi, zero), m);
+            expr_ref in_range(m.mk_and(hi_len1, m.mk_and(m_util.mk_le(c_lo, m_ele), m_util.mk_le(m_ele, hi_0))), m);
+            return mk_ite(in_range, eps, empty);
+        }
+        if (!u().str.is_string(lo) && !u().str.is_string(hi)) {
+            // both non-ground: |lo| = 1 ∧ |hi| = 1 ∧ lo[0] ≤ ele ≤ hi[0]
+            expr_ref lo_len1(m.mk_eq(u().str.mk_length(lo), one), m);
+            expr_ref hi_len1(m.mk_eq(u().str.mk_length(hi), one), m);
+            expr_ref lo_0(u().str.mk_nth_i(lo, zero), m);
+            expr_ref hi_0(u().str.mk_nth_i(hi, zero), m);
+            expr_ref in_range(m.mk_and(lo_len1, m.mk_and(hi_len1, m.mk_and(m_util.mk_le(lo_0, m_ele), m_util.mk_le(m_ele, hi_0)))), m);
+            return mk_ite(in_range, eps, empty);
+        }
+
         // Fallback: stuck derivative
         return expr_ref(re().mk_derivative(m_ele, re().mk_range(lo, hi)), m);
     }

src/ast/rewriter/seq_rewriter.cpp

@@ -4132,7 +4132,7 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
         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 +4140,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