From 54280b6cc508d7c6ce9867a4ade36a2a2f6782a3 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 5 Feb 2017 17:20:45 +0000
Subject: [PATCH] Fixed model-converter segfault in ::check_sat. Relates to
 #881

---
 src/tactic/tactic.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 9315f73b0..e6f342300 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -200,7 +200,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
 
     if (is_decided_sat(r)) {
         if (models_enabled) {
-            (*mc)(labels, 0);
+            if (mc)
+                (*mc)(labels, 0);
             model_converter2model(m, mc.get(), md);
             if (!md) {
                 // create empty model.