mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix #7268

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-08 14:50:38 -07:00
parent 6bd9ea5006
commit fd95a0c90c
1 changed files with 5 additions and 1 deletions
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.
func_decl_ref_vector pinned(m);
ptr_vector<func_decl> sorted_decls;
while (true) {
top_sort ts(m);
collect_deps(ts);
@ -259,6 +260,7 @@ void model::compress(bool force_inline) {
ts.m_occur_count.reset();
for (func_decl * f : ts.top_sorted())
collect_occs(ts, f);
sorted_decls.reset();
// remove auxiliary declarations that are not used.
for (func_decl * f : ts.top_sorted()) {
@ -267,11 +269,13 @@ void model::compress(bool force_inline) {
unregister_decl(f);
removed.insert(f);
}
else
sorted_decls.push_back(f);
}
std::swap(m_decls, sorted_decls);
if (removed.empty())
break;
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_const_decls, removed);
}