mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Fix well-sorted traversal lifetime bug

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-07 20:20:37 +00:00 • committed by GitHub
parent 7dfdce3fd7
commit 042bb0d6f0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/ast/well_sorted.cpp
View file

@ -36,13 +36,27 @@ struct well_sorted_proc {
well_sorted_proc(ast_manager & m):m(m), m_error(false) {}
void check(expr* e) {
for (auto term : subterms::ground(expr_ref(e, m))) {
if (is_app(term))
ptr_vector<expr> todo;
expr_mark visited;
todo.push_back(e);
while (!todo.empty()) {
expr* term = todo.back();
todo.pop_back();
if (visited.is_marked(term))
continue;
visited.mark(term, true);
if (is_app(term)) {
for (expr* arg : *to_app(term))
if (!visited.is_marked(arg))
todo.push_back(arg);
check_app(to_app(term));
else if (is_var(term))
}
else if (is_var(term)) {
check_var(to_var(term));
else if (is_quantifier(term))
}
else if (is_quantifier(term)) {
check_quantifier(to_quantifier(term));
}
}
}
@ -119,4 +133,3 @@ bool is_well_sorted(ast_manager const & m, expr * n) {
return !p.m_error;
}