From 5cff0de844998b7b20eb174560c7aed12a909af1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Apr 2018 11:19:00 -0700
Subject: [PATCH] fix #1567

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 227e14ca6..0b25a250b 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -454,6 +454,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
         func_interp* g = m_model.get_func_interp(f);
+		if (!g) return false;
         unsigned sz = g->num_entries();
         unsigned arity = f->get_arity();
         unsigned base_sz = stores.size();