From e527aca29619d241a869c142bf75729ef466a2b0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 6 Apr 2016 15:39:32 +0100
Subject: [PATCH] Bugfix for unspecified else-case in func_interps.

---
 src/model/func_interp.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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<expr> 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);