mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

avoid crash from #4772

Browse source 
To take care of "When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults."
This commit is contained in:
Nikolaj Bjorner 2020-11-27 14:41:28 -08:00
parent 67a8492bd0
commit 35900ee8ea
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/model/model.cpp
View file

@ -451,10 +451,12 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
// only expand auxiliary definitions that occur once. // only expand auxiliary definitions that occur once.
if (can_inline_def(ts, f)) { if (can_inline_def(ts, f)) {
fi = get_func_interp(f); fi = get_func_interp(f);
if (fi) {
new_t = fi->get_array_interp(f); new_t = fi->get_array_interp(f);
TRACE("model", tout << "array interpretation:" << new_t << "\n";); TRACE("model", tout << "array interpretation:" << new_t << "\n";);
} }
} }
}
if (new_t) { if (new_t) {
// noop // noop