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."
Z3Prover · Nov 27, 2020 · 35900ee · 35900ee
1 parent 67a8492
commit 35900ee
Showing 1 changed file with 4 additions and 2 deletions.
diff --git 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";);
+                    }
                 }
             }