From 35900ee8eaf890edba32ccc877830073dd9b914f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Nov 2020 14:41:28 -0800 Subject: [PATCH] avoid crash from #4772 To take care of "When I use options fp.xform.slice=false fp.xform.inline_eager=false Z3 actually seg-faults." --- src/model/model.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 647dc444f..023502485 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -451,8 +451,10 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) // only expand auxiliary definitions that occur once. if (can_inline_def(ts, f)) { fi = get_func_interp(f); - new_t = fi->get_array_interp(f); - TRACE("model", tout << "array interpretation:" << new_t << "\n";); + if (fi) { + new_t = fi->get_array_interp(f); + TRACE("model", tout << "array interpretation:" << new_t << "\n";); + } } }