diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 122b23291a..a8a41d730f 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2329,7 +2329,7 @@ namespace seq {
         // differs), so it would alias the parent's signature, yet it still has
         // pending splits to explore — it is not a true recurrence.
         {
-            if (!node->rf_cont() && m_unsat_node_cache.contains(node)) {
+            if (!node->is_rf_cont() && m_unsat_node_cache.contains(node)) {
                 node->set_conflict(backtrack_reason::sibling, nullptr /*we use the one of the sibling*/);
                 node->set_general_conflict();
                 node->m_unsat_cacheable = true;
@@ -2429,12 +2429,17 @@ namespace seq {
         // with string-only conflicts and self-contained cuts (see the epilogue).
         // -------------------------------------------------------------------
         node->canonize_and_compute_final_node_hash();
-        // A lazy-factorization continuation node (rf_cont set) is EXEMPT from the
+        // A lazy-factorization continuation node (is_rf_cont) is EXEMPT from the
         // loop-cut: it aliases its parent's string signature (only the suspended
         // split iterator differs) but is not a true recurrence — it still has
         // pending splits.  The iterator is finite, so the continuation chain
-        // terminates on its own (exhaustion → regex conflict).
-        if (!node->rf_cont()) {
+        // terminates on its own (exhaustion → regex conflict).  The exemption uses
+        // the STICKY is_rf_cont() marker, not the live rf_cont() pointer: the
+        // pointer is nulled once the node is extended, but on a hot-restart the
+        // node is re-traversed without re-extending, and it must stay exempt (else
+        // it is wrongly cut as a sibling of the ancestor it aliases, pruning a
+        // branch that may still lead to SAT).
+        if (!node->is_rf_cont()) {
             auto it = m_siblings.find(node);
             if (it != m_siblings.end() && !it->second.empty()) {
                 nielsen_node* anc = it->second.back(); // deepest sibling still on the path
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 8120a4e74f..e594e8a36f 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -600,6 +600,14 @@ namespace seq {
         // split iterator so factorization resumes from the next split when this
         // node is extended.  Owned by nielsen_graph::m_rf_states (raw pointer here).
         rf_state*               m_rf_cont = nullptr;
+        // Sticky marker: true once this node was ever created as a factorization
+        // continuation (child B), even after its iterator has been consumed
+        // (m_rf_cont reset to null when the node is extended).  The subsumption
+        // loop-cut and unsat-cache exemptions (§1.6b) are a PERMANENT structural
+        // property of a continuation node — it aliases its parent's string
+        // signature yet is not a recurrence — so they must survive the hot-restart
+        // re-traversal, where m_rf_cont is already null.  See search_dfs.
+        bool                    m_is_rf_cont = false;
         // number of constraints inherited from the parent node at clone time.
         // constraints[0..m_parent_ic_count) are already asserted at the
         // parent's solver scope; only [m_parent_ic_count..end) need to be
@@ -657,7 +665,11 @@ namespace seq {
 
         // lazy regex factorization continuation (see m_rf_cont).
         rf_state* rf_cont() const { return m_rf_cont; }
-        void set_rf_cont(rf_state* s) { m_rf_cont = s; }
+        void set_rf_cont(rf_state* s) { m_rf_cont = s; if (s) m_is_rf_cont = true; }
+        // Sticky: true if this node was ever a factorization continuation, even
+        // after its iterator has been consumed.  Drives the loop-cut / unsat-cache
+        // exemptions so they persist across the hot-restart re-traversal.
+        bool is_rf_cont() const { return m_is_rf_cont; }
 
         // returns 0 if hash is unknown
         unsigned hash() const {