diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp
index c398af53d0..9654a3fc15 100644
--- a/src/ast/rewriter/seq_monadic.cpp
+++ b/src/ast/rewriter/seq_monadic.cpp
@@ -29,19 +29,6 @@ TODOs:
   Model construction would assign values to the elements.
 - make unsat core tracking less naive by tracking dependencies at a finer grain.
 - add selective tracing TRACE(seq, ..).
-- revisit DFS to select next membership constraint to explore base on the current state.
-  In the current state include current set of variable intersection membership constraints.
-  The next membership constraint to explore is preferrably for a variable that was just
-  explored and we can check the variable intersection membership constraints if the new
-  expansion is feasible. Constant characters are consumed at the same time to also prune
-  the choice.
-- separate out "live-state" and enumerator over reachable live states:
-  - make it share live states between callers.
-  - make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states.
-  - make use of DFS exploration of derivatives to extract live states without visiting all states up front.
-  - use it in seq_regex legacy mode that also has this notion.
-
-
 
 Author:
 
@@ -71,19 +58,6 @@ namespace {
         return "unknown";
     }
 
-    char const* bail_name(unsigned i) {
-        static char const* const names[] = {
-            "unsupported",
-            "state-cap",
-            "dnf-cap",
-            "budget",
-            "resource",
-            "nullability",
-            "guard"
-        };
-        return i < std::size(names) ? names[i] : "unknown";
-    }
-
     char const* result_name(lbool r) {
         switch (r) {
         case l_true:  return "sat";
@@ -93,6 +67,24 @@ namespace {
     }
 }
 
+#define SEQ_MONADIC_BAIL_PREFIX "seq monadic bail "
+
+char const* seq_monadic::bail_stat_name(bail_reason reason) {
+    switch (reason) {
+    case bail_reason::unsupported: return SEQ_MONADIC_BAIL_PREFIX "unsupported";
+    case bail_reason::state_cap:   return SEQ_MONADIC_BAIL_PREFIX "state cap";
+    case bail_reason::budget:      return SEQ_MONADIC_BAIL_PREFIX "budget";
+    case bail_reason::resource:    return SEQ_MONADIC_BAIL_PREFIX "resource";
+    case bail_reason::nullability: return SEQ_MONADIC_BAIL_PREFIX "nullability";
+    case bail_reason::guard:       return SEQ_MONADIC_BAIL_PREFIX "guard";
+    default:                       return SEQ_MONADIC_BAIL_PREFIX "unknown";
+    }
+}
+
+char const* seq_monadic::bail_name(bail_reason reason) {
+    return bail_stat_name(reason) + (sizeof(SEQ_MONADIC_BAIL_PREFIX) - 1);
+}
+
 
 expr_ref seq_monadic::der_elem(expr* r, expr* elem) {
     expr* cached = nullptr;
@@ -515,6 +507,8 @@ unsigned seq_monadic::var_index(expr* v) {
     m_var_idx.insert(v, vi);
     m_vars.push_back(v);
     m_groups.push_back(svector<component>());
+    m_num_occ.push_back(0);
+    m_head_cnt.push_back(0);
     return vi;
 }
 
@@ -526,11 +520,15 @@ void seq_monadic::reset_search() {
     m_vars.reset();
     m_var_idx.reset();
     m_groups.reset();
-    m_last_occ.reset();
+    m_num_occ.reset();
     m_group_cache.clear();
     m_der_cache.reset();
     m_nullable_cache.reset();
     m_undef_vars = 0;
+    m_cursors.reset();
+    m_last_var = UINT_MAX;
+    m_head_cnt.reset();
+    m_head_stack.reset();
     m_live_states.reset();
 }
 
@@ -554,17 +552,12 @@ bool seq_monadic::prepare(membership_vec const& memberships) {
         m_atoms.push_back(atoms);
         m_pin.push_back(regex);
     }
-    // A variable's component group is complete once the search passes the variable's
-    // last occurrence; positions are compared in search order, i.e. lexicographically
-    // on (membership index, atom index).
     for (unsigned mi = 0; mi < m_atoms.size(); ++mi) {
         vector<atom> const& atoms = m_atoms[mi];
-        for (unsigned i = 0; i < atoms.size(); ++i) {
-            if (!atoms[i].is_var)
+        for (atom const& a : atoms) {
+            if (!a.is_var)
                 continue;
-            expr* v = atoms[i].var.get();
-            var_index(v);
-            m_last_occ.insert(v, (static_cast<uint64_t>(mi) << 32) | i);
+            ++m_num_occ[var_index(a.var.get())];
         }
     }
     return true;
@@ -618,6 +611,23 @@ lbool seq_monadic::leaf() {
     return l_true;
 }
 
+bool seq_monadic::inc_budget() {
+    if (m_giveup)
+        return false;                             // unwind the whole search, don't keep branching
+    if (m_budget == 0) {
+        m_stats.inc_bail(bail_reason::budget);
+        m_giveup = true;
+        return false;
+    }
+    if (!m.inc()) {
+        m_stats.inc_bail(bail_reason::resource);
+        m_giveup = true;
+        return false;
+    }
+    --m_budget;
+    return true;
+}
+
 lbool seq_monadic::dfs_membership(unsigned mi) {
     if (mi == m_atoms.size())
         return leaf();
@@ -625,19 +635,8 @@ lbool seq_monadic::dfs_membership(unsigned mi) {
 }
 
 lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
-    if (m_giveup)
-        return l_undef;                           // unwind the whole search, don't keep branching
-    if (m_budget == 0) {
-        m_stats.inc_bail(bail_reason::budget);
-        m_giveup = true;
+    if (!inc_budget())
         return l_undef;
-    }
-    if (!m.inc()) {
-        m_stats.inc_bail(bail_reason::resource);
-        m_giveup = true;
-        return l_undef;
-    }
-    --m_budget;
     vector<atom> const& atoms = m_atoms[mi];
     if (i == atoms.size()) {                      // the rest of this membership is epsilon
         lbool nb = nullable(R);
@@ -653,7 +652,6 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
         expr_ref d = der_elem(R, a.elem.get());
         if (re().is_empty(d))
             return l_false;
-        m_pin.push_back(d);
         return dfs_atoms(mi, i + 1, d);
     }
 
@@ -661,9 +659,6 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
     // the derivative automaton from R to some live state q, which splits the search.
     bool last_atom = (i + 1 == atoms.size());
     unsigned vi = var_index(a.var.get());
-    uint64_t pos = (static_cast<uint64_t>(mi) << 32) | i;
-    uint64_t last = 0;
-    bool finalize = m_last_occ.find(a.var.get(), last) && last == pos;
 
     // Explores one split target; the caller stops at the first l_true.
     auto explore = [&](expr* target) -> lbool {
@@ -674,7 +669,7 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
         lbool ne = l_true;
         if (re().is_empty(R))
             ne = l_false;
-        else if (finalize || m_groups[vi].size() > 1)
+        else if (group_complete(vi) || m_groups[vi].size() > 1)
             ne = group_nonempty(vi);
         lbool r;
         if (ne == l_false)
@@ -719,7 +714,182 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) {
     return any_undef ? l_undef : l_false;
 }
 
-lbool seq_monadic::decide(membership_vec const& memberships) {
+// ---- state-based search driver ------------------------------------------------------
+//
+// This is an alternative to the strictly positional dfs_membership/dfs_atoms above.  The
+// positional search finishes membership 0 entirely, then membership 1, and so on, so two
+// memberships that share a variable only intersect that variable's components deep in the
+// tree -- after the first membership's alignment was chosen blindly.  The state-based
+// search keeps a *cursor* per membership and, at each step, expands ONE variable across
+// ALL memberships whose current head is that variable, intersecting the per-variable
+// components (m_groups) immediately.  An infeasible choice for a shared variable is thus
+// pruned as soon as it is made, rather than after committing to a full membership.
+//
+// A search state is:
+//   - the set of active (non-complete) cursors      == active membership constraints,
+//   - the per-variable component groups (m_groups)  == variable intersection constraints,
+//   - the last expanded variable (m_last_var)       == locality hint for the next choice.
+// Every non-complete cursor has a variable head (leading constants are eagerly consumed by
+// consume_constants).  The state is complete when every cursor is complete, and accepting
+// when additionally every variable group is non-empty.
+
+lbool seq_monadic::consume_constants(cursor& c, unsigned mi) {
+    vector<atom> const& atoms = m_atoms[mi];
+    while (c.i < atoms.size() && !atoms[c.i].is_var) {
+        expr_ref d = der_elem(c.R, atoms[c.i].elem.get());
+        if (re().is_empty(d))
+            return l_false;                        // dead: this continuation is empty
+        c.R = d;
+        c.i += 1;
+    }
+    c.complete = (c.i == atoms.size());
+    if (!c.complete)
+        return l_true;                             // stopped on a variable head
+    lbool nb = nullable(c.R);                      // the remaining tail is epsilon
+    if (nb == l_false)
+        return l_false;
+    if (nb == l_undef) {
+        m_stats.inc_bail(bail_reason::nullability);
+        return l_undef;                            // tail nullability undecidable
+    }
+    return l_true;
+}
+
+lbool seq_monadic::advance_cursor(cursor& c, unsigned mi, expr* target) {
+    // Step past the head variable.  target == null encodes "the variable is the last atom",
+    // i.e. a plain membership component: nothing follows, the cursor is complete.
+    if (!target) {
+        c.i = m_atoms[mi].size();
+        c.complete = true;
+        return l_true;
+    }
+    c.i += 1;
+    c.R = target;
+    return consume_constants(c, mi);
+}
+
+lbool seq_monadic::search() {
+    if (!inc_budget())
+        return l_undef;
+
+    unsigned best_vi = UINT_MAX, best_cnt = 0;
+    for (unsigned mi = 0; mi < m_cursors.size(); ++mi) {
+        cursor const& c = m_cursors[mi];
+        if (c.complete)
+            continue;
+        unsigned vi = m_var_idx[m_atoms[mi][c.i].var.get()];
+        unsigned cnt = ++m_head_cnt[vi];
+        // Prefer the most frequent head variable; break ties toward the smallest index so
+        // the choice is deterministic.  m_last_var (locality) is applied afterwards.
+        if (cnt > best_cnt || (cnt == best_cnt && vi < best_vi)) {
+            best_cnt = cnt;
+            best_vi = vi;
+        }
+    }
+
+    // Locality: if the last expanded variable is still an active head, expand it next --
+    // its freshly chosen continuation can be checked against the intersection immediately.
+    unsigned vi = best_vi;
+    if (best_vi != UINT_MAX && m_last_var != UINT_MAX && m_head_cnt[m_last_var] > 0)
+        vi = m_last_var;
+
+    // All cursors whose current head is variable vi are expanded together at this step.
+    unsigned s_offset = m_head_stack.size(), s_size = 0;
+    for (unsigned mi = 0; mi < m_cursors.size(); ++mi) {
+        cursor const& c = m_cursors[mi];
+        if (c.complete)
+            continue;
+        unsigned hv = m_var_idx[m_atoms[mi][c.i].var.get()];
+        m_head_cnt[hv] = 0;
+        if (hv == vi) {
+            m_head_stack.push_back(mi);
+            ++s_size;
+        }
+    }
+    if (best_vi == UINT_MAX)
+        return leaf();                             // every cursor complete
+
+    lbool r = choose_cont(vi, s_offset, s_size, 0);
+    m_head_stack.shrink(s_offset);
+    return r;
+}
+
+lbool seq_monadic::choose_cont(unsigned vi, unsigned s_offset, unsigned s_size, unsigned k) {
+    if (!inc_budget())
+        return l_undef;
+    if (k == s_size) {
+        unsigned saved = m_last_var;
+        m_last_var = vi;
+        lbool r = search();
+        m_last_var = saved;
+        return r;
+    }
+    unsigned mi = m_head_stack[s_offset + k];
+    cursor& c = m_cursors[mi];
+    vector<atom> const& atoms = m_atoms[mi];
+    expr* R = c.R;
+    expr* v = atoms[c.i].var.get();
+    bool last_atom = (c.i + 1 == atoms.size());
+
+    auto explore = [&](expr* target) -> lbool {
+        m_groups[vi].push_back(component{ v, R, target });
+        // Intersect immediately: prune as soon as vi's accumulated components are empty.
+        // The test is forced once the group is complete so the accepting state does not
+        // need to re-verify; running it earlier (size > 1) prunes.
+        lbool ne;
+        if (re().is_empty(R))
+            ne = l_false;
+        else if (group_complete(vi) || m_groups[vi].size() > 1)
+            ne = group_nonempty(vi);
+        else
+            ne = l_true;
+        if (ne == l_false) {
+            m_groups[vi].pop_back();
+            return l_false;                        // infeasible continuation for vi: prune
+        }
+        cursor saved = c;                          // save/restore cursor across the branch
+        lbool adv = advance_cursor(c, mi, target);
+        if (adv == l_false) {
+            c = saved;
+            m_groups[vi].pop_back();
+            return l_false;
+        }
+        unsigned undef_here = (ne == l_undef ? 1u : 0u) + (adv == l_undef ? 1u : 0u);
+        m_undef_vars += undef_here;
+        lbool r = choose_cont(vi, s_offset, s_size, k + 1);
+        m_undef_vars -= undef_here;
+        c = saved;
+        m_groups[vi].pop_back();
+        return r;
+    };
+
+    // A last variable contributes a plain membership component. Otherwise consume live
+    // split states lazily so an early satisfying continuation avoids expanding the rest.
+    if (last_atom)
+        return explore(nullptr);
+
+    bool any_undef = false;
+    auto live = m_live_states.reachable_live(R);
+    for (expr* target : live) {
+        lbool r = explore(target);
+        if (r == l_true)
+            return l_true;
+        if (r == l_undef) {
+            if (m_giveup)
+                return l_undef;
+            any_undef = true;
+        }
+    }
+    if (live.failed()) {
+        m_stats.inc_bail(
+            live.failure_reason() == seq::live_states::failure::state_cap ?
+            bail_reason::state_cap : bail_reason::resource);
+        return l_undef;
+    }
+    return any_undef ? l_undef : l_false;
+}
+
+lbool seq_monadic::decide(membership_vec const& memberships, bool core_trial) {
     m_last_search_memberships = memberships;
     m_model.reset();
     reset_search();                               // clear the caches before dropping the
@@ -727,13 +897,50 @@ lbool seq_monadic::decide(membership_vec const& memberships) {
     m_rp_cache.maybe_reset(1u << 16);
     reset_ivl_cache();
     m_rw.get_derive().maybe_reset_cached_cofactors(1u << 16);
-    m_budget = 200000;
+    constexpr unsigned state_search_budget = 200000;
+    constexpr unsigned positional_search_budget = 200000;
+    constexpr unsigned extended_positional_search_budget = 1000000;
+    m_budget = m_config.m_state_search ? state_search_budget : positional_search_budget;
     m_giveup = false;
     lbool r = l_true;                             // empty conjunction is vacuously true
     if (!memberships.empty() && !prepare(memberships))
         r = l_undef;
-    else if (!memberships.empty())
-        r = dfs_membership(0);
+    else if (!memberships.empty()) {
+        if (m_config.m_state_search) {
+            // Build one cursor per membership at its regex start; consuming the leading
+            // constants leaves every active cursor on a variable head.
+            m_cursors.reset();
+            m_last_var = UINT_MAX;
+            for (unsigned mi = 0; mi < m_atoms.size() && r != l_false; ++mi) {
+                m_cursors.push_back(cursor{ 0, m_regexes.get(mi), false });
+                r = consume_constants(m_cursors.back(), mi);
+                if (r == l_undef)
+                    ++m_undef_vars;
+            }
+            if (r != l_false)
+                r = search();
+
+            // State search and positional DFS have complementary good orderings.
+            // If state search exhausts its private work budget, retry from a clean
+            // search state. The extended retry is reserved for conjunctions with enough
+            // independent intersections to justify delaying the legacy solver.
+            bool use_portfolio = memberships.size() >= m_vars.size() + 2;
+            if (!core_trial && r == l_undef && m_giveup && m_budget == 0) {
+                m_giveup = false;
+                m_budget = positional_search_budget;
+                if (prepare(memberships))
+                    r = dfs_membership(0);
+            }
+            if (!core_trial && use_portfolio && r == l_undef && m_giveup && m_budget == 0) {
+                m_giveup = false;
+                m_budget = extended_positional_search_budget;
+                if (prepare(memberships))
+                    r = dfs_membership(0);
+            }
+        }
+        else
+            r = dfs_membership(0);
+    }
     if (r != l_true)
         m_model.reset();
     m_last_search_result = r;
@@ -831,7 +1038,7 @@ void seq_monadic::minimize_core(membership_vec const& memberships) {
     for (unsigned i = 0; i < keep.size(); ) {
         membership_vec trial(keep);
         trial.erase(trial.begin() + i);
-        if (decide(trial) == l_false)
+        if (decide(trial, true) == l_false)
             keep.swap(trial);                     // membership i is not needed for unsat
         else
             ++i;                                  // membership i is needed; keep it
@@ -864,6 +1071,7 @@ std::ostream& seq_monadic::display(std::ostream& out) const {
         << "  :mode " << mode_name(m_config.m_mode) << "\n"
         << "  :generate-model " << (m_config.m_model ? "true" : "false") << "\n"
         << "  :minimize-core " << (m_config.m_min_core ? "true" : "false") << "\n"
+        << "  :state-search " << (m_config.m_state_search ? "true" : "false") << "\n"
         << "  :last-result " << result_name(m_last_result) << "\n"
         << "  :budget " << m_budget << "\n"
         << "  :giveup " << (m_giveup ? "true" : "false") << "\n"
@@ -921,6 +1129,9 @@ std::ostream& seq_monadic::display(std::ostream& out) const {
         out << " ";
         display_expr(var);
     }
+    out << " )\n     :variable-occurrences (";
+    for (unsigned n : m_num_occ)
+        out << " " << n;
     out << " )\n     :parsed-memberships (";
     for (unsigned mi = 0; mi < m_atoms.size(); ++mi) {
         out << "\n       [" << mi << "] :regex ";
@@ -965,25 +1176,14 @@ std::ostream& seq_monadic::display(std::ostream& out) const {
         << "     :pinned-expressions " << m_pin.size() << ")\n";
 
     out << "  :statistics\n"
-        << "    (:cofactor-calls " << m_stats.m_cofactor_calls << "\n"
-        << "     :states " << m_stats.m_states;
+        << "    (:cofactor-calls " << m_stats.m_cofactor_calls;
     for (unsigned i = 0; i < static_cast<unsigned>(bail_reason::num_reasons); ++i)
-        out << "\n     :bail-" << bail_name(i) << " " << m_stats.m_bails[i];
+        out << "\n     :bail-" << bail_name(static_cast<bail_reason>(i)) << " " << m_stats.m_bails[i];
     return out << "))\n";
 }
 
 void seq_monadic::collect_statistics(::statistics& st) const {
-    static char const* const bail_names[] = {
-        "seq monadic bail unsupported",
-        "seq monadic bail state cap",
-        "seq monadic bail dnf cap",
-        "seq monadic bail budget",
-        "seq monadic bail resource",
-        "seq monadic bail nullability",
-        "seq monadic bail guard"
-    };
     st.update("seq monadic cofactor calls", m_stats.m_cofactor_calls);
-    st.update("seq monadic states", m_stats.m_states);
     for (unsigned i = 0; i < static_cast<unsigned>(bail_reason::num_reasons); ++i)
-        st.update(bail_names[i], m_stats.m_bails[i]);
+        st.update(bail_stat_name(static_cast<bail_reason>(i)), m_stats.m_bails[i]);
 }
diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h
index c878a8b40e..aeb71c40a5 100644
--- a/src/ast/rewriter/seq_monadic.h
+++ b/src/ast/rewriter/seq_monadic.h
@@ -84,15 +84,20 @@ class seq_monadic {
         seq::transition_mode m_mode;
         bool m_model = true;  // whether solve()/check() extract a feasible model
         bool m_min_core = true;   // whether check() minimizes the unsat core (else: all deps)
+        bool m_state_search = true;  // use the state-based search driver (select next
+                                     // membership by the last-expanded / most-frequent
+                                     // head variable) instead of the positional DFS
 
         config(seq::transition_mode mode) : m_mode(mode) {}
     };
 
-    enum class bail_reason { unsupported, state_cap, dnf_cap, budget, resource, nullability, guard, num_reasons };
+    enum class bail_reason { unsupported, state_cap, budget, resource, nullability, guard, num_reasons };
+
+    static char const* bail_stat_name(bail_reason reason);
+    static char const* bail_name(bail_reason reason);
 
     struct statistics {
         unsigned m_cofactor_calls = 0;
-        unsigned m_states = 0;
         unsigned m_bails[static_cast<unsigned>(bail_reason::num_reasons)] = {};
 
         void inc_bail(bail_reason reason) {
@@ -164,7 +169,7 @@ class seq_monadic {
     ptr_vector<expr>       m_vars;          // variables occurring in the memberships
     obj_map<expr, unsigned> m_var_idx;      // variable -> index into m_vars / m_groups
     vector<svector<component>> m_groups;    // components accumulated on the current branch
-    obj_map<expr, uint64_t> m_last_occ;     // variable -> last (membership, atom) position
+    svector<unsigned>      m_num_occ;
     unsigned               m_undef_vars = 0;  // depth of groups whose emptiness test gave up
     // memo for the per-variable emptiness test, keyed by the sorted, deduplicated
     // (state, target) signature of the variable's component group
@@ -183,6 +188,20 @@ class seq_monadic {
     std::unordered_map<group_sig, lbool, group_sig_hash> m_group_cache;
     seq::live_states m_live_states;
 
+    // ---- state-based search driver (see the "search state" note in the .cpp) ----
+    // A membership cursor: how far membership `mi` has been consumed on the current
+    // branch.  `i` is the next unconsumed atom, `R` the derivative state of the regex
+    // after the consumed prefix, `complete` once every atom is consumed (and the tail is
+    // known nullable / covered by a membership component).  The set of non-complete
+    // cursors is the "set of active membership constraints"; each non-complete cursor has
+    // a *variable* head (leading constants are eagerly consumed).  The per-variable
+    // component groups (m_groups) are the "variable intersection membership constraints".
+    struct cursor { unsigned i; expr* R; bool complete; };
+    svector<cursor> m_cursors;              // one cursor per membership (parallel to m_atoms)
+    unsigned        m_last_var = UINT_MAX;  // index (in m_vars) of the last expanded variable
+    unsigned_vector m_head_cnt;
+    unsigned_vector m_head_stack;
+
     // Brzozowski derivative of regex `r` by the concrete element `elem`.  Memoized on
     // (r, elem): the search revisits the same constant step on many branches.
     expr_ref der_elem(expr* r, expr* elem);
@@ -208,11 +227,13 @@ class seq_monadic {
     // Drop all search state accumulated by the previous decide()/solve().
     void reset_search();
 
-    // Parse every membership into atoms, register its variables and record each
-    // variable's last occurrence.  Sets m_seq_sort/m_elem_sort.  False on an
+    // Parse every membership into atoms, register its variables and count each
+    // variable's occurrences.  Sets m_seq_sort/m_elem_sort.  False on an
     // unsupported shape.
     bool prepare(membership_vec const& memberships);
 
+    bool group_complete(unsigned vi) const { return m_groups[vi].size() == m_num_occ[vi]; }
+
     // Index of `v` in m_vars / m_groups, registering it on first sight.
     unsigned var_index(expr* v);
 
@@ -224,6 +245,31 @@ class seq_monadic {
     lbool dfs_membership(unsigned mi);
     lbool dfs_atoms(unsigned mi, unsigned i, expr* R);
 
+    // ---- state-based search driver ----------------------------------------------------
+    bool inc_budget();
+
+    // One search step: pick the next variable to expand (preferring the last-expanded
+    // variable, else the one occurring most often as a head atom of the active cursors),
+    // and expand it.  Returns l_true (sat leaf found), l_false (this branch is empty), or
+    // l_undef (gave up on a sub-branch).
+    lbool search();
+
+    // Expand variable `vi`, which is the head of the cursors in
+    // m_head_stack[s_offset .. s_offset + s_size).  Assign a continuation (a reach target
+    // q, or the epsilon/membership encoding for a last atom) to each cursor in turn (k
+    // indexes the set), pushing the component on m_groups[vi] and pruning as soon as the
+    // accumulated intersection for vi is empty.  When every cursor is assigned, recurse
+    // into search().
+    lbool choose_cont(unsigned vi, unsigned s_offset, unsigned s_size, unsigned k);
+
+    lbool consume_constants(cursor& c, unsigned mi);
+
+    // Advance cursor `mi` past its head variable to continuation `target` (null = the
+    // variable is a last atom, i.e. a plain membership component), then eagerly consume
+    // the following constant atoms.  l_false = the continuation is empty (prune),
+    // l_undef = feasible but the tail nullability is unknown, l_true = feasible.
+    lbool advance_cursor(cursor& c, unsigned mi, expr* target);
+
     // Emptiness of the components accumulated for variable `vi` on the current branch,
     // memoized on their signature.  Duplicated components are collapsed before the
     // product search (they constrain the variable identically).
@@ -238,8 +284,9 @@ class seq_monadic {
     // by several memberships accumulates several components in the same branch, which are
     // intersected -- enforcing one consistent value across all memberships.  Does not
     // touch m_memberships or m_core; fills m_model on l_true when model generation is
-    // enabled.
-    lbool decide(membership_vec const& memberships);
+    // enabled. Core-minimization trials skip the search portfolio because l_undef safely
+    // keeps the candidate dependency in the core.
+    lbool decide(membership_vec const& memberships, bool core_trial = false);
 
     // Given an unsatisfiable membership set, extract a minimal unsatisfiable subset by
     // deletion and collect the (non-null) dependencies of its members into m_core.
@@ -284,6 +331,9 @@ public:
     // returns the dependencies of all asserted memberships (no deletion-based shrinking).
     void set_min_core(bool b) { m_config.m_min_core = b; }
 
+    void set_state_search(bool b) { m_config.m_state_search = b; }
+    bool state_search() const { return m_config.m_state_search; }
+
     void set_is_var(std::function<bool(expr *)> const &is_var) {
         m_is_var = is_var;
     }
diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp
index 65867ac4ad..4082854045 100644
--- a/src/test/seq_monadic.cpp
+++ b/src/test/seq_monadic.cpp
@@ -29,6 +29,7 @@ Author:
 #include <iostream>
 #include <sstream>
 #include <set>
+#include <functional>
 
 namespace {
 
@@ -126,9 +127,28 @@ class seq_monadic_test {
                   << mode_name() << " cofactor construction\n";
     }
 
+    lbool run_both_drivers(char const* name, std::function<lbool()> const& query) {
+        bool saved = m_mon.state_search();
+        m_mon.set_state_search(true);
+        lbool a = query();
+        m_mon.set_state_search(false);
+        lbool b = query();
+        m_mon.set_state_search(saved);
+        if (a != b && a != l_undef && b != l_undef) {
+            ++m_fail;
+            std::cout << "  FAIL " << name << "  drivers contradict: state=" << s(a)
+                      << " positional=" << s(b) << "\n";
+        }
+        else if (a != b) {
+            std::cout << "  NOTE " << name << "  state=" << s(a)
+                      << " positional=" << s(b) << " (one gave up)\n";
+        }
+        return a;
+    }
+
     void check(char const* name, expr* term, expr* R, lbool expected) {
         m_mon.set_gen_model(false);               // this check does not use the model
-        lbool got = m_mon.solve(term, R);
+        lbool got = run_both_drivers(name, [&]() { return m_mon.solve(term, R); });
         bool ok = (got == expected);
         if (!ok) ++m_fail;
         std::cout << (ok ? "  OK   " : "  FAIL ") << name
@@ -148,7 +168,7 @@ class seq_monadic_test {
         m_trail.push_scope();
         add_extra(term, R, ve);
         m_mon.set_gen_model(false);               // this check does not use the model
-        lbool got = m_mon.check();
+        lbool got = run_both_drivers(name, [&]() { return m_mon.check(); });
         m_trail.pop_scope(1);
         bool ok = (got == expected);
         if (!ok) ++m_fail;