diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 6ae072c013..122b23291a 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -4115,6 +4115,17 @@ namespace seq {
         return false;
     }
 
+    bool nielsen_graph::mem_has_cycle_token(str_mem const& mem) const {
+        static const symbol cycle_sym("cycle");
+        SASSERT(mem.m_str);
+        for (euf::snode const* t : mem.m_str->collect_tokens()) {
+            expr* const e = t->get_expr();
+            if (e && m_sk.is_skolem(cycle_sym, e))
+                return true;
+        }
+        return false;
+    }
+
     rf_state* nielsen_graph::mk_rf_state(nielsen_node* /*node*/, str_mem const& mem) {
         euf::snode const* const first = mem.m_str->first();
         SASSERT(first);
@@ -4251,6 +4262,10 @@ namespace seq {
         if (m_regex_factorization_threshold == 0)
             return false;
 
+        for (str_mem const& mem : node->str_mems())
+            if (mem.is_view() || mem.is_guard() || mem_has_cycle_token(mem))
+                return false;
+
         // Continuation: resume the iterator handed down to this node by its
         // parent's "remaining splits" branch.
         if (rf_state* st = node->rf_cont()) {
@@ -4292,6 +4307,12 @@ namespace seq {
             if (leading_var_guarded(node, mem.m_str->first()))
                 continue;
 
+            // Defer when the membership mentions a cycle stabilizer token: the
+            // cycle machinery owns it, and factorizing it re-expands the cycle
+            // structure indefinitely (see mem_has_cycle_token).
+            if (mem_has_cycle_token(mem))
+                continue;
+
             rf_state* st = mk_rf_state(node, mem);
             if (!st)
                 continue;   // unsupported regex shape → try the next membership
@@ -5077,16 +5098,11 @@ namespace seq {
             // not true anymore since we might have done a hot-restart where we previously created the child:
             //SASSERT(n->outgoing().empty());
             SASSERT(n->is_currently_conflict());
-            if (n->m_conflict_external_literal != sat::null_literal) {
-                std::cout << "Node " << n->id() << std::endl;
+            if (n->m_conflict_external_literal != sat::null_literal)
                 // We know from the outer solver that this literal is assigned true and contradicts node constraint
                 deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
-            }
-
-            if (n->m_conflict_internal) {
-                std::cout << "Node " << n->id() << std::endl;
+            if (n->m_conflict_internal)
                 deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
-            }
         }
         return deps;
     }
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 331eebc2f5..8120a4e74f 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -1399,6 +1399,14 @@ namespace seq {
         // disjunction is refuted → the continuation node is a regex conflict.
         bool apply_regex_factorization(nielsen_node* node);
 
+        // True if the membership's string mentions a `cycle` stabilizer token
+        // (the (cycle x R) Skolem minted by apply_cycle_decomposition).  Such a
+        // membership is owned by the cycle machinery; factorization must defer to
+        // it — re-splitting it re-expands the very structure the cycle rule is
+        // trying to close, and the fresh slice variables each cycle step mints
+        // defeat the exact-structural loop-cut → non-termination.
+        bool mem_has_cycle_token(str_mem const& mem) const;
+
         // Build a suspended factorization (boundary head/tail + split iterator)
         // for `mem`.  Returns null if the regex shape is unsupported (the engine
         // cannot even start a split).  Allocated into m_rf_states.
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 0da43bd7f0..2bdfe67dd5 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -1005,6 +1005,7 @@ namespace smt {
                 m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
                 m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
                 m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager);
+                m_nielsen.set_regex_dynamic_decomposition(get_fparams().m_nseq_regex_dynamic_decomposition);
                 m_nielsen.set_harvest(get_fparams().m_nseq_harvest);
                 m_nielsen.set_harvest_dir(get_fparams().m_nseq_harvest_dir.str());