From 654780bb4b2ee6a0f793aeb5fd2eaefffc296b8e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Jul 2016 09:26:01 -0700
Subject: [PATCH] check that model is availble before evaluation, issue #595

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/interp/iz3base.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 57188e5ca..100f16559 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -280,6 +280,10 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &v
     else if(vars.size()) {
         model_ref(_m);
         s.get_model(_m);
+        if (!_m.get()) {
+            SASSERT(l_undef == res);
+            throw iz3_exception("interpolation cannot proceed without a model");
+        }
         for(unsigned i = 0; i < vars.size(); i++){
             expr_ref r(m());
             _m.get()->eval(to_expr(vars[i].raw()),r,true);