From 784ca5eb380504bbf163e4bbeec68144372941b7 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 31 Jul 2026 13:20:44 -0700 Subject: [PATCH] Fix constant element lifetime in seq monadic decomposition (#10329) ## Summary Pin constant elements extracted while parsing sequence terms so they remain alive throughout monadic decomposition. Without these references, character ASTs could be reclaimed while still stored as raw pointers in decomposition atoms, causing assertion failures, fast-fail exits, and access violations during derivative construction. The fix eliminates 26 previously observed process failures in the regex benchmark corpus. No stack-depth bailout is needed for these failures. --- src/ast/rewriter/seq_monadic.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 3d9b11c014..1ecd0c5180 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -426,13 +426,17 @@ bool seq_monadic::parse_term(expr* t, svector& atoms, expr*& the_var) { return true; // epsilon: contributes nothing zstring s; if (u().str.is_string(t, s)) { - for (unsigned i = 0; i < s.length(); ++i) - atoms.push_back(atom{ false, nullptr, u().str.mk_char(s, i) }); + for (unsigned i = 0; i < s.length(); ++i) { + expr* elem = u().str.mk_char(s, i); + m_pin.push_back(elem); + atoms.push_back(atom{ false, nullptr, elem }); + } return true; } if (u().str.is_unit(t)) { // seq.unit of a constant element expr* elem = to_app(t)->get_arg(0); if (m.is_value(elem)) { + m_pin.push_back(elem); atoms.push_back(atom{ false, nullptr, elem }); return true; }