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

fix bug in model compression that skips dependencies in function entries. Exposed in t171.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-10 11:12:26 -08:00
parent c5df6ce96e
commit 81d322b79f
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/model/model.cpp
View file

@ -277,6 +277,13 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
fi->compress(); fi->compress();
expr* e = fi->get_else(); expr* e = fi->get_else();
if (e) for_each_expr(collector, e); if (e) for_each_expr(collector, e);
unsigned num_args = fi->get_arity();
for (func_entry* fe : *fi) {
for (unsigned i = 0; i < num_args; ++i) {
for_each_expr(collector, fe->get_arg(i));
}
for_each_expr(collector, fe->get_result());
}
return s; return s;
} }