mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix #7268

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-08 14:50:38 -07:00
parent 6e069c1f41
commit af1f0e3184
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/model/model.cpp
View file

@ -248,6 +248,7 @@ void model::compress(bool force_inline) {
// by substituting in auxiliary definitions that can be eliminated. // by substituting in auxiliary definitions that can be eliminated.
func_decl_ref_vector pinned(m); func_decl_ref_vector pinned(m);
ptr_vector<func_decl> sorted_decls;
while (true) { while (true) {
top_sort ts(m); top_sort ts(m);
collect_deps(ts); collect_deps(ts);
@ -259,6 +260,7 @@ void model::compress(bool force_inline) {
ts.m_occur_count.reset(); ts.m_occur_count.reset();
for (func_decl * f : ts.top_sorted()) for (func_decl * f : ts.top_sorted())
collect_occs(ts, f); collect_occs(ts, f);
sorted_decls.reset();
// remove auxiliary declarations that are not used. // remove auxiliary declarations that are not used.
for (func_decl * f : ts.top_sorted()) { for (func_decl * f : ts.top_sorted()) {
@ -267,11 +269,13 @@ void model::compress(bool force_inline) {
unregister_decl(f); unregister_decl(f);
removed.insert(f); removed.insert(f);
} }
else
sorted_decls.push_back(f);
} }
std::swap(m_decls, sorted_decls);
if (removed.empty()) if (removed.empty())
break; break;
TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";); TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";);
remove_decls(m_decls, removed);
remove_decls(m_func_decls, removed); remove_decls(m_func_decls, removed);
remove_decls(m_const_decls, removed); remove_decls(m_const_decls, removed);
} }