diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 45bcd7780..7103c495d 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -145,7 +145,7 @@ void func_interp::set_else(expr * e) { m_manager.dec_ref(m_else); ptr_vector args; - while (is_fi_entry_expr(e, args)) { + while (e && is_fi_entry_expr(e, args)) { TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;); insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); e = to_app(e)->get_arg(2);