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.