diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 9892ffd35c..8bfe4bf96b 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -1567,5 +1567,66 @@ namespace seq {
         get_cofactors(m_ele, d, result);
     }
 
+    void derive::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
+        expr_ref_pair_vector brz(m);
+        derivative_cofactors(r, brz);
+
+        obj_map<expr, unsigned> target_index;
+        expr_ref_vector guards(m);
+        expr_ref_vector targets(m);
+
+        auto add = [&](expr* guard, expr* target) {
+            unsigned index = 0;
+            if (target_index.find(target, index)) {
+                expr_ref merged(m);
+                m_br.mk_or(guards.get(index), guard, merged);
+                guards.set(index, merged);
+            }
+            else {
+                target_index.insert(target, targets.size());
+                targets.push_back(target);
+                guards.push_back(guard);
+            }
+        };
+
+        for (auto const& [guard, target] : brz) {
+            ptr_vector<expr> pending;
+            pending.push_back(target);
+            while (!pending.empty()) {
+                expr* t = pending.back();
+                pending.pop_back();
+                expr* left = nullptr, * right = nullptr;
+                if (re().is_union(t, left, right)) {
+                    pending.push_back(right);
+                    pending.push_back(left);
+                }
+                else if (re().is_concat(t, left, right) && re().is_union(left)) {
+                    ptr_vector<expr> heads;
+                    heads.push_back(left);
+                    while (!heads.empty()) {
+                        expr* head = heads.back();
+                        heads.pop_back();
+                        expr* a = nullptr, * b = nullptr;
+                        if (re().is_union(head, a, b)) {
+                            heads.push_back(b);
+                            heads.push_back(a);
+                        }
+                        else {
+                            expr_ref split = m_re.mk_regex_concat(head, right);
+                            add(guard, split);
+                        }
+                    }
+                }
+                else {
+                    add(guard, t);
+                }
+            }
+        }
+
+        result.reset();
+        for (unsigned i = 0; i < targets.size(); ++i)
+            result.push_back(guards.get(i), targets.get(i));
+    }
+
 }
 
diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h
index e0559bdf1d..08e8631315 100644
--- a/src/ast/rewriter/seq_derive.h
+++ b/src/ast/rewriter/seq_derive.h
@@ -261,6 +261,25 @@ namespace seq {
          */
         void derivative_cofactors(expr* r, expr_ref_pair_vector& result);
 
+        /**
+         * Compute the Brzozowski cofactors of r (derivative_cofactors above),
+         * then expose the nondeterminism that a union leaf hides: a target of
+         * the form (s1 | ... | sn), or (s1 | ... | sn) . tail, is split into
+         * one cofactor per alternative si (resp. si . tail). Splitting is
+         * applied recursively, so nested unions are flattened as well.
+         *
+         * Splitting can make two originally distinct cofactors reach the same
+         * target; such cofactors are merged back into a single pair whose
+         * guard is the disjunction of the original guards. The result is
+         * therefore still a list of distinct targets, but each one is a
+         * single Antimirov-style alternative rather than a union state.
+         *
+         * The guards are not required to be mutually exclusive after merging,
+         * and the transition relation is genuinely nondeterministic: a
+         * character may be accepted by several of the returned guards.
+         */
+        void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result);
+
     };
 
 }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 508e2dea6d..6b71e47db5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2931,67 +2931,6 @@ expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
     return result;
 }
 
-void seq_rewriter::light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
-    expr_ref_pair_vector brz(m());
-    m_derive.derivative_cofactors(r, brz);
-
-    obj_map<expr, unsigned> target_index;
-    expr_ref_vector guards(m());
-    expr_ref_vector targets(m());
-
-    auto add = [&](expr* guard, expr* target) {
-        unsigned index = 0;
-        if (target_index.find(target, index)) {
-            expr_ref merged(m());
-            m_br.mk_or(guards.get(index), guard, merged);
-            guards.set(index, merged);
-        }
-        else {
-            target_index.insert(target, targets.size());
-            targets.push_back(target);
-            guards.push_back(guard);
-        }
-    };
-
-    for (auto const& [guard, target] : brz) {
-        ptr_vector<expr> pending;
-        pending.push_back(target);
-        while (!pending.empty()) {
-            expr* t = pending.back();
-            pending.pop_back();
-            expr* left = nullptr, * right = nullptr;
-            if (re().is_union(t, left, right)) {
-                pending.push_back(right);
-                pending.push_back(left);
-            }
-            else if (re().is_concat(t, left, right) && re().is_union(left)) {
-                ptr_vector<expr> heads;
-                heads.push_back(left);
-                while (!heads.empty()) {
-                    expr* head = heads.back();
-                    heads.pop_back();
-                    expr* a = nullptr, * b = nullptr;
-                    if (re().is_union(head, a, b)) {
-                        heads.push_back(b);
-                        heads.push_back(a);
-                    }
-                    else {
-                        expr_ref split = mk_regex_concat(head, right);
-                        add(guard, split);
-                    }
-                }
-            }
-            else {
-                add(guard, t);
-            }
-        }
-    }
-
-    result.reset();
-    for (unsigned i = 0; i < targets.size(); ++i)
-        result.push_back(guards.get(i), targets.get(i));
-}
-
 expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     expr_ref _r1(r1, m()), _r2(r2, m());
     expr *a1, *b1, *a2, *b2;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index c9c5ea989f..5bad5ae3dc 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -480,7 +480,9 @@ public:
     form (s1 | ... | sn) or (s1 | ... | sn) . tail. Cofactors with the same
     resulting target are merged by disjoining their guards.
     */
-    void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result);
+    void light_ant_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
+        m_derive.light_ant_derivative_cofactors(r, result);
+    }
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.