diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py
index 7dbebae9ef..acd022a876 100644
--- a/scripts/compare_seq_solvers.py
+++ b/scripts/compare_seq_solvers.py
@@ -37,9 +37,9 @@ COMMON_ARGS = ["model_validate=true"]
 # All three configurations are always run.
 SOLVERS = {
     "nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
-                "smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true"],
+                "smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=true", "smt.nseq.regex_dynamic_decomposition=false"],
     "nseq_pa": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
-                "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false"],
+                "smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=true"],
     "seq":     ["smt.string_solver=seq"],
 }
 
diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index fcba3a8d03..e896820cc5 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -223,7 +223,7 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul
     split_set acc;
     push(acc, oracle, r.mk_complement(sp[0].m_d), full);
     push(acc, oracle, full, r.mk_complement(sp[0].m_n));
-    for (unsigned i = 1; i < sp.size(); ++i) {
+    for (unsigned i = 1; i < sp.size(); i++) {
         split_set next;
         push(next, oracle, r.mk_complement(sp[i].m_d), full);
         push(next, oracle, full, r.mk_complement(sp[i].m_n));
@@ -300,7 +300,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
             }
         }
         expr_ref acc = mk_empty();
-        for (unsigned i = 0; i <= str.length(); ++i) {
+        for (unsigned i = 0; i <= str.length(); i++) {
             const expr_ref p(rex.mk_to_re(sq.str.mk_string(str.extract(0, i))), m);
             const expr_ref q(rex.mk_to_re(sq.str.mk_string(str.extract(i, str.length() - i))), m);
             acc = mk_union(acc, mk_single(p, q));
@@ -338,7 +338,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
         app* ap = to_app(r);
         const unsigned n = ap->get_num_args();
         expr_ref acc = mk_empty();
-        for (unsigned i = 0; i < n; ++i) {
+        for (unsigned i = 0; i < n; i++) {
             expr_ref left(m), right(m);
             if (i == 0)
                 left = rex.mk_epsilon(seq_sort);
@@ -381,8 +381,9 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
         app* ap = to_app(r);
         const unsigned n = ap->get_num_args();
         expr_ref acc = mk_fromre(ap->get_arg(0));
-        for (unsigned i = 1; i < n; ++i)
+        for (unsigned i = 1; i < n; i++) {
             acc = mk_inter(acc, mk_fromre(ap->get_arg(i)));
+        }
         return acc;
     }
 
@@ -390,10 +391,24 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) {
     if (rex.is_complement(r, a))
         return mk_compl(mk_fromre(a));
 
+    // abbreviation
     // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b).
     if (rex.is_diff(r, a, b))
         return mk_inter(mk_fromre(a), mk_compl(mk_fromre(b)));
 
+    // abbreviation
+    // optional: a? = eps | a ; sigma(a?) = sigma(eps | a) = eps cup sigma(a)
+    if (rex.is_opt(r, a)) {
+        const expr_ref eps(rex.mk_epsilon(seq_sort), m);
+        return mk_union(mk_single(eps, eps), mk_fromre(a));
+    }
+
+    // loop
+    unsigned l, h;
+    if (rex.is_loop(r, a, l, h)) {
+        // TODO
+    }
+
     // bounded loop / ite / other: not handled (paper "v1: bail").
     TRACE(seq, tout << "seq_split: unsupported regex " << mk_pp(r, m) << "\n";);
     ok = false;
@@ -624,7 +639,7 @@ void seq_split::simplify(split_set& pairs) const {
 
     // 1. drop pairs with a bottom (empty-language) component.
     unsigned w = 0;
-    for (unsigned i = 0; i < pairs.size(); ++i) {
+    for (unsigned i = 0; i < pairs.size(); i++) {
         if (r.is_empty(pairs[i].m_d) || r.is_empty(pairs[i].m_n))
             continue;
         if (w != i)
@@ -650,7 +665,7 @@ void seq_split::simplify(split_set& pairs) const {
 
     struct row { expr* d; expr* n; unsigned idx; };
     vector<row> rows;
-    for (unsigned i = 0; i < pairs.size(); ++i)
+    for (unsigned i = 0; i < pairs.size(); i++)
         rows.push_back({ pairs[i].m_d.get(), pairs[i].m_n.get(), i });
 
     auto subsumes = [&](row const& a, row const& b) {
@@ -769,7 +784,7 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
     // Build the constant lookahead c and (if non-empty) an oracle that
     // prunes splits whose postfix cannot match c.
     zstring c;
-    for (i = 0; i < run_len; ++i) {
+    for (i = 0; i < run_len; i++) {
         unsigned cv;
         VERIFY(seq().str.is_unit(tokens.get(run_start + i), ch));
         VERIFY(seq().is_const_char(ch, cv));
@@ -791,7 +806,7 @@ std::pair<expr_ref, expr_ref> seq_split::split_membership(expr* str, expr* regex
     // of each postfix
     if (!c.empty()) {
         unsigned w = 0;
-        for (i = 0; i < result.size(); ++i) {
+        for (i = 0; i < result.size(); i++) {
             expr* d = result[i].m_n;
             for (unsigned k = 0; d && !seq().re.is_empty(d) && k < c.length(); ++k) {
                 d = m_rw.mk_derivative(seq().mk_char(c[k]), d);
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index a8a41d730f..4e9bff3fa7 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -288,15 +288,12 @@ namespace seq {
 
     bool str_mem::is_trivial(nielsen_node const* n) const {
         SASSERT(m_str && m_regex);
-        if (m_kind == mem_kind::no_loop)
-            // guard: discharged ⇒ Σ* (accepts all); ε has no non-empty lap-prefix.
-            return m_discharged || m_str->is_empty();
         if (m_regex->is_full_seq())
             return true;
         if (!m_str->is_empty())
             return false;
         if (m_kind == mem_kind::stab_view)
-            // ε ∈ stab(root,Q) iff current state ≡ root (i.e. root ∈ F={root}).
+            // ε ∈ L_{Q,{s}}(state) iff current state ≡ acceptance state s (=m_root).
             return m_regex == m_root;
         return n->graph().sg().re_nullable(m_regex) == l_true;
     }
@@ -304,10 +301,8 @@ namespace seq {
     bool str_mem::is_contradiction(nielsen_node const* n) const {
         if (!(m_str && m_regex && m_str->is_empty()))
             return false;
-        if (m_kind == mem_kind::no_loop)
-            return false; // guard acceptance is always true on the empty word
         if (m_kind == mem_kind::stab_view)
-            return m_regex != m_root; // ε ∉ stab(root,Q) when state ≢ root
+            return m_regex != m_root; // ε ∉ view when current state ≢ acceptance s
         return n->graph().sg().re_nullable(m_regex) == l_false;
     }
 
@@ -427,11 +422,14 @@ namespace seq {
         SASSERT(mem.m_regex != nullptr);
         if (mem.is_trivial(this))
             return;
-        // check if root node contains this membership constraint already
-        if (std::ranges::any_of(str_mems(),
-                                [&](const str_mem &e) { return e.m_regex == mem.m_regex && e.m_str == mem.m_str; }))
-            // already present, no need to add again
-            return;
+        // Skip only a FULLY identical membership.  The dedup must compare the
+        // whole membership (kind/root/ν), not just (m_str,m_regex): a land-state
+        // view (paper §5.3) shares (m_str,m_regex) with a plain membership on the
+        // same variable+state, and two land-views on the same state differ only
+        // in their acceptance root / ν.  Deduping on (m_str,m_regex) alone would
+        // silently drop such a view and lose the constraint (→ unsound leaf).
+        if (std::ranges::any_of(str_mems(), [&](const str_mem &e) { return e == mem; }))
+            return; // already present
         m_str_mem.push_back(mem);
     }
 
@@ -1262,6 +1260,107 @@ namespace seq {
         return newly_marked;
     }
 
+    // -----------------------------------------------------------------------
+    // Landing decomposition support: Q = states forward-reachable from the head.
+    // -----------------------------------------------------------------------
+
+    void nielsen_graph::collect_reachable_from_head(euf::snode const* head_re, uint_set& Q) const {
+        Q.reset();
+        if (!head_re || !head_re->get_expr())
+            return;
+        unsigned_vector stack;
+        stack.push_back(head_re->get_expr()->get_id());
+        while (!stack.empty()) {
+            const unsigned s = stack.back();
+            stack.pop_back();
+            if (Q.contains(s))
+                continue;
+            Q.insert(s);
+            auto it = m_partial_dfa_out.find(s);
+            if (it == m_partial_dfa_out.end())
+                continue;
+            for (const unsigned edge_idx : it->second) {
+                if (edge_idx >= m_partial_dfa_edges.size())
+                    continue;
+                partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx];
+                if (e.m_dst)
+                    stack.push_back(e.m_dst->get_id());
+            }
+        }
+    }
+
+    unsigned nielsen_graph::mark_reachable_projection_edges(euf::snode const* head_re) {
+        // Generalizes mark_scc_projection_edges to the forward-reachable set:
+        // mark every edge whose source is reachable from head_re with the current
+        // extraction index ν, bumping ν iff something new was marked.  Views/co-
+        // views gate on projection_state_in_Q (edges marked ≤ ν), so the ν
+        // returned here identifies exactly this Q.
+        uint_set Q;
+        collect_reachable_from_head(head_re, Q);
+        unsigned newly_marked = 0;
+        for (const unsigned src_id : Q) {
+            auto it = m_partial_dfa_out.find(src_id);
+            if (it == m_partial_dfa_out.end())
+                continue;
+            for (const unsigned edge_idx : it->second) {
+                if (edge_idx >= m_partial_dfa_edges.size())
+                    continue;
+                partial_dfa_edge const& e = m_partial_dfa_edges[edge_idx];
+                if (!e.m_dst || !Q.contains(e.m_dst->get_id()))
+                    continue;
+                if (e.m_projection_idx == 0)
+                    ++newly_marked;
+            }
+        }
+        if (newly_marked == 0)
+            return m_projection_extract_idx; // Q already covered by the current ν
+
+        ++m_projection_extract_idx;
+        const unsigned extract_idx = m_projection_extract_idx;
+        for (const unsigned src_id : Q) {
+            auto it = m_partial_dfa_out.find(src_id);
+            if (it == m_partial_dfa_out.end())
+                continue;
+            for (const unsigned edge_idx : it->second) {
+                if (edge_idx >= m_partial_dfa_edges.size())
+                    continue;
+                partial_dfa_edge& e = m_partial_dfa_edges[edge_idx];
+                if (!e.m_dst || !Q.contains(e.m_dst->get_id()))
+                    continue;
+                if (e.m_projection_idx == 0)
+                    e.m_projection_idx = extract_idx;
+            }
+        }
+        return extract_idx;
+    }
+
+    void nielsen_graph::compute_frontier(uint_set const& Q, svector<euf::snode const*> const& Qstates,
+                                         vector<frontier_edge>& out_frontier) {
+        // One lazy step from each Q state.  Derive over the minterms of every
+        // p ∈ Qstates: δ_mt(p) ∈ Q is an internal edge (recorded, closing cycles
+        // for a future land-at-R); δ_mt(p) ∉ Q (and ≠ ⊥) is a frontier/escape
+        // edge.  Snapshot Qstates was collected by the caller BEFORE this call,
+        // so recording internal edges (which appends to m_partial_dfa_edges) does
+        // not disturb the iteration.
+        for (euf::snode const* p : Qstates) {
+            if (!m.inc())
+                return;
+            if (!p || !p->is_ground())
+                continue;
+            euf::snode_vector mts;
+            m_sg.compute_minterms(p, mts);
+            for (euf::snode const* mt : mts) {
+                euf::snode const* q = m_sg.brzozowski_deriv(p, mt);
+                if (!q || q->is_fail() || !q->is_ground())
+                    continue;
+                if (Q.contains(q->get_expr()->get_id()))
+                    record_partial_derivative_edge(p, q);   // internal edge
+                else
+                    out_frontier.push_back(frontier_edge{ p, mt, q });
+            }
+        }
+    }
+
     euf::snode const* nielsen_graph::get_slice(euf::snode const* v, expr* left, expr* right) {
         SASSERT(v && v->get_expr() && left && right);
         SASSERT(v->is_var());
@@ -1804,15 +1903,15 @@ namespace seq {
             }
         }
 
-        // consume leading characters of view / guard memberships (Section 3.3).
+        // consume leading characters of land-state view memberships (paper §5.3).
         // m_regex is the current (plain) derivative state; we gate on whether it
         // lies in Q_ν (projection_state_in_Q) and step with the ordinary
-        // derivative, keeping the view/guard annotation.
+        // derivative, keeping the view annotation.
         for (str_mem& mem : m_str_mem) {
             SASSERT(mem.well_formed());
             if (mem.is_plain())
                 continue;
-            if (consume_view_guard(mem))
+            if (consume_view(mem))
                 return simplify_result::conflict;
         }
 
@@ -1864,8 +1963,8 @@ namespace seq {
         return simplify_result::proceed;
     }
 
-    bool nielsen_node::consume_view_guard(str_mem& mem) {
-        SASSERT(!mem.is_plain());
+    bool nielsen_node::consume_view(str_mem& mem) {
+        SASSERT(mem.is_view());
         euf::sgraph& sg = m_graph.sg();
 
         auto set_regex_conflict = [&]() {
@@ -1883,24 +1982,17 @@ namespace seq {
             // leave it for apply_regex_if_split.
             if (!c->is_ground() || c->kind() == euf::snode_kind::s_ite)
                 break;
-            const bool in_Q = m_graph.projection_state_in_Q(c->get_expr(), mem.m_nu);
-            if (!in_Q) {
-                if (mem.is_guard()) {
-                    // The run left Q: no lap from the start can complete within Q
-                    // anymore, so the guard is discharged (accepts every suffix).
-                    mem.m_discharged = true;
-                    return false;
-                }
-                // view: a^{-1} L_{Q,F}(c) = ∅ when c ∉ Q.
+            if (!m_graph.projection_state_in_Q(c->get_expr(), mem.m_nu)) {
+                // a^{-1} L_{Q,F}(c) = ∅ when c ∉ Q.
                 set_regex_conflict();
                 return true;
             }
             // Step with brzozowski_deriv for BOTH concrete and symbolic tokens.
             // This is essential: the partial-DFA states (and m_root) are produced
             // by brzozowski_deriv, so its canonicalization must be used here too —
-            // otherwise the guard's resolved state never equals m_root by snode
-            // identity and laps never close.  For a symbolic unit it yields a
-            // canonical ite residual that apply_regex_if_split later resolves.
+            // otherwise the resolved state never equals m_root by snode identity.
+            // For a symbolic unit it yields a canonical ite residual that
+            // apply_regex_if_split later resolves.
             euf::snode const* next = sg.brzozowski_deriv(c, tok);
             if (!next)
                 break;
@@ -1908,25 +2000,11 @@ namespace seq {
             mem.m_regex = next;
             if (next->is_fail()) {
                 // view: derivative collapsed to ∅ — unsatisfiable.
-                // guard: the lap can never close through ∅; treat as discharged.
-                if (mem.is_guard()) { mem.m_discharged = true; return false; }
                 set_regex_conflict();
                 return true;
             }
-            if (next->is_ground() && next->kind() != euf::snode_kind::s_ite) {
-                // concrete next state resolved immediately
-                if (mem.is_guard() && next == mem.m_root) {
-                    // a non-empty prefix completed a lap r→…→r within Q.
-                    set_regex_conflict();
-                    return true;
-                }
-            }
-            else {
-                // symbolic ite residual: defer to apply_regex_if_split, which
-                // resolves the character and (for guards) detects a lap landing
-                // back on the root.
-                break;
-            }
+            if (!(next->is_ground() && next->kind() != euf::snode_kind::s_ite))
+                break;   // symbolic ite residual: defer to apply_regex_if_split
         }
         return false;
     }
@@ -2106,7 +2184,7 @@ namespace seq {
             ++m_stats.m_num_unknown;
             return search_result::unknown;
         }
-        catch(const std::exception&) {
+        catch(const std::exception& e) {
 #ifdef Z3DEBUG
             std::string dot = to_dot();
 #endif
@@ -3381,9 +3459,11 @@ namespace seq {
         if (!harvest_mode() && apply_cycle_subsumption(node))
             return ++m_stats.m_mod_cycle_subsumption, true;
 
-        // Priority 6: CycleDecomp - stabilizer introduction for regex cycles using partial DFA projection
+        // Priority 6: LandingDecomp - the core branching rule (paper §5.3):
+        // split the leading variable by its landing state in the explored region
+        // (land-at-s + escape-via-frontier).  Subsumes character unwinding.
         // (regex-related: skipped in benchmark-harvest mode)
-        if (!harvest_mode() && apply_cycle_decomposition(node))
+        if (!harvest_mode() && apply_landing_decomposition(node))
             return ++m_stats.m_mod_star_intr, true;
 
         // Priority 7: GPowerIntr - ground power introduction
@@ -3883,12 +3963,17 @@ namespace seq {
             if (!first->is_var())
                 continue;
             euf::snode const* R = mem.m_regex;
+            if (!R->is_ground() || R->kind() == euf::snode_kind::s_ite)
+                continue;
 
-            // R must lie on a detected cycle with a marked SCC snapshot.
+            // R must lie on a detected cycle in the explored region.  Use the
+            // same reachable-Q snapshot as apply_landing_decomposition so the
+            // stabilizer view stab(R,Q_ν) matches the land-at-R view.
+            ensure_automaton_explored(R);
             uint_set scc;
             if (!collect_scc_for_projection(R, scc))
                 continue;
-            const unsigned nu = m_projection_extract_idx;
+            const unsigned nu = mark_reachable_projection_edges(R);
             if (nu == 0)
                 continue;
 
@@ -3924,105 +4009,156 @@ namespace seq {
     }
 
     // -----------------------------------------------------------------------
-    // Modifier: apply_cycle_decomposition  (paper Section "Cycle Decomposition")
+    // Modifier: apply_landing_decomposition  (paper §5.3 "Landing Decomposition")
     //
-    // For a membership x·u ∈ R whose leading variable x sits on a detected cycle
-    // (R lies in an SCC of the partial DFA) and that does not already carry a
-    // matching cycle guard for the current SCC snapshot, split
-    //   x → x'·x''
-    // and attach the two *view*/*guard* primitive constraints (Section 3.3):
-    //   x' ∈ stab(R, Q_ν)            -- stabilizer view  (F = {R})
-    //   noloop(x'', R, Q_ν)          -- cycle guard      (two-mode monitor)
-    // The leading x' is immediately subsumed (its only constraint is the view,
-    // and stab ⊆ stab trivially), so it is dropped from the primary constraint.
+    // The core branching rule.  For a plain non-primitive membership x·u ∈ R
+    // (u ≠ ε, x a variable, R a ground regex) we split x by WHERE its value
+    // lands in the explored region Q — the states forward-reachable from R in
+    // the partial DFA G — using the frontier partition (Lemma 4.7):
     //
-    // Unlike the old projection-operator encoding, the view and guard are kept
-    // as *constraint metadata* over the plain state R and the ν-indexed explored
-    // subautomaton Q_ν — nothing is materialized as a regex, which keeps the
-    // reachable state space finite (termination).
+    //   Land-at-s  (for each s ∈ Q):
+    //       pin  x ∈_{Q_ν,{s}} R   (land-state view, acceptance F = {s},
+    //                               current state = R) and advance to  u ∈ s.
+    //       x is removed outright (no split, no guard).  s = R is stabilizer
+    //       absorption: one view swallows every lap of the R-cycle.
+    //
+    //   Escape-via-(p,a)  (for each frontier edge p ∈ Q, δ_a(p) ∉ Q):
+    //       substitute  x → x1·a·x2  (x1,x2 fresh), pin  x1 ∈_{Q_ν,{p}} R,
+    //       drop x1 from the active constraint (it lands at p) leaving
+    //       a·x2·u ∈ p; the normal char-consumption then steps p →a δ_a(p),
+    //       recording the new edge and growing Q.
+    //
+    // By Lemma 4.7 the blocks partition Σ*, so the branches are exhaustive and
+    // pairwise disjoint.  Character unwinding is the degenerate Q = {R} case
+    // (land-at-R = x→ε; escape-via-(R,a) = x→a·x2), so this rule subsumes
+    // apply_regex_var_split for ground regexes.  Views are constraint metadata
+    // over the plain state R and the ν-indexed explored subautomaton Q_ν
+    // (projection_state_in_Q) — nothing is materialized as a regex.
+    // Termination: a landing removes a variable (active term shrinks); each
+    // escape consumes a fresh state of the finite monotone G.
     // -----------------------------------------------------------------------
 
-    bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) {
+    bool nielsen_graph::apply_landing_decomposition(nielsen_node* node) {
         if (!m_regex_dynamic_decomposition)
             return false;
-        // Look for a str_mem with a variable-headed string
         for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) {
             str_mem const& mem = node->str_mems()[mi];
             SASSERT(mem.well_formed());
             if (!mem.is_plain() || mem.is_primitive())
                 continue;
-            euf::snode const* first = mem.m_str->first();
-            SASSERT(first);
-            if (!first->is_var())
+            euf::snode const* x = mem.m_str->first();
+            SASSERT(x);
+            if (!x->is_var())
+                continue;
+            euf::snode const* R = mem.m_regex;
+            // R must be a settled ground state; an unresolved symbolic ite is
+            // left to apply_regex_if_split, a non-ground regex to the var-split
+            // fallback.
+            if (!R->is_ground() || R->kind() == euf::snode_kind::s_ite)
                 continue;
 
-            euf::snode const* x = first;
-            euf::snode const* R = mem.m_regex;
-
-            // Lazily explore R's full automaton (once, cached) so that
-            // collect_scc_for_projection sees the complete SCC of R and the
-            // stabilizer view / cycle guard gate on a complete Q.
+            // Eagerly explore R's reachable automaton (once, cached) so the SCC
+            // gate below and the landing enumeration see the full explored region
+            // Q — this is the automaton-based landing.  Without it the cycle would
+            // not be recorded before factorization/var_split fire, so landing
+            // would never trigger.  If exploration hits the resource limit Q is
+            // left partial (a sound under-approximation) and the escape branches
+            // recover completeness.
             ensure_automaton_explored(R);
 
-            // R must sit on a cycle (an SCC of the partial DFA).
-            uint_set scc;
-            if (!collect_scc_for_projection(R, scc))
-                continue;
-            // Mark the SCC edges; this gives a ν identifying the current Q_SCC.
-            // (We trigger on absence of a matching guard, NOT on novelty.)
-            mark_scc_projection_edges(scc);
-            const unsigned nu = m_projection_extract_idx;
-            if (nu == 0)
-                continue;
+            // Trigger: R must sit on a detected cycle in the explored G.  This is
+            // the same gate the old split-and-guard apply_cycle_decomposition
+            // used; the acyclic growth/unwinding of x is left to the pre-existing
+            // flow (apply_regex_var_split / apply_regex_factorization).  Landing
+            // then replaces the split+guard on cyclic heads with land-at-s +
+            // escape, and is exhaustive on its own (frontier partition) so
+            // preempting var_split at this node loses no words.
+            {
+                uint_set scc;
+                if (!collect_scc_for_projection(R, scc))
+                    continue;
+            }
 
-            // Trigger condition: x must not already carry a cycle guard for the
-            // current SCC snapshot ν.  All states of one SCC share a single ν, so
-            // the guard is keyed on ν rather than on the (changing) head R: as the
-            // derivation walks the SCC the head moves, but the lineage is already
-            // guarded against re-traversing the cycle.  An already-decomposed
-            // variable whose guard refers to a strictly smaller, stale ν is
-            // re-decomposed to adopt the enlarged SCC.
-            bool already_guarded = false;
-            for (str_mem const& g : node->str_mems()) {
-                if (g.is_guard() && g.m_nu >= nu
-                    && g.m_str && g.m_str->first() == x) {
-                    already_guarded = true;
-                    break;
+            // Q = states forward-reachable from R (ids), and their snode handles.
+            uint_set Q;
+            collect_reachable_from_head(R, Q);
+            svector<euf::snode const*> Qstates;
+            uint_set added;
+            Qstates.push_back(R);
+            added.insert(R->get_expr()->get_id());
+            for (partial_dfa_edge const& e : m_partial_dfa_edges) {
+                for (expr* ep : { e.m_src, e.m_dst }) {
+                    if (!ep) continue;
+                    const unsigned id = ep->get_id();
+                    if (!Q.contains(id) || added.contains(id)) continue;
+                    euf::snode const* sn = m_sg.find(ep);
+                    if (sn) { added.insert(id); Qstates.push_back(sn); }
                 }
             }
-            if (already_guarded)
-                continue;
+
+            // One lazy exploration step: record internal (cycle-closing) edges
+            // and collect the frontier (escape candidates).
+            vector<frontier_edge> frontier;
+            compute_frontier(Q, Qstates, frontier);
+
+            // Mark the reachable subautomaton, fixing the ν that identifies Q_ν
+            // for every view created below.  ν may be 0 in the Q = {R} bootstrap
+            // (no in-Q edges yet); a view with ν = 0 denotes exactly {ε} at R,
+            // which is precisely what unwinding needs.
+            const unsigned nu = mark_reachable_projection_edges(R);
 
             sort* seq_sort = x->get_expr()->get_sort();
 
-            // Construct the replacement x = x' x''
-            euf::snode const* xp      = m_sg.mk(m_sk.mk("cycle", x->get_expr(), R->get_expr(), seq_sort));
-            euf::snode const* xpp     = get_tail(x, compute_length_expr(xp).get());
-            euf::snode const* xp_xpp  = m_sg.mk_concat(xp, xpp);
+            // (a) LAND-AT-s branches (progress: x removed).
+            for (euf::snode const* s : Qstates) {
+                nielsen_node* child = mk_child(node);
+                mk_edge(node, child, "land", /*progress*/ true);
+                str_mem& cm = child->m_str_mem[mi];
+                cm.m_str = m_sg.drop_first(cm.m_str);      // u
+                cm.m_regex = s;                            // active becomes  u ∈ s
+                // x ∈_{Q_ν,{s}} R : state = R (start), root = s (acceptance).
+                child->add_str_mem(str_mem::mk_view(m, x, R, s, nu, mem.m_dep));
+                TRACE(seq, tout << "landing: land x=" << mk_pp(x->get_expr(), m)
+                                << " at " << mk_pp(s->get_expr(), m)
+                                << " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n");
+            }
 
-            nielsen_node* child = mk_child(node);
-            SASSERT(child->m_str_mem[mi] == mem);
-            nielsen_edge* e     = mk_edge(node, child, "cycle decomp", false);
-            const nielsen_subst s(x, xp_xpp, mem.m_dep);
-            e->add_subst(s);
-            child->apply_subst(m_sg, s);
+            // (b) ESCAPE branches (non-progress: consumes a fresh state, grows Q).
+            for (frontier_edge const& fe : frontier) {
+                euf::snode const* p = fe.m_src;
+                char_set cs = m_seq_regex->minterm_to_char_set(fe.m_mt->get_expr());
+                if (cs.is_empty())
+                    continue;
+                euf::snode const* aunit =
+                    m_sg.mk(m_seq.str.mk_unit(m_seq.mk_char(cs.first_char())));
+                euf::snode const* x1 = mk_fresh_var(seq_sort);
+                // x2 = x[|x1|+1:]  (slice tail after the landed prefix and the char)
+                const expr_ref after =
+                    normalize_arith(m, a.mk_add(compute_length_expr(x1).get(), a.mk_int(1)));
+                euf::snode const* x2 = get_tail(x, after.get());
+                euf::snode const* repl = m_sg.mk_concat(x1, m_sg.mk_concat(aunit, x2));
 
-            // remove from mi^th element of the child the leading token, as it is immediately subsumed
-            SASSERT(child->m_str_mem[mi].m_str->first() == xp);
-            child->m_str_mem[mi].m_str = dir_drop(m_sg, child->m_str_mem[mi].m_str, 1, true);
+                nielsen_node* child = mk_child(node);
+                nielsen_edge* e = mk_edge(node, child, "escape", /*progress*/ false);
+                const nielsen_subst sub(x, repl, mem.m_dep);
+                e->add_subst(sub);
+                child->apply_subst(m_sg, sub);
 
-            // x' ∈ stab(R, Q_ν)   (stabilizer view, F = {R}, current state = R)
-            child->add_str_mem(str_mem::mk_view(m, xp, R, R, nu, mem.m_dep));
+                // x1 lands at p: drop it from the active constraint, whose state
+                // becomes p; the leading a is then consumed by simplify_and_init
+                // (stepping p →a δ_a(p) and recording the edge).
+                str_mem& cm = child->m_str_mem[mi];
+                SASSERT(cm.m_str->first() == x1);
+                cm.m_str = dir_drop(m_sg, cm.m_str, 1, true);   // a·x2·u
+                cm.m_regex = p;
+                // x1 ∈_{Q_ν,{p}} R
+                child->add_str_mem(str_mem::mk_view(m, x1, R, p, nu, mem.m_dep));
+                TRACE(seq, tout << "landing: escape x=" << mk_pp(x->get_expr(), m)
+                                << " via (" << mk_pp(p->get_expr(), m) << ", "
+                                << cs.first_char() << ") R=" << mk_pp(R->get_expr(), m)
+                                << " nu=" << nu << "\n");
+            }
 
-            // noloop(x'', R, Q_ν)  (cycle guard, two-mode monitor, state = R)
-            child->add_str_mem(str_mem::mk_guard(m, xpp, R, R, nu, mem.m_dep));
-
-            TRACE(seq, tout << "cycle_decomp: x=" << mk_pp(x->get_expr(), m)
-                            << " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n");
-
-#ifdef Z3DEBUG
-            std::string dot = partial_dfa_to_dot(R, false);
-#endif
             return true;
         }
         return false;
@@ -4108,29 +4244,6 @@ namespace seq {
     // complement bodies against runaway space blow-up.
     static const unsigned RF_LAZY_CAP = 1u << 20;
 
-    // The cycle machinery (apply_cycle_decomposition) owns variables it has put
-    // under a noloop guard: factorizing such a variable's membership would split
-    // it in a way that violates the guard's premise (that the variable is handled
-    // by the stabilizer/guard decomposition), yielding a spurious conflict.  So
-    // factorization defers whenever the leading token is a guarded variable.
-    static bool leading_var_guarded(nielsen_node const* node, euf::snode const* lead) {
-        for (str_mem const& g : node->str_mems())
-            if (g.is_guard() && g.m_str && g.m_str->first() == lead)
-                return true;
-        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);
@@ -4267,18 +4380,18 @@ 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))
+        // A node under landing control carries land-state views; the cycle
+        // machinery (apply_landing_decomposition / apply_cycle_subsumption) owns
+        // it, so factorization defers.
+        for (str_mem const& mem : node->str_mems()) {
+            if (mem.is_view())
                 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()) {
             node->set_rf_cont(nullptr);   // the iterator migrates to child B (or is dropped)
-            // If the cycle machinery has, in the meantime, put the leading variable
-            // under a guard, stop factorizing and defer (the iterator is dropped).
-            if (leading_var_guarded(node, st->m_mem.m_str->first()))
-                return false;
             dep_tracker conflict_dep = nullptr;
             switch (rf_step(node, st, conflict_dep)) {
             case rf_step_result::branched:
@@ -4297,27 +4410,18 @@ namespace seq {
         // Fresh: find the first factorizable membership and start an iterator.
         for (str_mem const& mem : node->str_mems()) {
             SASSERT(mem.well_formed());
+            SASSERT(!mem.m_str->is_empty()); // should have been eliminated already
 
             // split() handles all regex forms (incl. complement / intersection),
             // so the classical restriction is no longer needed.
-            if (mem.m_str->is_empty() || mem.is_primitive())
+            if (mem.is_primitive())
                 continue;
 
-            // View / guard memberships (Section 3.3) are handled by the
-            // cycle machinery and the synchronous product, not by factorization.
+            // Land-state view memberships (paper §5.3) are handled by the cycle
+            // machinery and the synchronous product, not by factorization.
             if (!mem.is_plain())
                 continue;
 
-            // Defer to the cycle machinery when the leading variable is guarded.
-            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
@@ -4659,7 +4763,7 @@ namespace seq {
                     // Canonicalize with th_rewriter so that the resolved leaf shares
                     // its snode id with the corresponding partial-DFA state (which is
                     // built by brzozowski_deriv); otherwise un-simplified residuals
-                    // like (a|∅)·R≠a·R break view/guard Q-membership and lap checks.
+                    // like (a|∅)·R≠a·R break view Q-membership checks.
                     euf::snode const* new_regex_snode = mk_rewrite(r);
                     nielsen_node *child = mk_child(node);
                     nielsen_edge* e = mk_edge(node, child, "regex if", true);
@@ -4669,12 +4773,6 @@ namespace seq {
                     for (str_mem &cm : child->str_mems()) {
                         if (cm == mem) {
                             cm.m_regex = new_regex_snode;
-                            // A guard whose symbolic step lands back on the cycle
-                            // head closed a lap within Q → this branch is dead.
-                            if (cm.is_guard() && new_regex_snode == cm.m_root) {
-                                child->set_general_conflict();
-                                child->set_conflict(backtrack_reason::regex, cm.m_dep);
-                            }
                             break;
                         }
                     }
@@ -5599,8 +5697,6 @@ namespace seq {
             if (c.m_complemented)
                 return (c.m_sink || c.m_state != c.m_root) ? l_true : l_false;
             return (c.m_state == c.m_root) ? l_true : l_false;
-        case mem_kind::no_loop:
-            return l_true; // guard accepts on every prefix it has not failed on
         }
         return l_undef;
     }
@@ -5630,15 +5726,6 @@ namespace seq {
             r.m_state = d;
             return r;
         }
-        case mem_kind::no_loop: {
-            if (c.m_sink) return r;                        // discharged: Σ*
-            if (!projection_state_in_Q(c.m_state->get_expr(), c.m_nu)) { r.m_sink = true; return r; }
-            euf::snode const* d = m_sg.brzozowski_deriv(c.m_state, mt);
-            if (!d || d->is_fail()) { r.m_sink = true; return r; } // lap cannot close through ∅
-            if (d == c.m_root) { r.m_dead = true; return r; }      // lap completed → forbidden
-            r.m_state = d;
-            return r;
-        }
         }
         return r;
     }
@@ -5733,9 +5820,6 @@ namespace seq {
             case mem_kind::stab_view:
                 out.push_back(prod_comp::mk_view(mem.m_regex, mem.m_root, mem.m_nu, false));
                 break;
-            case mem_kind::no_loop:
-                out.push_back(prod_comp::mk_guard(mem.m_regex, mem.m_root, mem.m_nu, mem.m_discharged));
-                break;
             }
             dep = m_dep_mgr.mk_join(dep, mem.m_dep);
             found = true;
@@ -5743,6 +5827,111 @@ namespace seq {
         return found;
     }
 
+    bool nielsen_graph::product_witness(euf::snode const* var, nielsen_node const& node,
+                                        unsigned len, zstring& out) {
+        // Shortest-accepting-word search over the product of all of var's
+        // primitive components (plain regexes AND land-state views), optionally
+        // intersected with Σ^len.  Mirrors check_product_emptiness but records
+        // the spelled word so a SAT-leaf variable pinned to a land-state view
+        // (F={s}) gets a concrete witness (ε alone is inadmissible when s≠head).
+        vector<prod_comp> comps0;
+        dep_tracker d = nullptr;
+        collect_var_components(var, node, comps0, d);
+
+        if (len != UINT_MAX) {
+            // force exact length via a Σ^len plain component
+            sort* re_sort = nullptr;
+            if (!comps0.empty() && comps0[0].m_state)
+                re_sort = comps0[0].m_state->get_expr()->get_sort();
+            if (re_sort) {
+                const expr_ref sigma_n(
+                    m_seq.re.mk_loop(m_seq.re.mk_full_char(re_sort), len, len), m);
+                comps0.push_back(prod_comp::mk_plain(m_sg.mk(sigma_n)));
+            }
+        }
+
+        if (comps0.empty()) {
+            // no constraints: any word of the requested length (default ε)
+            out = zstring();
+            for (unsigned i = 0; i < (len == UINT_MAX ? 0u : len); ++i)
+                out = out + zstring((unsigned)'a');
+            return true;
+        }
+
+        auto encode = [](vector<prod_comp> const& cs) {
+            std::vector<unsigned> key;
+            key.reserve(cs.size() * 3);
+            for (auto const& c : cs) {
+                key.push_back(static_cast<unsigned>(c.m_kind));
+                key.push_back((c.m_complemented ? 1u : 0u) | (c.m_sink ? 2u : 0u) | (c.m_dead ? 4u : 0u));
+                key.push_back(c.m_state ? c.m_state->id() : UINT_MAX);
+            }
+            return key;
+        };
+
+        std::set<std::vector<unsigned>> visited;
+        // BFS (vector + head index) for a SHORTEST accepting word.
+        vector<std::pair<vector<prod_comp>, zstring>> work;
+        work.push_back({ comps0, zstring() });
+        visited.insert(encode(comps0));
+        unsigned head = 0;
+        const unsigned MAX_STATES = 200000;
+
+        while (head < work.size()) {
+            if (!m.inc() || head >= MAX_STATES)
+                return false;
+            vector<prod_comp> cur = work[head].first;
+            zstring w = work[head].second;
+            ++head;
+
+            bool any_dead = false;
+            for (auto const& c : cur) if (c.m_dead) { any_dead = true; break; }
+            if (any_dead)
+                continue;
+
+            bool all_acc = true, any_undef = false;
+            for (auto const& c : cur) {
+                const lbool a = comp_accepting(c);
+                if (a == l_false) { all_acc = false; break; }
+                if (a == l_undef) any_undef = true;
+            }
+            if (all_acc && !any_undef) {
+                out = w;
+                return true;
+            }
+
+            expr* combined = nullptr;
+            for (auto const& c : cur) {
+                if (c.m_sink || c.m_dead) continue;
+                combined = combined ? m_seq.re.mk_inter(combined, c.m_state->get_expr())
+                                    : c.m_state->get_expr();
+            }
+            if (!combined)
+                continue;
+            euf::snode_vector mts;
+            m_sg.compute_minterms(m_sg.mk(combined), mts);
+
+            for (euf::snode const* mt : mts) {
+                char_set cs = m_seq_regex->minterm_to_char_set(mt->get_expr());
+                if (cs.is_empty())
+                    continue;
+                const unsigned ch = cs.first_char();
+                vector<prod_comp> nxt;
+                bool dead = false;
+                for (auto const& c : cur) {
+                    prod_comp e = comp_step(c, mt);
+                    if (e.m_dead) { dead = true; break; }
+                    nxt.push_back(e);
+                }
+                if (dead)
+                    continue;
+                if (visited.insert(encode(nxt)).second)
+                    work.push_back({ nxt, w + zstring(ch) });
+            }
+        }
+        return false;
+    }
+
     bool nielsen_graph::check_leaf_regex(nielsen_node const& node, dep_tracker& dep) {
         SASSERT(m_seq_regex);
 
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index e594e8a36f..1b1cb47000 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -302,15 +302,17 @@ namespace seq {
             << snode_label_html(p.deq.m_rhs, p.deq.m, false);
     }
 
-    // kind of a regex membership constraint (paper Section 3.3, "views"):
+    // kind of a regex membership constraint (paper §5.3, "land-state views"):
     //  - plain:     ordinary u ∈ r
-    //  - stab_view: stabilizer view  u ∈_{Q,{root}} root   (acceptance set F={root})
-    //  - no_loop:   cycle guard  noloop(u, root, Q)         (two-mode monitor)
-    // For view/guard, m_regex holds the *current derivative state* (a plain
-    // regex; starts at m_root) and Q is identified by the ν-index m_nu over
-    // the partial DFA (projection_state_in_Q).  This replaces the old re.proj
-    // projection operator: m_regex is always a plain regex now.
-    enum class mem_kind : unsigned char { plain, stab_view, no_loop };
+    //  - stab_view: land-state view  u ∈_{Q,{s}} r   (acceptance set F={s})
+    //               (the stabilizer is the special case s = r).
+    // For a view, m_regex holds the *current derivative state* (a plain regex;
+    // starts at the head r) and m_root holds the landing/acceptance state s.
+    // Q is identified by the ν-index m_nu over the partial DFA
+    // (projection_state_in_Q).  m_regex is always a plain regex.
+    // The old two-mode `no_loop` cycle guard has been removed: landing
+    // decomposition (paper §5.3) needs no guard.
+    enum class mem_kind : unsigned char { plain, stab_view };
 
     // regex membership constraint: str in regex
     // mirrors ZIPT's StrMem
@@ -320,11 +322,10 @@ namespace seq {
         euf::snode const* m_regex; // assumed to be non-null (plain regex = current run state)
         dep_tracker m_dep;
 
-        // view / guard annotation (Section 3.3)
+        // land-state view annotation (paper §5.3)
         mem_kind          m_kind = mem_kind::plain;
-        euf::snode const* m_root = nullptr;  // cycle head r (view F={r}; guard lap head)
+        euf::snode const* m_root = nullptr;  // landing/acceptance state s (view F={s}; stabilizer: s=head)
         unsigned          m_nu = 0;          // ν: snapshot index identifying Q
-        bool              m_discharged = false; // guard monitor: false=watch, true=discharged
 
         str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, dep_tracker const& dep):
             m(m), m_str(str), m_regex(regex), m_dep(dep) {}
@@ -336,33 +337,25 @@ namespace seq {
             m_kind = other.m_kind;
             m_root = other.m_root;
             m_nu = other.m_nu;
-            m_discharged = other.m_discharged;
             return *this;
         }
 
-        // factory for a stabilizer view  str ∈_{Q_ν,{root}} root  (m_regex=state)
+        // factory for a land-state view  str ∈_{Q_ν,{root}} state  (m_regex=state,
+        // root = landing/acceptance state s; the stabilizer is state=root=head).
         static str_mem mk_view(ast_manager& m, euf::snode const* str, euf::snode const* state,
                                euf::snode const* root, unsigned nu, dep_tracker const& dep) {
             str_mem r(m, str, state, dep);
             r.m_kind = mem_kind::stab_view; r.m_root = root; r.m_nu = nu;
             return r;
         }
-        // factory for a cycle guard  noloop(str, root, Q_ν)  (m_regex=state)
-        static str_mem mk_guard(ast_manager& m, euf::snode const* str, euf::snode const* state,
-                                euf::snode const* root, unsigned nu, dep_tracker const& dep) {
-            str_mem r(m, str, state, dep);
-            r.m_kind = mem_kind::no_loop; r.m_root = root; r.m_nu = nu;
-            return r;
-        }
 
         bool is_plain() const { return m_kind == mem_kind::plain; }
         bool is_view()  const { return m_kind == mem_kind::stab_view; }
-        bool is_guard() const { return m_kind == mem_kind::no_loop; }
 
         bool operator==(const str_mem& other) const {
             return m_str->similar(other.m_str, m) && m_regex == other.m_regex
                 && m_kind == other.m_kind && m_root == other.m_root
-                && m_nu == other.m_nu && m_discharged == other.m_discharged;
+                && m_nu == other.m_nu;
         }
 
         bool operator<(const str_mem& other) const {
@@ -747,11 +740,11 @@ namespace seq {
         // Returns proceed, conflict, satisfied, or restart.
         simplify_result simplify_and_init(ptr_vector<nielsen_edge> const& cur_path);
 
-        // Consume leading concrete/symbolic characters of a view/guard membership
-        // (Section 3.3): gate on Q_ν, step with the ordinary derivative, keeping
-        // the annotation.  Returns true if the constraint died (view left Q, or
-        // guard completed a lap) — the caller reports a regex conflict.
-        bool consume_view_guard(str_mem& mem);
+        // Consume leading concrete/symbolic characters of a land-state view
+        // membership (paper §5.3): gate on Q_ν, step with the ordinary
+        // derivative, keeping the annotation.  Returns true if the view died
+        // (left Q or derivative collapsed to ∅) — caller reports a regex conflict.
+        bool consume_view(str_mem& mem);
 
         // true if all str_eqs are trivial and there are no str_mems
         bool is_satisfied() const;
@@ -1059,6 +1052,16 @@ namespace seq {
         // path of edges from root to sat_node (set when sat_node is set)
         ptr_vector<nielsen_edge> const& sat_path() const { return m_sat_path; }
 
+        // Model construction (called by seq_model): build a concrete word for
+        // `var` satisfying ALL its primitive constraints on `node` simultaneously
+        // (plain regexes AND land-state views), by a shortest-accepting-word
+        // product search.  If len != UINT_MAX the word is forced to that exact
+        // length (Σ^len factor).  Returns true and sets `out` on success.  Used
+        // for view-constrained variables at a SAT leaf, where a land-state view
+        // (F={s}, s≠head) does not denote a plain regex and ε may be inadmissible.
+        bool product_witness(euf::snode const* var, nielsen_node const& node,
+                             unsigned len, zstring& out);
+
         // add constraints to the root node from external solver
         void add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode* l, smt::enode* r) const;
         void add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const;
@@ -1253,17 +1256,20 @@ namespace seq {
             mem_kind          m_kind = mem_kind::plain;
             bool              m_complemented = false; // ~stab co-view (kind==stab_view)
             euf::snode const* m_state = nullptr;      // current plain regex state
-            euf::snode const* m_root = nullptr;       // view/guard cycle head
+            euf::snode const* m_root = nullptr;       // land-state view acceptance state s
             unsigned          m_nu = 0;               // ν (Q snapshot)
-            bool              m_sink = false;         // co-view became Σ* / guard discharged
+            bool              m_sink = false;         // co-view became Σ*
             bool              m_dead = false;         // language collapsed to ∅
 
             static prod_comp mk_plain(euf::snode const* s) { prod_comp c; c.m_state = s; return c; }
             static prod_comp mk_view(euf::snode const* s, euf::snode const* root, unsigned nu, bool compl_) {
-                prod_comp c; c.m_kind = mem_kind::stab_view; c.m_state = s; c.m_root = root; c.m_nu = nu; c.m_complemented = compl_; return c;
-            }
-            static prod_comp mk_guard(euf::snode const* s, euf::snode const* root, unsigned nu, bool discharged) {
-                prod_comp c; c.m_kind = mem_kind::no_loop; c.m_state = s; c.m_root = root; c.m_nu = nu; c.m_sink = discharged; return c;
+                prod_comp c;
+                c.m_kind = mem_kind::stab_view;
+                c.m_state = s;
+                c.m_root = root;
+                c.m_nu = nu;
+                c.m_complemented = compl_;
+                return c;
             }
         };
 
@@ -1276,7 +1282,7 @@ namespace seq {
         prod_comp comp_step(prod_comp const& c, euf::snode const* mt);
 
         // Build the product components for variable `var` from the node's
-        // primitive memberships (plain / view / guard).  Joins their deps.
+        // primitive memberships (plain / land-state view).  Joins their deps.
         bool collect_var_components(euf::snode const* var, nielsen_node const& node,
                                     vector<prod_comp>& out, dep_tracker& dep);
 
@@ -1296,6 +1302,36 @@ namespace seq {
         // currently covered edge count for this extraction.
         unsigned mark_scc_projection_edges(uint_set const& scc);
 
+        // Landing decomposition (paper §5.3): Q is the set of explored states
+        // forward-reachable from the head r in the partial DFA G, not merely r's
+        // SCC.  These generalize the SCC helpers above.
+
+        // Collect (into Q, as expr ids) every state forward-reachable from
+        // head_re over the recorded partial-DFA edges.  Always includes head_re.
+        void collect_reachable_from_head(euf::snode const* head_re, uint_set& Q) const;
+
+        // Mark every forward-reachable edge from head_re with a monotone
+        // extraction index ν (only previously-unmarked edges), bumping ν iff
+        // something new was marked.  Returns the ν identifying this Q
+        // (0 if there is nothing marked, i.e. no reachable edge).
+        unsigned mark_reachable_projection_edges(euf::snode const* head_re);
+
+        // A frontier edge (p, mt, q): p ∈ Q, mt a minterm of p, q = δ_mt(p) ∉ Q
+        // and q ≠ ⊥.  The escape candidates of the landing decomposition.
+        struct frontier_edge {
+            euf::snode const* m_src;   // p ∈ Q
+            euf::snode const* m_mt;    // minterm
+            euf::snode const* m_dst;   // q = δ_mt(p) ∉ Q
+        };
+
+        // One lazy exploration step around Q: for each p ∈ Qstates, take every
+        // minterm derivative δ_mt(p).  If δ_mt(p) ∈ Q record the internal edge
+        // (closing cycles); otherwise (and ≠ ⊥) append it to out_frontier.
+        // Q holds expr ids (as produced by collect_reachable_from_head);
+        // Qstates are the corresponding snode handles (including the head).
+        void compute_frontier(uint_set const& Q, svector<euf::snode const*> const& Qstates,
+                              vector<frontier_edge>& out_frontier);
+
         euf::snode const* get_slice(euf::snode const* v, expr* left, expr* right);
 
         euf::snode const* get_tail(euf::snode const* v, expr* cnt, bool fwd = true);
@@ -1377,10 +1413,18 @@ namespace seq {
         // branch into s ∈ th under condition c, and s ∈ el under condition ¬c.
         bool apply_regex_if_split(nielsen_node* node);
 
-        // cycle decomposition: for a str_mem x·s ∈ R where a partial DFA
-        // cycle is detected, project SCC onto stabilizer constraint b.
-        // Rewrites x into x'·x'' with x' ∈ b*, x'' ∈ complement((b ∩ complement(eps)) · Sigma*).
-        bool apply_cycle_decomposition(nielsen_node* node);
+        // landing decomposition (paper §5.3): the core branching rule for a
+        // plain non-primitive membership x·u ∈ R (u ≠ ε, x a variable, R ground).
+        // Splits x by WHERE its value lands in the explored region Q (states
+        // forward-reachable from R):
+        //   - land-at-s (for each s ∈ Q): pin x ∈_{Q,{s}} R and advance to u ∈ s
+        //     (no split; s = R is stabilizer/cycle absorption);
+        //   - escape-via-(p,a) (for each frontier edge): x → x1·a·x2 with
+        //     x1 ∈_{Q,{p}} R, advancing to x2·u ∈ δ_a(p) and growing Q.
+        // By the frontier partition (Lemma 4.7) these branches are exhaustive and
+        // disjoint; character unwinding is the degenerate Q = {R} case.  Replaces
+        // the old split-and-guard apply_cycle_decomposition.
+        bool apply_landing_decomposition(nielsen_node* node);
 
         // cycle subsumption: for a str_mem x·rest ∈ R where x is constrained
         // to L(Reg_x) ⊆ L(stabilizer of R), simplify to rest ∈ R.
@@ -1411,14 +1455,6 @@ 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/seq_model.cpp b/src/smt/seq_model.cpp
index b27285f0eb..d527b30ba5 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -99,6 +99,7 @@ namespace smt {
         m_var_values.reset();
         m_var_replacement.reset();
         m_var_regex.reset();
+        m_view_vars.reset();
         m_trail.reset();
 
         m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model());
@@ -106,6 +107,8 @@ namespace smt {
 
         seq::nielsen_node* sat_node = nielsen.sat_node();
         SASSERT(sat_node); // in case we report sat, this has to point to a satisfied Nielsen node!
+        m_nielsen = &nielsen;
+        m_sat_node = sat_node;
         collect_var_regex_constraints(sat_node);
 
 
@@ -451,11 +454,45 @@ namespace smt {
         SASSERT(var->get_expr());
         SASSERT(m_seq.is_seq(var->get_expr()));
         auto  srt = var->get_expr()->get_sort();
-
-        // check if this variable has regex constraints
-        euf::snode const* re = nullptr;
         unsigned key = var_key(var);
-        if (m_var_regex.find(key, re) && re) {
+
+        // Land-state view (paper §5.3): the variable is pinned to L_{Q,{s}}(head),
+        // which is not a plain regex.  Build a witness by the product search over
+        // ALL of the variable's primitive constraints (view AND any plain regex).
+        // This is authoritative for a view variable — we must NOT fall through to
+        // the plain m_var_regex path below, which sees only the plain constraints
+        // and would emit a word that violates the view (unsound witness).
+        if (m_nielsen && m_sat_node && m_view_vars.contains(key)) {
+            expr_ref len_e(m_seq.str.mk_length(var->get_expr()), m);
+            rational len_val;
+            unsigned len = UINT_MAX;
+            if (get_arith_value(len_e, len_val) && len_val.is_unsigned())
+                len = len_val.get_unsigned();
+            zstring w;
+            // Try the arith-assigned length first (keeps the model length-consistent);
+            // if the view∩plain intersection has no word of that length (the arith
+            // length and the regex are only loosely coupled), retry unconstrained so
+            // the emitted word still satisfies every regex/view constraint.
+            bool ok = m_nielsen->product_witness(var, *m_sat_node, len, w);
+            if (!ok && len != UINT_MAX)
+                ok = m_nielsen->product_witness(var, *m_sat_node, UINT_MAX, w);
+            if (ok) {
+                expr* witness = m_seq.str.mk_string(w);
+                m_trail.push_back(witness);
+                m_factory->register_value(witness);
+                return witness;
+            }
+            IF_VERBOSE(1, verbose_stream() << "nseq view witness failed for "
+                << mk_pp(var->get_expr(), m) << "\n");
+            // product search exhausted: fall through only to the length fallback,
+            // never to the view-ignoring plain path (guarded by !m_view_vars below).
+        }
+
+        // check if this variable has regex constraints (non-view vars only; a view
+        // var is fully handled above — its plain constraints are already folded
+        // into the product search).
+        euf::snode const* re = nullptr;
+        if (!m_view_vars.contains(key) && m_var_regex.find(key, re) && re) {
             expr* re_expr = re->get_expr();
             SASSERT(re_expr);
 
@@ -596,11 +633,13 @@ namespace smt {
             if (mem.is_trivial(sat_node))
                 continue; // empty string in nullable regex: already satisfied, no variable to constrain
             VERIFY(mem.is_primitive()); // everything else should have been eliminated already
-            // TODO(view/guard witness): a stabilizer view / cycle guard does not
-            // denote a plain regex on the variable; for now skip it during model
-            // construction (handled by the dedicated view/guard witness below).
-            if (!mem.is_plain())
+            // A land-state view (paper §5.3) does not denote a plain regex on the
+            // variable; mark it so mk_fresh_value builds its witness via the
+            // product search (which respects the view AND any plain constraints).
+            if (!mem.is_plain()) {
+                m_view_vars.insert(var_key(mem.m_str));
                 continue;
+            }
             unsigned id = var_key(mem.m_str);
             euf::snode const* existing = nullptr;
             if (m_var_regex.find(id, existing) && existing) {
diff --git a/src/smt/seq_model.h b/src/smt/seq_model.h
index 06c24bc3c2..8e31963977 100644
--- a/src/smt/seq_model.h
+++ b/src/smt/seq_model.h
@@ -70,6 +70,15 @@ namespace smt {
         // collected during init() from the state's str_mem list.
         u_map<euf::snode const*> m_var_regex;
 
+        // variables carrying a land-state view (paper §5.3) at the SAT leaf; their
+        // witness is produced by the product search (m_nielsen->product_witness),
+        // not by some_string_in_re over a plain regex.
+        uint_set m_view_vars;
+
+        // the SAT leaf and its owning graph, captured in init() for view witnesses.
+        seq::nielsen_graph*      m_nielsen  = nullptr;
+        seq::nielsen_node const* m_sat_node = nullptr;
+
     public:
         seq_model(ast_manager& m, context& ctx, seq_util& seq,
                    seq_rewriter& rw, euf::sgraph& sg);