diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 2101223b4..7b7d3fca9 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -725,11 +725,9 @@ namespace seq {
     expr_ref derive::merge_union(expr* r1, expr* r2) {
         expr_ref _r1(r1, m), _r2(r2, m);
 
-        if (r1 == r2) return expr_ref(r1, m);
-        if (re().is_empty(r1)) return expr_ref(r2, m);
-        if (re().is_empty(r2)) return expr_ref(r1, m);
-        if (re().is_full_seq(r1)) return expr_ref(r1, m);
-        if (re().is_full_seq(r2)) return expr_ref(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
@@ -811,8 +809,7 @@ namespace seq {
 
     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)
-        expr *c1, *t1, *e1, *c2, *t2, *e2;
-        if (m.is_ite(a, c1, t1, e1) || m.is_ite(b, c2, t2, e2)) {
+        if (m.is_ite(a) || m.is_ite(b)) {
             // Canonical order for non-ITE cases handled by merge below
             auto union_op = [&](expr* x, expr* y) { return mk_union(x, y); };
             expr_ref r = hoist_ite(a, b, union_op);
@@ -849,7 +846,6 @@ namespace seq {
     }
 
     expr_ref derive::mk_inter_core(expr* a, expr* b) {
-        // Canonical order: smaller id first
         if (a->get_id() > b->get_id())
             std::swap(a, b);
 
@@ -1136,6 +1132,8 @@ namespace seq {
     // Returns nullptr if neither a nor b is ITE (or depth limit reached).
     expr_ref derive::hoist_ite(expr* a, expr* b, std::function<expr_ref(expr*, expr*)> apply_op) {
         expr *c1, *t1, *e1, *c2, *t2, *e2;
+        if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2) && c1->get_id() > c2->get_id()) 
+            std::swap(a, b);
         if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2)) {
             expr_ref r(m);
             if (c1 == c2)
@@ -1401,4 +1399,4 @@ namespace seq {
         m_intervals_start = old_sz;
     }
 
-}
\ No newline at end of file
+}