diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 8bfe4bf96b..39f2ea2a44 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/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);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index d0f45485dd..36310fd3c3 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/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;
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index 55c318aa86..ebfdb09e11 100644
--- a/src/test/seq_rewriter.cpp
+++ b/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";
 }