Add monadic regex end-game solver

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 1a1a0632-f993-4bee-b4f8-a87f960836a1

src/ast/rewriter/seq_monadic.cpp

@@ -19,7 +19,6 @@ Abstract:
     yields the concrete element used to build a witness sequence.
 
 TODOs:
-- track unsat cores and expose them as explain functionality
 - if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead)
 - create a validation harness: expose certificates for correctness that can be checked.
 - extend with lower and upper bound constraints
@@ -419,12 +418,12 @@ lbool seq_monadic::decide_dnf(vector<disjunct> const& dnf) {
     return any_undef ? l_undef : l_false;
 }
 
-void seq_monadic::add(expr* term, expr* regex, u_dependency* d) {
+void seq_monadic::add(expr* term, expr* regex, void* d) {
     m_memberships.push_back({ expr_ref(term, m), expr_ref(regex, m), d });
     m_undo_trail.push(push_back_vector(m_memberships));
 }
 
-void seq_monadic::add_lo(expr* term, unsigned lo, u_dependency* d) {
+void seq_monadic::add_lo(expr* term, unsigned lo, void* d) {
     if (lo == 0)
         return;
     sort* re_sort = re().mk_re(term->get_sort());
@@ -435,21 +434,21 @@ void seq_monadic::add_lo(expr* term, unsigned lo, u_dependency* d) {
     add(term, regex, d);
 }
 
-void seq_monadic::add_hi(expr* term, unsigned hi, u_dependency* d) {
+void seq_monadic::add_hi(expr* term, unsigned hi, void* d) {
     sort* re_sort = re().mk_re(term->get_sort());
     expr_ref all_char(re().mk_full_char(re_sort), m);
     expr_ref regex(re().mk_loop_proper(all_char, 0, hi), m);
     add(term, regex, d);
 }
 
-void seq_monadic::add_len(expr* term, unsigned len, u_dependency* d) {
+void seq_monadic::add_len(expr* term, unsigned len, void* d) {
     sort* re_sort = re().mk_re(term->get_sort());
     expr_ref all_char(re().mk_full_char(re_sort), m);
     expr_ref regex(re().mk_loop_proper(all_char, len, len), m);
     add(term, regex, d);
 }
 
-lbool seq_monadic::decide(vector<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships) {
+lbool seq_monadic::decide(membership_vec const& memberships) {
     m_model.reset();
     if (memberships.empty())
         return l_true;                            // empty conjunction is vacuously true
@@ -487,7 +486,7 @@ lbool seq_monadic::decide(vector<std::tuple<expr_ref, expr_ref, u_dependency*>>
     return decide_dnf(combined);
 }
 
-void seq_monadic::minimize_core(vector<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships) {
+void seq_monadic::minimize_core(membership_vec const& memberships) {
     m_core.reset();
     if (!m_min_core) {
         // No minimization: the core is simply every asserted membership's dependency.
@@ -499,13 +498,10 @@ void seq_monadic::minimize_core(vector<std::tuple<expr_ref, expr_ref, u_dependen
     // Deletion-based minimization: start from the full unsat set and try to drop each
     // membership; a membership is kept only if removing it makes the set no longer
     // provably unsat.  The result is a minimal unsat subset (relevant constraints only).
-    vector<std::tuple<expr_ref, expr_ref, u_dependency*>> keep(memberships);
-    unsigned i = 0;
-    while (i < keep.size()) {
-        vector<std::tuple<expr_ref, expr_ref, u_dependency*>> trial;
-        for (unsigned j = 0; j < keep.size(); ++j)
-            if (j != i)
-                trial.push_back(keep[j]);
+    membership_vec keep(memberships);
+    for (unsigned i = 0; i < keep.size(); ) {
+        membership_vec trial(keep);
+        trial.erase(trial.begin() + i);
         if (decide(trial) == l_false)
             keep.swap(trial);                     // membership i is not needed for unsat
         else

src/ast/rewriter/seq_monadic.h

@@ -85,8 +85,9 @@ private:
     bool            m_min_core = true;      // whether check() minimizes the unsat core (else: all deps)
     obj_map<expr, expr*> m_model;           // last extracted model (var -> witness); see get_model()
     obj_map<expr, expr_ref_pair_vector*> m_cofactor_cache;  // memoizes derivative_cofactors per regex
-    vector<std::tuple<expr_ref, expr_ref, u_dependency*>> m_memberships;  // asserted (term in regex, dep) for check()
-    ptr_vector<u_dependency> m_core;        // dependencies of an unsat subset, filled by check() on l_false
+    using membership_vec = vector<std::tuple<expr_ref, expr_ref, void*>>;
+    membership_vec m_memberships;           // asserted (term in regex, dep) for check()
+    ptr_vector<void> m_core;                // dependencies of an unsat subset, filled by check() on l_false
 
     seq_util&      u() const { return m_rw.u(); }
     seq_util::rex& re() const { return m_rw.u().re; }
@@ -155,11 +156,11 @@ private:
     // Decide a CONJUNCTION of memberships jointly (the core algorithm behind check()):
     // multiplies the per-membership DNFs and decides emptiness.  Does not touch
     // m_memberships or m_core; fills m_model on l_true when model generation is enabled.
-    lbool decide(vector<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships);
+    lbool decide(membership_vec const& memberships);
 
     // Given an unsatisfiable membership set, extract a minimal unsatisfiable subset by
     // deletion and collect the (non-null) dependencies of its members into m_core.
-    void minimize_core(vector<std::tuple<expr_ref, expr_ref, u_dependency*>> const& memberships);
+    void minimize_core(membership_vec const& memberships);
 
 public:
     seq_monadic(seq_rewriter& rw, trail_stack& undo_trail,
@@ -193,16 +194,16 @@ public:
     // Assert a membership  (term in regex)  to be decided jointly by the next check().
     // `d` carries the dependency used for unsat-core tracking and may be nullptr.
     // Memberships remain asserted until the constructor-provided trail is popped.
-    void add(expr* term, expr* regex, u_dependency* d);
+    void add(expr* term, expr* regex, void* d);
 
     // Assert that `term` has at least `lo` elements.  A zero lower bound is a no-op.
-    void add_lo(expr* term, unsigned lo, u_dependency* d);
+    void add_lo(expr* term, unsigned lo, void* d);
 
     // Assert that `term` has at most `hi` elements.
-    void add_hi(expr* term, unsigned hi, u_dependency* d);
+    void add_hi(expr* term, unsigned hi, void* d);
 
     // Assert that `term` has exactly `len` elements.
-    void add_len(expr* term, unsigned len, u_dependency* d);
+    void add_len(expr* term, unsigned len, void* d);
 
     // Decide the CONJUNCTION of all memberships asserted via add() jointly: a variable
     // shared across memberships is constrained consistently (the DNFs are multiplied and
@@ -217,5 +218,5 @@ public:
 
     // Dependencies of a minimal unsatisfiable subset from the last check() that returned
     // l_false (nullptr dependencies are omitted).  Empty otherwise.
-    ptr_vector<u_dependency> const& core() const { return m_core; }
+    ptr_vector<void> const& core() const { return m_core; }
 };

src/params/smt_params_helper.pyg

@@ -141,6 +141,7 @@ def_module_params(module_name='smt',
                           ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
                           ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
+                          ('seq.regex_monadic', BOOL, False, 'use the monadic regular-expression end-game solver'),
                           ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'),
                           ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),

src/params/theory_seq_params.cpp

@@ -21,6 +21,7 @@ void theory_seq_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_split_w_len = p.seq_split_w_len();
     m_seq_validate = p.seq_validate();
+    m_seq_regex_monadic = p.seq_regex_monadic();
     m_seq_max_unfolding = p.seq_max_unfolding();
     m_seq_min_unfolding = p.seq_min_unfolding();
 }

src/params/theory_seq_params.h

@@ -24,6 +24,7 @@ struct theory_seq_params {
      */
     bool m_split_w_len = false;
     bool m_seq_validate = false;
+    bool m_seq_regex_monadic = false;
     unsigned m_seq_max_unfolding = UINT_MAX/4;
     unsigned m_seq_min_unfolding = 1;
 
@@ -33,4 +34,3 @@ struct theory_seq_params {
 
     void updt_params(params_ref const & p);
 };
-

src/smt/seq_regex.cpp

@@ -30,6 +30,7 @@ namespace smt {
         th(th),
         ctx(th.get_context()),
         m(th.get_manager()),
+        m_monadic(seq_rw(), ctx.get_trail_stack()),
         m_state_to_expr(m),
         m_state_graph(state_graph::state_pp(this, pp_state)) { }
 
@@ -41,6 +42,104 @@ namespace smt {
     arith_util& seq_regex::a() { return th.m_autil; }
     void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); }
 
+    void seq_regex::add_monadic_membership(literal lit, expr* s, expr* r) {
+        for (auto const& membership : m_monadic_memberships)
+            if (membership.m_lit == lit)
+                return;
+        m_monadic_memberships.push_back(monadic_membership(m, lit, s, r));
+        ctx.push_trail(push_back_vector(m_monadic_memberships));
+        theory_seq::dependency* dep = th.m_dm.mk_leaf(theory_seq::assumption(lit));
+        m_monadic.add(s, r, dep);
+        ctx.push_trail(value_trail<unsigned>(m_monadic_generation));
+        ++m_monadic_generation;
+        TRACE(seq_regex, tout << "monadic add " << lit << ": "
+                             << mk_pp(s, m) << " in " << mk_pp(r, m) << "\n";);
+    }
+
+    void seq_regex::propagate_accept_legacy(literal lit, expr* s, expr* r) {
+        expr_ref regex(r, m);
+        if (!m.is_value(s)) {
+            expr_ref s_approx = get_overapprox_regex(s);
+            if (!re().is_full_seq(s_approx)) {
+                regex = re().mk_inter(regex, s_approx);
+                TRACE(seq_regex, tout
+                    << "get_overapprox_regex(" << mk_pp(s, m)
+                    << ") = " << mk_pp(s_approx, m) << std::endl;);
+                STRACE(seq_regex_brief, tout
+                    << "overapprox=" << state_str(regex) << " ";);
+            }
+        }
+
+        expr_ref zero(a().mk_int(0), m);
+        expr_ref acc(sk().mk_accept(s, zero, regex), m);
+        literal acc_lit = th.mk_literal(acc);
+
+        TRACE(seq, tout << "propagate " << acc << "\n";);
+        th.add_axiom(~lit, acc_lit);
+    }
+
+    void seq_regex::enable_legacy_fallback() {
+        if (m_monadic_fallback_generation == m_monadic_generation)
+            return;
+        for (auto const& membership : m_monadic_memberships)
+            propagate_accept_legacy(membership.m_lit, membership.m_s, membership.m_re);
+        ctx.push_trail(value_trail<unsigned>(m_monadic_fallback_generation));
+        m_monadic_fallback_generation = m_monadic_generation;
+        ++th.m_stats.m_regex_monadic_fallbacks;
+    }
+
+    final_check_status seq_regex::final_check() {
+        if (!th.use_monadic_regex() || m_monadic_memberships.empty())
+            return FC_DONE;
+        if (m_monadic_fallback_generation == m_monadic_generation)
+            return FC_DONE;
+
+        if (m_monadic_assumption_generation == m_monadic_generation) {
+            for (auto const& assumption : m_monadic_assumptions) {
+                if (assumption.m_generation != m_monadic_generation)
+                    continue;
+                if (assumption.m_var->get_root() != assumption.m_witness->get_root()) {
+                    enable_legacy_fallback();
+                    return FC_CONTINUE;
+                }
+            }
+            return FC_DONE;
+        }
+
+        ++th.m_stats.m_regex_monadic_checks;
+        lbool result = m_monadic.check();
+        if (result == l_false) {
+            ++th.m_stats.m_regex_monadic_unsat;
+            theory_seq::dependency* dep = nullptr;
+            for (void* core_dep : m_monadic.core())
+                dep = th.m_dm.mk_join(dep, static_cast<theory_seq::dependency*>(core_dep));
+            th.set_conflict(dep);
+            return FC_CONTINUE;
+        }
+        if (result == l_undef) {
+            ++th.m_stats.m_regex_monadic_undef;
+            enable_legacy_fallback();
+            return FC_CONTINUE;
+        }
+
+        ++th.m_stats.m_regex_monadic_sat;
+        ctx.push_trail(value_trail<unsigned>(m_monadic_assumption_generation));
+        m_monadic_assumption_generation = m_monadic_generation;
+        for (auto const& [var, witness] : m_monadic.get_model()) {
+            enode* var_node = th.ensure_enode(var);
+            enode* witness_node = th.ensure_enode(witness);
+            if (var_node->get_root() == witness_node->get_root())
+                continue;
+            ctx.assume_eq(var_node, witness_node);
+            m_monadic_assumptions.push_back({ m_monadic_generation, var_node, witness_node });
+            ctx.push_trail(push_back_vector(m_monadic_assumptions));
+            ++th.m_stats.m_regex_monadic_assumptions;
+            TRACE(seq_regex, tout << "monadic assume "
+                                  << mk_pp(var, m) << " = " << mk_pp(witness, m) << "\n";);
+        }
+        return FC_CONTINUE;
+    }
+
     /**
      * is_string_equality holds of str.in_re s R, 
      * 
@@ -128,34 +227,10 @@ namespace smt {
             return;
         }
 
-        // Convert a non-ground sequence into an additional regex and
-        // strengthen the original regex constraint into an intersection
-        // for example:
-        //     (x ++ "a" ++ y) in b*
-        // is coverted to
-        //     (x ++ "a" ++ y) in intersect((.* ++ "a" ++ .*), b*)
-        expr_ref _r_temp_owner(m);
-        if (!m.is_value(s)) {
-            expr_ref s_approx = get_overapprox_regex(s);
-            if (!re().is_full_seq(s_approx)) {
-                r = re().mk_inter(r, s_approx);
-                _r_temp_owner = r;
-                TRACE(seq_regex, tout
-                    << "get_overapprox_regex(" << mk_pp(s, m)
-                    << ") = " << mk_pp(s_approx, m) << std::endl;);
-                STRACE(seq_regex_brief, tout
-                    << "overapprox=" << state_str(r) << " ";);
-            }
-        }
-
-        expr_ref zero(a().mk_int(0), m);
-        expr_ref acc(sk().mk_accept(s, zero, r), m);
-        literal acc_lit = th.mk_literal(acc);
-
-        TRACE(seq, tout << "propagate " << acc << "\n";);
-
-        //th.propagate_lit(nullptr, 1, &lit, acc_lit);
-        th.add_axiom(~lit, acc_lit);
+        if (th.use_monadic_regex())
+            add_monadic_membership(lit, s, r);
+        else
+            propagate_accept_legacy(lit, s, r);
     }
 
     /**

src/smt/seq_regex.h

@@ -19,6 +19,7 @@ Author:
 #include "util/scoped_vector.h"
 #include "util/state_graph.h"
 #include "ast/seq_decl_plugin.h"
+#include "ast/rewriter/seq_monadic.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_skolem.h"
 #include "smt/smt_context.h"
@@ -108,6 +109,28 @@ namespace smt {
         ast_manager&                     m;
         vector<s_in_re>                  m_s_in_re;
 
+        struct monadic_membership {
+            literal  m_lit;
+            expr_ref m_s;
+            expr_ref m_re;
+
+            monadic_membership(ast_manager& m, literal lit, expr* s, expr* re) :
+                m_lit(lit), m_s(s, m), m_re(re, m) {}
+        };
+
+        struct monadic_assumption {
+            unsigned m_generation;
+            enode*   m_var;
+            enode*   m_witness;
+        };
+
+        seq_monadic                       m_monadic;
+        vector<monadic_membership>         m_monadic_memberships;
+        svector<monadic_assumption>        m_monadic_assumptions;
+        unsigned                          m_monadic_generation = 0;
+        unsigned                          m_monadic_assumption_generation = UINT_MAX;
+        unsigned                          m_monadic_fallback_generation = UINT_MAX;
+
         /*
             state_graph for dead state detection, and associated methods
         */
@@ -188,6 +211,9 @@ namespace smt {
         }
 
         bool block_if_empty(expr* r, literal lit);
+        void add_monadic_membership(literal lit, expr* s, expr* r);
+        void propagate_accept_legacy(literal lit, expr* s, expr* r);
+        void enable_legacy_fallback();
 
     public:
 
@@ -197,6 +223,7 @@ namespace smt {
         void pop_scope(unsigned num_scopes) {}
         bool can_propagate() const { return false; }
         bool propagate() const { return false; }
+        final_check_status final_check();
 
         void propagate_in_re(literal lit);
 

src/smt/theory_seq.cpp

@@ -428,6 +428,16 @@ final_check_status theory_seq::final_check_eh(unsigned level) {
         TRACEFIN("solve_recfun");
         return FC_CONTINUE;
     }
+    switch (m_regex.final_check()) {
+    case FC_CONTINUE:
+        TRACEFIN("regex monadic");
+        return FC_CONTINUE;
+    case FC_GIVEUP:
+        TRACEFIN("regex monadic giveup");
+        return FC_GIVEUP;
+    case FC_DONE:
+        break;
+    }
     if (m_unhandled_expr) {
         TRACEFIN("give_up");
         TRACE(seq, tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
@@ -1956,6 +1966,12 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq fixed length", m_stats.m_fixed_length);
     st.update("seq int.to.str", m_stats.m_int_string);
     st.update("seq str.from_ubv", m_stats.m_ubv_string);
+    st.update("seq regex monadic checks", m_stats.m_regex_monadic_checks);
+    st.update("seq regex monadic sat", m_stats.m_regex_monadic_sat);
+    st.update("seq regex monadic unsat", m_stats.m_regex_monadic_unsat);
+    st.update("seq regex monadic undef", m_stats.m_regex_monadic_undef);
+    st.update("seq regex monadic assumptions", m_stats.m_regex_monadic_assumptions);
+    st.update("seq regex monadic fallbacks", m_stats.m_regex_monadic_fallbacks);
 }
 
 void theory_seq::init_search_eh() {

src/smt/theory_seq.h

@@ -319,6 +319,12 @@ namespace smt {
             unsigned m_propagate_contains;
             unsigned m_int_string;
             unsigned m_ubv_string;
+            unsigned m_regex_monadic_checks;
+            unsigned m_regex_monadic_sat;
+            unsigned m_regex_monadic_unsat;
+            unsigned m_regex_monadic_undef;
+            unsigned m_regex_monadic_assumptions;
+            unsigned m_regex_monadic_fallbacks;
         };
         typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
 
@@ -632,6 +638,7 @@ namespace smt {
         app* mk_value(expr* a);
 
         trail_stack& get_trail_stack() { return m_trail_stack; }
+        bool use_monadic_regex() const { return get_fparams().m_seq_regex_monadic; }
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
         void unmerge_eh(theory_var v1, theory_var v2) {}
@@ -644,4 +651,3 @@ namespace smt {
     };
 }
 
-

src/test/seq_monadic.cpp

@@ -24,6 +24,8 @@ Author:
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_monadic.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "params/smt_params.h"
+#include "smt/smt_kernel.h"
 #include <iostream>
 #include <set>
 
@@ -220,8 +222,10 @@ class seq_monadic_test {
     // collect the core ids after a check() into `ids`.
     void core_ids(std::set<unsigned>& ids) {
         ids.clear();
-        for (u_dependency* d : m_mon.core())
+        for (void* dep : m_mon.core()) {
+            u_dependency* d = static_cast<u_dependency*>(dep);
             ids.insert(d->leaf_value());
+        }
     }
 
     // Assert each membership with a distinct leaf dependency (id = its index) and expect
@@ -265,6 +269,24 @@ class seq_monadic_test {
         std::cout << "} full=" << (ok0 ? "yes" : "no") << "\n";
     }
 
+    lbool smt_check(expr_ref_vector const& assertions, bool enable_monadic = true) {
+        smt_params params;
+        params.m_seq_regex_monadic = enable_monadic;
+        smt::kernel solver(m, params);
+        for (expr* assertion : assertions)
+            solver.assert_expr(assertion);
+        return solver.check();
+    }
+
+    void check_smt(char const* name, expr_ref_vector const& assertions, lbool expected,
+                   bool enable_monadic = true) {
+        lbool got = smt_check(assertions, enable_monadic);
+        bool ok = got == expected;
+        if (!ok) ++m_fail;
+        std::cout << (ok ? "  OK   " : "  FAIL ") << name
+                  << "  got=" << s(got) << " expected=" << s(expected) << "\n";
+    }
+
 public:
     seq_monadic_test(seq_monadic::transition_mode mode) :
         m_reg(m), m_rw(m), m_mon(m_rw, m_trail, mode), u(m), m_str(m), m_re(m), m_mode(mode) {
@@ -489,6 +511,70 @@ public:
         std::cout << (zero_lo_ok ? "  OK   " : "  FAIL ")
                   << "|x| >= 0 is a no-op\n";
 
+        std::cout << "=== seq_monadic: SMT regex end-game ===\n";
+        {
+            expr_ref_vector assertions(m);
+            assertions.push_back(re().mk_in_re(x, star(alt(a, b))));
+            check_smt("enabled SAT membership", assertions, l_true);
+            check_smt("disabled legacy membership", assertions, l_true, false);
+        }
+        {
+            expr_ref_vector assertions(m);
+            expr_ref a_star(star(a), m);
+            assertions.push_back(re().mk_in_re(x, a_star));
+            assertions.push_back(re().mk_in_re(x, comp(a_star)));
+            check_smt("enabled joint UNSAT memberships", assertions, l_false);
+        }
+        {
+            expr_ref_vector assertions(m);
+            assertions.push_back(m.mk_not(re().mk_in_re(x, star(a))));
+            assertions.push_back(re().mk_in_re(x, star(a)));
+            check_smt("enabled negative membership", assertions, l_false);
+        }
+        {
+            expr_ref_vector assertions(m);
+            assertions.push_back(m.mk_eq(x, sword("aa")));
+            assertions.push_back(re().mk_in_re(x, expr_ref(re().mk_plus(a), m)));
+            check_smt("rejected witness uses legacy fallback", assertions, l_true);
+        }
+        {
+            expr_ref_vector assertions(m);
+            assertions.push_back(m.mk_eq(x, y));
+            assertions.push_back(re().mk_in_re(x, star(a)));
+            assertions.push_back(re().mk_in_re(y, expr_ref(re().mk_plus(b), m)));
+            check_smt("aliased variables use legacy fallback", assertions, l_false);
+        }
+        {
+            arith_util ar2(m);
+            sort_ref int_sort(ar2.mk_int(), m);
+            sort_ref seq_sort(u.str.mk_seq(int_sort), m);
+            sort_ref regex_sort(re().mk_re(seq_sort), m);
+            expr_ref seq_var(m.mk_const("seq_var", seq_sort), m);
+            expr_ref elem_var(m.mk_const("elem_var", int_sort), m);
+            expr_ref symbolic_unit(u.str.mk_unit(elem_var), m);
+            expr_ref term(u.str.mk_concat(seq_var, symbolic_unit), m);
+            expr_ref_vector assertions(m);
+            assertions.push_back(re().mk_in_re(term, re().mk_full_seq(regex_sort)));
+            check_smt("unsupported symbolic unit uses fallback", assertions, l_true);
+        }
+        {
+            smt_params params;
+            params.m_seq_regex_monadic = true;
+            smt::kernel solver(m, params);
+            expr_ref a_star(star(a), m);
+            solver.assert_expr(re().mk_in_re(x, a_star));
+            lbool before_push = solver.check();
+            solver.push();
+            solver.assert_expr(re().mk_in_re(x, comp(a_star)));
+            lbool in_push = solver.check();
+            solver.pop(1);
+            lbool after_pop = solver.check();
+            bool ok = before_push == l_true && in_push == l_false && after_pop == l_true;
+            if (!ok) ++m_fail;
+            std::cout << (ok ? "  OK   " : "  FAIL ")
+                      << "SMT membership trail push/pop\n";
+        }
+
         // ---- unsat cores: the extracted core must contain only constraints that
         // ---- participate in the contradiction, not independent ones.
         std::cout << "=== seq_monadic: unsat cores ===\n";