mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fix #2409

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-18 08:33:58 -07:00
parent 1fca76b0a1
commit d07f2d45e7
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/model/model.cpp
View file

@ -335,6 +335,9 @@ void model::collect_occs(top_sort& ts, func_decl* f) {
collect_occs(ts, e); collect_occs(ts, e);
for (auto const& fe : *fi) { for (auto const& fe : *fi) {
collect_occs(ts, fe->get_result()); collect_occs(ts, fe->get_result());
for (unsigned i = 0; i < fi->get_arity(); ++i) {
collect_occs(ts, fe->get_arg(i));
}
} }
} }
} }