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

fix #3906 by fixing a regression from today

Browse source
This commit is contained in:
Arie Gurfinkel 2020-04-11 00:18:25 -04:00
parent 136b0b23ce
commit ae5a713e81
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/muz/spacer/spacer_util.cpp
View file

@ -496,13 +496,17 @@ namespace {
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
if (m_visited.is_marked(e) || !is_app(e)) return; if (m_visited.is_marked(e) || !is_app(e)) return;
// -- keep track of all created expressions to
// -- make sure that expression ids are stable
expr_ref_vector pinned(m);
m_todo.reset(); m_todo.reset();
m_todo.push_back(e); m_todo.push_back(e);
while(!m_todo.empty()) { while(!m_todo.empty()) {
e = m_todo.back(); pinned.push_back(m_todo.back());
m_todo.pop_back(); m_todo.pop_back();
if (!is_app(e)) continue; if (!is_app(pinned.back())) continue;
app* a = to_app(e); app* a = to_app(pinned.back());
process_app(a, out); process_app(a, out);
m_visited.mark(a, true); m_visited.mark(a, true);
} }