mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 12:13:25 +00:00
Code Activity

Fix constant element lifetime in seq monadic decomposition (#10329)

Browse source 
## 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.
This commit is contained in:
Margus Veanes 2026-07-31 13:20:44 -07:00 • committed by GitHub
parent 88612e329e
commit 784ca5eb38
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_monadic.cpp
View file

@ -426,13 +426,17 @@ bool seq_monadic::parse_term(expr* t, svector<atom>& 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;
}