diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index a74030301..294967576 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -38,8 +38,8 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r
             if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) ||
                 r.is_empty(p1.m_n) || r.is_empty(p2.m_n))
                 continue;
-            result.push_back(split_pair(r.mk_inter(p1.m_d, p2.m_d),
-                                        r.mk_inter(p1.m_n, p2.m_n), m()));
+            result.push_back(split_pair(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d),
+                                        m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m()));
             if (result.size() > threshold)
                 return false;
         }
@@ -86,6 +86,8 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
     seq_util::rex& rex = re();
     ast_manager& mm = m();
 
+    // std::cout << "compute " << mk_pp(r, m()) << std::endl;
+
     sort* seq_sort = nullptr;
     if (!sq.is_re(r, seq_sort))
         return false;
@@ -147,9 +149,10 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
     // union: sigma(r0 | ... | r_{n-1}) = U sigma(ri)   (re.union may be n-ary)
     if (rex.is_union(r)) {
         app* ap = to_app(r);
-        for (unsigned i = 0; i < ap->get_num_args(); ++i)
+        for (unsigned i = 0; i < ap->get_num_args(); ++i) {
             if (!compute(ap->get_arg(i), result, threshold, mode))
                 return false;
+        }
         return true;
     }
 
@@ -270,6 +273,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
 
     // bounded loop / ite / other: not handled (paper "v1: bail").
     TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, mm) << "\n";);
+    std::cout << "seq_split: unsupported regex " << mk_pp(r, mm) << std::endl;
     return false;
 }
 
@@ -278,7 +282,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
 //   { <D,N>, <D',N> } -> <D | D', N>      (by_left = false, group by N)
 // Only fires on syntactically-identical (perfectly-shared) key components, so
 // it is a conservative instance of the rule.
-void seq_split::merge_by(split_set& pairs, bool by_left) {
+void seq_split::merge_by(split_set& pairs, bool by_left) const {
     seq_util::rex& r = re();
     ast_manager& mm = m();
     obj_map<expr, unsigned> idx;   // key component -> position in `out`
@@ -289,7 +293,8 @@ void seq_split::merge_by(split_set& pairs, bool by_left) {
         unsigned pos;
         if (idx.find(key, pos)) {
             expr* prev = by_left ? out[pos].m_n.get() : out[pos].m_d.get();
-            const expr_ref u(r.mk_union(prev, other), mm);
+            seq_rewriter rw(m());
+            const expr_ref u(m_rw.mk_regex_union_normalize(prev, other), mm);
             if (by_left)
                 out[pos].m_n = u;
             else
@@ -328,9 +333,9 @@ void seq_split::simplify(split_set& pairs) {
     // 3. subsumption: drop <D_i,N_i> when L(D_i) subseteq L(D_j) and
     //    L(N_i) subseteq L(N_j) for some kept j.  seq_subset is conservative
     //    (returns true only for definite containment), so we never drop a
-    //    needed split.  Size-capped to bound the O(n^2) subset checks.
-    if (pairs.size() > 64)
-        return;
+    //    needed split.
+    //if (pairs.size() > 64)
+    //    return;
 
     struct row { expr* d; expr* n; unsigned idx; };
     vector<row> rows;
diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h
index 308ab338a..78f6dcee9 100644
--- a/src/ast/rewriter/seq_split.h
+++ b/src/ast/rewriter/seq_split.h
@@ -75,7 +75,7 @@ class seq_split {
 
     // same-D / same-N merge: groups pairs that share a (syntactically identical)
     // left (resp. right) component and unions the other component.
-    void merge_by(split_set& pairs, bool by_left);
+    void merge_by(split_set& pairs, bool by_left) const;
 
 public:
     explicit seq_split(seq_rewriter& rw);
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 256a3469b..16e31bdbe 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -603,7 +603,7 @@ namespace smt {
                     expr_ref conj(m.mk_and(mem_head, mem_tail), m);
                     lits.push_back(mk_literal(conj));
                     //seq::dep_tracker dep = nullptr;
-                    //std::cout << seq::mem_pp(seq::str_mem(m_sgraph.mk(head), m_sgraph.mk(sp.m_p), dep), m) << " && " << seq::mem_pp(seq::str_mem(m_sgraph.mk(tail), m_sgraph.mk(sp.m_q), dep), m) << "\n";
+                    //std::cout << seq::mem_pp(seq::str_mem(m_sgraph.mk(head), m_sgraph.mk(sp.m_d), dep), m) << " && " << seq::mem_pp(seq::str_mem(m_sgraph.mk(tail), m_sgraph.mk(sp.m_n), dep), m) << "\n";
                 }
                 //std::cout << std::endl;
                 ctx.mk_th_axiom(get_id(), lits.size(), lits.data());