fix unsound regex info for the legacy argument form of re.loop (#10370)

`re.loop` has two accepted AST forms: bounds as decl parameters, `((_
re.loop lo hi) r)` (1 argument, 2 parameters), and bounds as arguments,
`(re.loop r lo hi)` (3 arguments, 0 parameters). The plugin accepts
arities 1, 2 and 3, and `is_loop` has separate overloads for each form.
Only the parameter form was recognized downstream.

### The soundness bug

`mk_info_rec`'s `OP_RE_LOOP` case read the bounds solely from
`get_decl()->get_num_parameters()`, which is 0 for the argument form, so
it silently fell back to the locals `lower_bound = 0, upper_bound =
UINT_MAX`. `info::loop` computes

```cpp
loop_nullable = (nullable == l_true || lower == 0) ? l_true : nullable;
```

so `lower == 0` forces nullability, and `min_length` collapses to
`min_length * 0 = 0`.

Net effect: `(re.loop (str.to_re "ab") 1 3)` was reported as `nullable =
l_true, min_length = 0`. At the SMT level

```smt2
(declare-const x String)
(assert (str.in_re x (re.loop (str.to_re "ab") 1 3)))
(assert (= (str.len x) 0))
(check-sat)
```

answered **sat** rather than unsat. The indexed form of the same regex
correctly answers unsat.

`seq_rewriter::mk_re_loop` already normalizes the argument form to
`mk_loop_proper`, which is why this was never observable on the usual
paths — it only surfaces where the rewriter is bypassed, as in
`seq_monadic`. The `info.nullable` fast path added in #10366 didn't
create the bug but widened the path that reaches it.

### The performance bug

`derive_core` had no case for the argument form either, so the
derivative got stuck as an uninterpreted `re.derivative` term.
Instrumenting all three sites that can emit a symbolic `re.derivative`
showed that **every one of the 4171 stuck terms** in the regex corpus
came from this fall-through (the 512-deep recursion cap and the
unnormalizable `re.reverse` site never fired), and 4096 of them came
from a single legacy-form loop, whose search then burned its full budget
before giving up.

### The fix

* `mk_info_rec` branches on `get_num_args()`; for the argument form it
reads the bounds from `get_arg(1)`/`get_arg(2)` when they are unsigned
numerals, and returns `unknown_info` when they are not.
* `derive_core` normalizes the numeral argument forms to
`mk_loop_proper`/`mk_loop` and recurses. The block is gated on the cheap
`re().is_loop(r)` kind check so that regexes falling through to the
later cases don't pay for the `rational` locals.

Arguably the right long-term place to normalize is the parser, so the
legacy form never reaches the AST at all. Keeping the `mk_info_rec` half
is still worthwhile as a guard for API-constructed terms, and the
regression test builds the term directly via `mk_app`, so it stays
meaningful either way.

### Regression test

`src/test/seq_rewriter.cpp` gains a case asserting that `get_info`
agrees on the two forms (`nullable == l_false`, `min_length == 2`).
Verified to actually catch the bug: reverting `seq_decl_plugin.cpp` and
rebuilding gives `ASSERTION VIOLATION` with `nullable=l_true
min_length=0`.

### Evaluation

Full run over 1545 regex benchmarks with declared statuses, in both
transition modes:

| | light-ant | brz |
|---|---|---|
| decided (before → after) | 1462 → **1463** | 1464 → **1465** |
| soundness mismatches | 0 → 0 | 0 → 0 |
| verdict changes | 1 | 1 (same file) |

The one changed file is `L4-01-loop-sat.smt2`: **undef @ 8625 ms → sat @
0.20 ms**. The corpus contains 1 legacy-form file and 236 indexed-form
files, which share the modified `OP_RE_LOOP` path, hence the full A/B
rather than a spot check.

Timing is neutral. Measured with an interleaved base/fix/base/fix
protocol over two saved binaries, since same-binary run-to-run variance
(±8%) turned out to exceed the effect: paired best-of-2 over the 315
files taking >1 ms gives a **median ratio of 0.998** (p25/p75 =
0.889/1.075), overall 0.976.

`tst_seq_rewriter` passes, `seq_monadic` is ALL PASS in both modes, and
the 22172-file QF_S corpus shows no verdict changes and no mismatches.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2

src/ast/rewriter/seq_derive.cpp

@@ -288,6 +288,22 @@ namespace seq {
             return mk_deriv_concat(d1, tail);
         }
 
+        // Legacy form where the loop bounds are arguments rather than
+        // decl parameters: (re.loop r lo hi) and (re.loop r lo).  The parser
+        // accepts these and seq_rewriter normalizes them, but unrewritten
+        // terms reach here directly.  Rewrite to the parameterized form.
+        if (re().is_loop(r)) {
+            expr* lo_e = nullptr, * hi_e = nullptr;
+            rational nlo, nhi;
+            if (re().is_loop(r, r1, lo_e, hi_e) &&
+                m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned() &&
+                m_autil.is_numeral(hi_e, nhi) && nhi.is_unsigned())
+                return derive_rec(re().mk_loop_proper(r1, nlo.get_unsigned(), nhi.get_unsigned()));
+            if (re().is_loop(r, r1, lo_e) &&
+                m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned())
+                return derive_rec(re().mk_loop(r1, nlo.get_unsigned()));
+        }
+
         // δ(r1 \ r2) = δ(r1) ∩ ~δ(r2)
         if (re().is_diff(r, r1, r2)) {
             expr_ref d1 = derive_rec(r1);

src/ast/seq_decl_plugin.cpp

@@ -1733,11 +1733,30 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
             return i1.complement();
         case OP_RE_LOOP:
             i1 = get_info_rec(e->get_arg(0));
-            if (e->get_decl()->get_num_parameters() >= 1)
-                lower_bound = e->get_decl()->get_parameter(0).get_int();
-            if (e->get_decl()->get_num_parameters() == 2)
-                upper_bound = e->get_decl()->get_parameter(1).get_int();
-            return i1.loop(lower_bound, upper_bound);
+            if (e->get_num_args() == 1) {
+                if (e->get_decl()->get_num_parameters() >= 1)
+                    lower_bound = e->get_decl()->get_parameter(0).get_int();
+                if (e->get_decl()->get_num_parameters() == 2)
+                    upper_bound = e->get_decl()->get_parameter(1).get_int();
+                return i1.loop(lower_bound, upper_bound);
+            }
+            else {
+                // legacy form carrying the bounds as arguments:
+                // (re.loop r lo) and (re.loop r lo hi)
+                arith_util autil(m);
+                rational n;
+                if (e->get_num_args() != 2 && e->get_num_args() != 3)
+                    return unknown_info;
+                if (!autil.is_numeral(e->get_arg(1), n) || !n.is_unsigned())
+                    return unknown_info;
+                lower_bound = n.get_unsigned();
+                if (e->get_num_args() == 3) {
+                    if (!autil.is_numeral(e->get_arg(2), n) || !n.is_unsigned())
+                        return unknown_info;
+                    upper_bound = n.get_unsigned();
+                }
+                return i1.loop(lower_bound, upper_bound);
+            }
         case OP_RE_DIFF:
             if (e->get_num_args() != 2)
                 return unknown_info;

src/test/seq_rewriter.cpp

@@ -16,7 +16,8 @@ Tests:
  18. Solver: (str.in_re x (re.range x x)) unsat when len(x)=2
  19. Solver: inverted symbolic bounds make membership unsatisfiable
  20. Solver: contradictory constant lexical bounds are unsatisfiable
- 22. (Σ*·S)* is flattened to () | Σ*·S
+ 22. re.loop with bounds as arguments agrees with the indexed form
+ 23. (Σ*·S)* is flattened to () | Σ*·S
 --*/
 
 #include "ast/arith_decl_plugin.h"
@@ -323,5 +324,30 @@ void tst_seq_rewriter() {
         }
     }
 
+    // -----------------------------------------------------------------------
+    // 22. re.loop with the bounds given as arguments must be interpreted the
+    //     same as the indexed form.  get_info used to read the bounds only
+    //     from the decl parameters, which the argument form does not carry,
+    //     so it silently fell back to lo = 0 and reported (ab){1,3} as
+    //     nullable with min_length 0.  seq_rewriter normalizes the argument
+    //     form, so this is only observable on paths that bypass it.
+    // -----------------------------------------------------------------------
+    {
+        arith_util a_util(m);
+        expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m);
+        expr_ref indexed(su.re.mk_loop_proper(ab, 1, 3), m);
+        expr* args[3] = { ab.get(), a_util.mk_int(1), a_util.mk_int(3) };
+        expr_ref as_args(m.mk_app(su.get_family_id(), OP_RE_LOOP, 0, nullptr, 3, args), m);
+
+        auto i1 = su.re.get_info(indexed);
+        auto i2 = su.re.get_info(as_args);
+        std::cout << "re.loop indexed:   " << mk_pp(indexed, m)
+                  << " nullable=" << i1.nullable << " min_length=" << i1.min_length << "\n";
+        std::cout << "re.loop arguments: " << mk_pp(as_args, m)
+                  << " nullable=" << i2.nullable << " min_length=" << i2.min_length << "\n";
+        ENSURE(i1.nullable == l_false && i1.min_length == 2);
+        ENSURE(i2.nullable == l_false && i2.min_length == 2);
+    }
+
     std::cout << "tst_seq_rewriter: all tests passed\n";
 }