From 9ac438b199134b9e843d4099874f5b31ed519eb1 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 22 Jul 2026 10:30:45 -0700
Subject: [PATCH] Fix nested symbolic re.range under re.++ ignoring solver
 timeout (#10181)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Symbolic `re.range` nested under `re.++` caused Z3 to loop indefinitely,
ignoring timeouts. Direct symbolic range membership was fixed
previously, but the nested case reaches a different code path — the
Brzozowski derivative engine in `derive_range`.

## Root cause

`derive_range` in `seq_derive.cpp` only handled concrete unit-string
bounds. For symbolic bounds it returned a stuck `re.derivative(ele,
re.range(lo, hi))` term. When nested under concatenation, this stuck
term cycled infinitely:

1. `is_nullable` of the stuck term → `is_nullable_symbolic_regex` →
emits `re.in_re("", re.derivative(...))`
2. That `in_re` triggers `propagate_in_re` → new `accept` predicate
3. New `accept` computes another derivative → another stuck term →
repeat

## Fix

Replace the stuck fallback with a proper symbolic ITE. By SMT-LIB
semantics, `re.range(lo, hi)` accepts character `c` iff both bounds are
single-character strings and `lo[0] ≤ c ≤ hi[0]`. The derivative with
respect to `ele` becomes:

```
ite(len(lo)=1 ∧ len(hi)=1 ∧ lo[0] ≤ ele ∧ ele ≤ hi[0], ε, ∅)
```

Length conditions are omitted for bounds already known to be concrete
single-character strings.

```smt2
(set-logic ALL)
(declare-const s String)
(assert (str.in_re "a" (re.++ re.all (re.range s "c"))))
(check-sat)
; Previously hung indefinitely; now returns sat in ~10ms
```

## Changes

- **`src/ast/rewriter/seq_derive.cpp`** — `derive_range`: replace stuck
`re.derivative` fallback with symbolic ITE using `str.nth_i` and length
guards for non-concrete bounds
- **`src/test/seq_rewriter.cpp`** — add solver-level regression test
(case 21) for nested symbolic `re.range` under `re.++`

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/seq_derive.cpp | 22 ++++++++++++++++++++--
 src/test/seq_rewriter.cpp       | 20 ++++++++++++++++++++
 2 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index f0cd0aee9f..f84546282b 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -421,8 +421,26 @@ namespace seq {
             return mk_ite(in_range, eps, empty);
         }
 
-        // Fallback: stuck derivative
-        return expr_ref(re().mk_derivative(m_ele, re().mk_range(lo, hi)), m);
+        // One or both bounds are symbolic.  By SMT-LIB semantics re.range(lo,hi)
+        // accepts a single character c iff lo and hi are both single-character
+        // strings and lo[0] <= c <= hi[0].  Build the symbolic derivative
+        //   ite(len(lo)=1 ∧ len(hi)=1 ∧ lo[0] ≤ ele ∧ ele ≤ hi[0], ε, ∅)
+        // omitting length conditions for bounds that are already known to be
+        // concrete single-character strings.
+        expr_ref_vector conds(m);
+        expr_ref zero(m_autil.mk_int(0), m);
+        if (!u().str.is_unit_string(lo, c_lo)) {
+            conds.push_back(m.mk_eq(u().str.mk_length(lo), m_autil.mk_int(1)));
+            c_lo = u().str.mk_nth_i(lo, zero);
+        }
+        if (!u().str.is_unit_string(hi, c_hi)) {
+            conds.push_back(m.mk_eq(u().str.mk_length(hi), m_autil.mk_int(1)));
+            c_hi = u().str.mk_nth_i(hi, zero);
+        }
+        conds.push_back(m_util.mk_le(c_lo, m_ele));
+        conds.push_back(m_util.mk_le(m_ele, c_hi));
+        expr_ref in_range = m_br.mk_and(conds);
+        return mk_ite(in_range, eps, empty);
     }
 
     expr_ref derive::derive_of_pred(expr* pred, sort* seq_sort) {
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index 78290199c1..84facb37e4 100644
--- a/src/test/seq_rewriter.cpp
+++ b/src/test/seq_rewriter.cpp
@@ -325,6 +325,26 @@ void tst_seq_rewriter() {
             ENSURE(res == l_false);
         }
 
+        // 21. sat: (str.in_re "a" (re.++ re.all (re.range s "c")))
+        //     Regression for nested symbolic re.range under re.++.
+        //     The string "a" satisfies the regex when s = "a":
+        //     re.all matches "" and re.range "a" "c" accepts "a".
+        //     This must not hang; it should return sat.
+        {
+            smt_params sp;
+            smt::context ctx(m, sp);
+            app_ref s(m.mk_fresh_const("s", str_sort), m);
+            expr_ref a_str(su.str.mk_string(zstring('a')), m);
+            expr_ref c_str(su.str.mk_string(zstring('c')), m);
+            expr_ref re_all(su.re.mk_full_seq(re_sort), m);
+            expr_ref re_range(su.re.mk_range(s, c_str), m);
+            expr_ref regex(su.re.mk_concat(re_all, re_range), m);
+            ctx.assert_expr(su.re.mk_in_re(a_str, regex));
+            lbool res = ctx.check();
+            std::cout << "nested symbolic re.range under re.++ sat: " << res << "\n";
+            ENSURE(res == l_true);
+        }
+
         // 20. unsat: contradictory constant lexical bounds.
         //     "2024-01-01" < x < "2024-12-31" and x < "2023-01-01".
         //     Since "2023-01-01" < "2024-01-01", no such x exists.