Push complement through union/intersection in symbolic derivative

The derivative's mk_complement_core left complement over a union/intersection
unfolded (e.g. d(comp(S*a)) = comp(S*a U eps)). Across successive derivatives
the complemented argument grew (comp(S*a U eps U ...)), giving every loop /
intersection state a fresh AST identity and defeating the state-graph dead-state
detection, so str.in_re emptiness on loop-intersect-comp regexes timed out.

Apply De Morgan in mk_complement_core so complement is pushed to the leaves:
  ~(A U B) -> ~A & ~B     (keeps ~A invariant; ~(S*a U eps) -> ~(S*a) & .+)
  ~(A & B) -> ~A U ~B     (exposes unions so antimirov non-emptiness can decide
                           each alternative separately)
This matches the form master's inline mk_derivative produces. z3test 5728 now
solves in 0.13s (was timeout) and parts of 5731/5721 are resolved. Full unit
suite: 92 passed.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/ast/rewriter/seq_derive.cpp

@@ -894,6 +894,20 @@ namespace seq {
             return expr_ref(re().mk_plus(re().mk_full_char(a->get_sort())), m);
         }
 
+        // De Morgan: push complement through union/intersection to the leaves
+        // so that complemented subterms stay invariant across successive
+        // derivatives and unions are exposed at the top.  This keeps the
+        // symbolic derivative in transition-regex normal form and lets the
+        // antimirov non-emptiness check decide each union alternative
+        // separately.  In particular ~(Σ*a ∪ ε) → ~(Σ*a) ∩ .+, so the ~(Σ*a)
+        // state is shared rather than growing into ~(Σ*a ∪ ε ∪ ...), which
+        // otherwise defeats dead-state detection on loop ∩ comp regexes.
+        expr* e1 = nullptr, *e2 = nullptr;
+        if (re().is_union(a, e1, e2))
+            return mk_inter(mk_complement(e1), mk_complement(e2));
+        if (re().is_intersection(a, e1, e2))
+            return mk_union(mk_complement(e1), mk_complement(e2));
+
         return expr_ref(re().mk_complement(a), m);
     }