diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index dae3670a9..ea374d6c3 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -453,7 +453,7 @@ namespace seq {
         if (re().is_intersection(r, r1, r2)) {
             expr_ref a(re().mk_reverse(r1), m);
             expr_ref b(re().mk_reverse(r2), m);
-            return expr_ref(re().mk_inter(a, b), m);
+            return m_re.mk_inter(a, b);
         }
 
         // reverse(r1 \ r2) = reverse(r1) \ reverse(r2)
@@ -607,49 +607,7 @@ namespace seq {
 
     // Lightweight structural subsumption: checks if L(a) ⊆ L(b)
     bool derive::is_subset(expr* a, expr* b) {
-        if (a == b) return true;
-        if (re().is_empty(a)) return true;
-        if (re().is_full_seq(a)) return re().is_full_seq(b);
-        if (re().is_full_seq(b)) return true;
-
-        expr* b1 = nullptr;
-        if (re().is_plus(b, b1) && re().is_full_char(b1) &&
-            re().get_info(a).nullable == l_false)
-            return true;
-
-        if (re().is_star(b, b1) && a == b1) return true;
-
-        expr* a1 = nullptr;
-        if (re().is_star(a, a1) && re().is_star(b, b1) && is_subset(a1, b1)) return true;
-
-        if (re().is_union(b, b1, a1)) {
-            if (is_subset(a, b1) || is_subset(a, a1)) return true;
-        }
-        if (re().is_union(a, a1, b1)) {
-            if (is_subset(a1, b) && is_subset(b1, b)) return true;
-        }
-        if (re().is_intersection(a, a1, b1)) {
-            if (is_subset(a1, b) || is_subset(b1, b)) return true;
-        }
-        if (re().is_intersection(b, b1, a1)) {
-            if (is_subset(a, b1) && is_subset(a, a1)) return true;
-        }
-
-        expr* a2 = nullptr, * b2 = nullptr;
-        if (re().is_concat(a, a1, a2) && re().is_concat(b, b1, b2) &&
-            is_subset(a1, b1) && is_subset(a2, b2))
-            return true;
-
-        // loop subsumption: r{la,ua} ⊆ r{lb,ub} when lb <= la and ua <= ub
-        unsigned la, ua, lb, ub;
-        if (re().is_loop(a, a1, la, ua) && re().is_loop(b, b1, lb, ub) &&
-            a1 == b1 && lb <= la && ua <= ub)
-            return true;
-
-        if (re().is_complement(a, a1) && re().is_complement(b, b1))
-            return is_subset(b1, a1);
-
-        return false;
+        return m_re.is_subset(a, b);
     }
 
     unsigned derive::union_id(expr* e) {
@@ -662,94 +620,7 @@ namespace seq {
         if (re().is_complement(a, c) && c == b) return true;
         if (re().is_complement(b, c) && c == a) return true;
         return false;
-    }
-
-    // Merge two sorted right-associated union chains.
-    // Uses is_subset for pairwise subsumption during merge.
-    expr_ref derive::merge_union(expr* r1, expr* r2) {
-        expr_ref _r1(r1, m), _r2(r2, m);
-
-        if (is_subset(r1, r2)) return expr_ref(r2, m);
-        if (is_subset(r2, r1)) return expr_ref(r1, m);
-
-        if (are_complements(r1, r2)) return expr_ref(re().mk_full_seq(r1->get_sort()), m);
-
-        // Flatten both chains into a vector, merge-sort style
-        expr_ref_vector elems(m);
-        auto collect = [&](expr* r) {
-            expr* a, *b;
-            while (re().is_union(r, a, b)) {
-                elems.push_back(a);
-                r = b;
-            }
-            elems.push_back(r);
-        };
-        unsigned split;
-        collect(r1);
-        split = elems.size();
-        collect(r2);
-
-        // Merge pass: produce sorted result with subsumption
-        expr_ref_vector result_elems(m);
-        unsigned i = 0, j = split;
-        while (i < split && j < elems.size()) {
-            expr* a = elems.get(i);
-            expr* b = elems.get(j);
-            if (a == b) {
-                result_elems.push_back(a);
-                ++i; ++j;
-            } else if (are_complements(a, b)) {
-                return expr_ref(re().mk_full_seq(r1->get_sort()), m);
-            } else {
-                unsigned aid = union_id(a), bid = union_id(b);
-                if (aid == bid) {
-                    // Same union_id: check subsumption
-                    if (is_subset(a, b))
-                        result_elems.push_back(b);
-                    else if (is_subset(b, a))
-                        result_elems.push_back(a);
-                    else {
-                        result_elems.push_back(a);
-                        result_elems.push_back(b);
-                    }
-                    ++i; ++j;
-                } else if (aid < bid) {
-                    result_elems.push_back(a);
-                    ++i;
-                } else {
-                    result_elems.push_back(b);
-                    ++j;
-                }
-            }
-        }
-        while (i < split) result_elems.push_back(elems.get(i++));
-        while (j < elems.size()) result_elems.push_back(elems.get(j++));
-
-        // Subsumption pass: check each element against its neighbors
-        // This catches cases like loop(0,k)·star ⊆ loop(0,k+1)·star
-        // which have different union_ids
-        unsigned n = result_elems.size();
-        svector<bool> removed(n, false);
-        for (unsigned k = 0; k + 1 < n; ++k) {
-            if (removed[k]) continue;
-            if (is_subset(result_elems.get(k), result_elems.get(k + 1))) {
-                removed[k] = true;
-            } else if (is_subset(result_elems.get(k + 1), result_elems.get(k))) {
-                removed[k + 1] = true;
-            }
-        }
-
-        // Build right-associated chain from result
-        expr_ref result(m);
-        for (unsigned k = n; k-- > 0; ) {
-            if (removed[k]) continue;
-            if (!result)
-                result = expr_ref(result_elems.get(k), m);
-            else
-                result = expr_ref(re().mk_union(result_elems.get(k), result.get()), m);
-        }
-        return result ? result : expr_ref(re().mk_empty(r1->get_sort()), m);
-    }
+    }    
 
     expr_ref derive::mk_union_core(expr* a, expr* b) {
         // ITE handling with path pruning (before merge, since ITEs aren't part of sorted chains)
@@ -767,8 +638,7 @@ namespace seq {
             return mk_deriv_concat(a1, tail);
         }
 
-        // Merge-based normalization: merge two sorted right-associated union chains
-        return merge_union(a, b);
+        return m_re.mk_union(a, b);
     }
 
     expr_ref derive::mk_inter(expr* a, expr* b) {
@@ -798,11 +668,13 @@ namespace seq {
         if (is_subset(b, a)) return expr_ref(b, m);
 
         // Complement absorption: r ∩ ~r = ∅
-        expr* c = nullptr;
+        expr *c = nullptr, *d = nullptr;
         if (re().is_complement(a, c) && c == b)
             return expr_ref(re().mk_empty(a->get_sort()), m);
         if (re().is_complement(b, c) && c == a)
             return expr_ref(re().mk_empty(a->get_sort()), m);
+        if (re().is_complement(a, c) && re().is_complement(b, d))
+            return expr_ref(re().mk_complement(mk_union_core(c, d)), m);
 
         // ITE handling with path pruning
         auto inter_op = [&](expr* x, expr* y) { return mk_inter(x, y); };
@@ -818,9 +690,10 @@ namespace seq {
         //     return mk_union(mk_inter(a, u1), mk_inter(a, u2));
 
         // Base case: build raw intersection
-        return expr_ref(re().mk_inter(a, b), m);
+        return m_re.mk_inter(a, b);
     }
 
+
     expr_ref derive::mk_concat(expr* a, expr* b) {
         if (re().is_empty(a)) return expr_ref(a, m);
         if (re().is_empty(b)) return expr_ref(b, m);
diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h
index 17285962f..0c981d52f 100644
--- a/src/ast/rewriter/seq_derive.h
+++ b/src/ast/rewriter/seq_derive.h
@@ -128,13 +128,12 @@ namespace seq {
 
         // Smart constructors with path-aware simplification and ACI canonicalization
         expr_ref mk_union(expr* a, expr* b);
-        expr_ref merge_union(expr* a, expr* b);  // merge two sorted right-associated union chains
         bool are_complements(expr* a, expr* b);
         unsigned union_id(expr* e);              // complement-aware ID for sorting
         bool is_subset(expr* a, expr* b);
-        expr_ref mk_union_core(expr* a, expr* b);
+        expr_ref mk_union_core(expr* a, expr* b); 
         expr_ref mk_inter(expr* a, expr* b);
-        expr_ref mk_inter_core(expr* a, expr* b);
+        expr_ref mk_inter_core(expr* a, expr* b); 
         expr_ref mk_concat(expr* a, expr* b);
         expr_ref mk_complement(expr* a);
         expr_ref mk_complement_core(expr* a);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 8af435f09..08c7887ee 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2914,11 +2914,16 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) {
 #endif
 
 expr_ref seq_rewriter::mk_derivative(expr* r) {
-    return m_derive(r);
+    auto result = m_derive(r);
+    TRACE(seq, tout << "Derivative of " << mk_pp(r, m()) << "\nis\n" << result << std::endl;);
+    return result;
 }
 
 expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
-    return m_derive(ele, r);
+    auto result = m_derive(ele, r);
+    TRACE(seq,
+          tout << "Derivative of " << mk_pp(r, m()) << " w.r.t. " << mk_pp(ele, m()) << "\nis\n" << result << std::endl;);
+    return result;
 }
 
 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 33b1462e8..30134d1cd 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -365,6 +365,27 @@ public:
         return result;
     }
 
+    expr_ref mk_union(expr *a, expr *b) {
+        expr_ref result(m());
+        if (mk_re_union(a, b, result) == BR_FAILED)
+            result = re().mk_union(a, b);
+        return result;
+    }
+
+    expr_ref mk_inter(expr *a, expr *b) {
+        expr_ref result(m());
+        if (mk_re_inter(a, b, result) == BR_FAILED)
+            result = re().mk_inter(a, b);
+        return result;
+    }
+
+    expr_ref mk_complement(expr *a) {
+        expr_ref result(m());
+        if (mk_re_complement(a, result) == BR_FAILED)
+            result = re().mk_complement(a);
+        return result;
+    }
+
     /*
     * makes concat and simplifies
     */