mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Avoid broken stack by fix_dl_var_tactic

Browse source
This commit is contained in:
Kirill A. Korinsky 2024-08-26 12:25:07 +02:00
parent 749ea6c67c
commit 3656a26f18
No known key found for this signature in database
GPG key ID: 98D8D9867759226E
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -35,7 +35,7 @@ class fix_dl_var_tactic : public tactic {
struct failed {}; struct failed {};
ast_manager & m; ast_manager & m;
arith_util & m_util; arith_util & m_util;
expr_fast_mark1 * m_visited; expr_fast_mark1 * m_visited = nullptr;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
obj_map<app, unsigned> m_occs; obj_map<app, unsigned> m_occs;
obj_map<app, unsigned> m_non_nested_occs; obj_map<app, unsigned> m_non_nested_occs;
@ -214,8 +214,10 @@ class fix_dl_var_tactic : public tactic {
app * operator()(goal const & g) { app * operator()(goal const & g) {
try { try {
expr_fast_mark1 visited; if (m_visited != nullptr) {
m_visited = &visited; dealloc(m_visited);
}
m_visited = alloc(expr_fast_mark1);
unsigned sz = g.size(); unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
process(g.form(i)); process(g.form(i));