diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index e896820cc5..c7f997c65f 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -403,10 +403,26 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
         return mk_union(mk_single(eps, eps), mk_fromre(a));
     }
 
-    // loop
+    // loop: r{l,h} = \bigcup_{l <= j <= h} r^j.
+    // A split either singles out the i-th copy of a (0 <= i < h) as
+    // <r^i . D, N . r{lo_i,hi_i}> for <D,N> in sigma(a),
+    // where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining
+    // j in [l,h] with j > i, into a single loop [<eps,eps> when l == 0]
     unsigned l, h;
     if (rex.is_loop(r, a, l, h)) {
-        // TODO
+        expr_ref acc = mk_empty();
+        if (l == 0) {
+            const expr_ref eps(rex.mk_epsilon(seq_sort), m);
+            acc = mk_single(eps, eps);
+        }
+        for (unsigned i = 0; i < h; i++) {
+            const expr_ref pre(rex.mk_loop_proper(a, i, i), m);
+            const unsigned lo_i = l > i + 1 ? l - i - 1 : 0;
+            const unsigned hi_i = h - i - 1;
+            const expr_ref post(rex.mk_loop_proper(a, lo_i, hi_i), m);
+            acc = mk_union(acc, mk_lcat(pre, mk_rcat(mk_fromre(a), post)));
+        }
+        return acc;
     }
 
     // bounded loop / ite / other: not handled (paper "v1: bail").
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 4e9bff3fa7..b96e4990e3 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -4338,6 +4338,13 @@ namespace seq {
                     }
                 }
             }
+            // Self-concatenation (e.g. x++x): the tail collapses back onto the
+            // exact same token as the head, so Δ and ∇ constrain the same
+            // variable simultaneously and must be checked jointly -- otherwise
+            // a Δ/∇ pair that is only individually non-empty (e.g. <eps, "a">)
+            // is wrongly treated as feasible.
+            if (st->m_tail == first)
+                regexes_p.push_back(sn_q);
             if (m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) {
                 eliminated_dep = m_dep_mgr.mk_join(eliminated_dep, first_filter_dep);
                 continue;   // infeasible split → skip without branching