[snapshot-regression-fix] seq_rewriter: re.range with a provably-empty bound must be the empty language (#10047)

## Summary

Fixes a Z3 output regression detected by the `Z3Prover/bench`
snapshot-regression corpus.

- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/3050
- **Benchmark:** `iss-5134/small.smt2`
(`inputs/issues/iss-5134/small.smt2` in `Z3Prover/bench`)
- **Kind:** `diff` — recorded oracle vs. current nightly z3
(`z3-4.17.0-x64-glibc-2.39`)

## Divergence

The benchmark constrains a string `a` using a regex that contains
`(re.range "" <ite>)`:

```smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (re.union (str.to_re "b") (str.to_re (ite
 (str.in_re a (re.* (re.range "" (ite (str.in_re a (str.to_re "")) ""
 a)))) "" "a"))))))
(assert (not (str.in_re a (re.* (str.to_re "")))))
(check-sat)
(get-model)
```

Recorded oracle (**expected**) vs. current z3 (**current**):

```diff
-sat
-(
-  (define-fun a () String
-    "a")
-)
+unknown
+(error "line 7 column 10: model is not available")
```

## Root cause

Per SMT-LIB, `re.range` over an argument that is **not a single
character** denotes the empty language, so `(re.range "" X)` is
`re.none` regardless of `X` (the lower bound `""` is the empty string).

Before the *"Derive with ranges"* refactor (#9963 / #9965),
`seq_rewriter::mk_re_range` recognised this through several emptiness
checks, including a concrete non-single-character test and a `max_length
== 0` test:

```cpp
if (str().is_string(lo, slo) && slo.length() != 1) is_empty = true;
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;
```

The refactor rewrote `mk_re_range` and kept only the `min_length(..) >
1` emptiness test (a bound provably **≥ 2** characters). That misses a
bound of length **exactly 0**: an empty-string bound has `min_length ==
0`, so it is no longer detected as empty, and `mk_re_range` returns
`BR_FAILED`, leaving `(re.range "" X)` symbolic. The new range-aware
derivative engine (`seq_derive.cpp`) then produces a *stuck* derivative
for such a range (its `is_unit_string("")` test fails), so the sequence
theory can no longer decide membership and the solver answers `unknown`
/ "model is not available".

## Fix

Restore the sound emptiness check the refactor dropped — a bound whose
`max_length` is provably `0` can never be a single character, so the
range is empty:

```cpp
// 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;
```

This does **not** reintroduce the unsoundness the refactor guarded
against: `max_length == (true, 0)` is a *provable* emptiness fact and is
never true for a model-dependent (symbolic) bound, so `(re.range x x)`
is still correctly left symbolic (it denotes `{x}` whenever `x` is a
single character).

## Validation

Built the patched `./z3` checkout (`./configure && make -C build`) and
re-ran the benchmark with the option the snapshot capture uses
(`-T:20`):

- **Before the fix:** `z3 -T:20 small.smt2` → `unknown` + `(error "...
model is not available")` — reproduces the divergence.
- **After the fix:** `z3 -T:20 small.smt2` → `sat` + `(define-fun a ()
String "a")` — **exactly matches** the recorded oracle.

Additional checks with the rebuilt binary:
- Sibling benchmarks `iss-5134/bug.smt2` and `iss-5134/small-2.smt2`
still match their oracles.
- Symbolic bound not over-collapsed: `(str.in_re "a" (re.range x x))` →
`sat` (x = "a").
- `(re.range "" "a")` is the empty language: `(str.in_re "a" (re.range
"" "a"))` and `(str.in_re "" (re.range "" "a"))` → `unsat`.
- Ordinary ranges unaffected: `"b" ∈ (re.range "a" "c")` sat, `"d" ∈
(re.range "a" "c")` unsat, `(re.range "a" "a")` singleton.




> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28731229299)
· 592.3 AIC · ⌖ 39.1 AIC · ⊞ 8.9K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.63, model: claude-opus-4.8, id:
28731229299, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28731229299 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

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

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