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 #1901

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-25 17:29:09 -05:00
parent 2aeb814f4e
commit 5d06fa2347
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/model/model.cpp
View file

@ -410,8 +410,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
} }
else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) &&
fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) { fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
var_subst vs(m); var_subst vs(m, false);
// ? TBD args.reverse();
new_t = vs(fi->get_interp(), args.size(), args.c_ptr()); new_t = vs(fi->get_interp(), args.size(), args.c_ptr());
} }
#if 0 #if 0