diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d5f42cbbe9..508e2dea6d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4286,6 +4286,16 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         result = re().mk_star(re().mk_union(b1, c1));
         return BR_REWRITE2;
     }
+    // (Σ*·S)* = () | Σ*·S.
+    // Σ*·S is idempotent under concatenation: Σ*·S·Σ*·S = (Σ*·S·Σ*)·S ⊆ Σ*·S,
+    // since any prefix is absorbed by Σ*. Hence L·L ⊆ L and L* = () | L.
+    // Keeping the flat form avoids a large blowup in the derivative automaton.
+    if (re().is_concat(a, b, c) && re().is_full_seq(b)) {
+        sort* seq_sort = nullptr;
+        VERIFY(m_util.is_re(a, seq_sort));
+        result = re().mk_union(re().mk_epsilon(seq_sort), a);
+        return BR_REWRITE1;
+    }
     if (m().is_ite(a, c, b1, c1)) {
         if ((re().is_full_char(b1) || re().is_full_seq(b1)) &&
             (re().is_full_char(c1) || re().is_full_seq(c1))) {
diff --git a/src/test/seq_monadic_bench.cpp b/src/test/seq_monadic_bench.cpp
index ed56846553..09fca17cec 100644
--- a/src/test/seq_monadic_bench.cpp
+++ b/src/test/seq_monadic_bench.cpp
@@ -25,6 +25,7 @@ Abstract:
 #include "ast/arith_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/seq_monadic.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
@@ -100,6 +101,7 @@ lbool run_file(
     seq_util u(m);
     arith_util a(m);
     seq_rewriter rw(m);
+    th_rewriter trw(m);
     trail_stack undo_trail;
     seq_monadic mon(rw, undo_trail, mode);
 
@@ -197,6 +199,13 @@ lbool run_file(
             return;
         }
         obj_map<expr, expr*>& map = is_var ? var_re : term_re;
+        // Normalize the regex the way asserted_formulas normalizes assertions
+        // before seq_regex hands them to seq_monadic. Without this the bench
+        // measures raw parsed regexes, which no production path ever sees.
+        expr_ref normalized(r, m);
+        trw(normalized);
+        pin.push_back(normalized);
+        r = normalized;
         expr* previous = nullptr;
         if (map.find(s, previous)) {
             expr_ref intersection = rw.mk_regex_inter_normalize(previous, r);
diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp
index 9557b9cfc6..55c318aa86 100644
--- a/src/test/seq_rewriter.cpp
+++ b/src/test/seq_rewriter.cpp
@@ -16,6 +16,7 @@ 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
 --*/
 
 #include "ast/arith_decl_plugin.h"
@@ -276,7 +277,33 @@ void tst_seq_rewriter() {
             ENSURE(res == l_true);
         }
 
-        // 20. unsat: contradictory constant lexical bounds.
+        // 22. (Σ*·S)* is rewritten to the flat form () | Σ*·S.
+        //     Σ*·S is idempotent under concatenation — Σ*·S·Σ*·S = (Σ*·S·Σ*)·S
+        //     is again of the form Σ*·S — so its Kleene star contributes
+        //     nothing beyond the empty word. The star form is exponentially
+        //     more expensive to determinize, so the flat form is kept.
+        {
+            expr_ref sigma_star(su.re.mk_full_seq(re_sort), m);
+            expr_ref b_re(su.re.mk_to_re(su.str.mk_string(zstring('b'))), m);
+            expr_ref star(su.re.mk_star(su.re.mk_concat(sigma_star, b_re)), m);
+            expr_ref e(star);
+            rw(e);
+            std::cout << "(sigma* b)* flattened: " << mk_pp(e, m) << "\n";
+            ENSURE(!su.re.is_star(e));
+
+            // Semantics: L* = words ending in "b", plus the empty word.
+            auto member = [&](char const* w) {
+                smt_params sp;
+                smt::context ctx(m, sp);
+                ctx.assert_expr(su.re.mk_in_re(su.str.mk_string(w), star));
+                return ctx.check();
+            };
+            ENSURE(member("ab") == l_true);
+            ENSURE(member("") == l_true);
+            ENSURE(member("ba") == l_false);
+        }
+
+
         //     "2024-01-01" < x < "2024-12-31" and x < "2023-01-01".
         //     Since "2023-01-01" < "2024-01-01", no such x exists.
         if (false)