diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 64248fa2ca..f99abb382f 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -189,6 +189,18 @@ namespace seq {
 
         // δ(r1 · r2) = δ(r1) · r2 ∪ (if nullable(r1) then δ(r2) else ∅)
         if (re().is_concat(r, r1, r2)) {
+            // Ensure right-associative form first.  A left-nested concat
+            // (a·b)·r2 makes the head r1 a large sub-concat, so deriving it
+            // recurses through the whole left spine and can exceed
+            // m_max_depth, producing stuck symbolic re.derivative terms that
+            // accumulate across states and blow up.  mk_concat right-
+            // associates in a single linear pass (without touching the
+            // derivative depth counter), keeping the head atomic.
+            if (re().is_concat(r1)) {
+                expr_ref rr = mk_concat(r1, r2);
+                if (rr != r)
+                    return derive_rec(rr);
+            }
             expr_ref d1 = derive_rec(r1);
             expr_ref d1_r2 = mk_deriv_concat(d1, r2);
             expr_ref nullable_r1 = is_nullable(r1);
@@ -748,6 +760,13 @@ namespace seq {
             return mk_deriv_concat(a1, tail);
         }
 
+        // Subsumption: L(a) ⊆ L(b) ⇒ a ∪ b = b (and symmetrically).
+        // This collapses semantically-equal union states that arise in
+        // antimirov intersection derivatives, which is essential to keep the
+        // emptiness/bisim worklist from blowing up on contains-patterns.
+        if (is_subset(a, b)) return expr_ref(b, m);
+        if (is_subset(b, a)) return expr_ref(a, m);
+
         return m_re.mk_union(a, b);
     }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index fe932ec782..774664c097 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3969,10 +3969,10 @@ expr_ref seq_rewriter::mk_regex_concat(expr *r, expr *s) {
         result = r;
     else if (re().is_full_char(r) && re().is_full_seq(s))
         // ..* = .+
-        result = re().mk_plus(re().mk_full_char(ele_sort));
+        result = re().mk_plus(re().mk_full_char(r->get_sort()));
     else if (re().is_full_seq(r) && re().is_full_char(s))
         // .*. = .+
-        result = re().mk_plus(re().mk_full_char(ele_sort));
+        result = re().mk_plus(re().mk_full_char(r->get_sort()));
     else if (re().is_concat(r, r1, r2))
         // create the resulting concatenation in right-associative form except for the following case
         // TODO: maintain the following invariant for A ++ B{m,n} + C