From e4411265ea6c78c2aa00df9860d5b25ab47ac42d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 5 Feb 2017 17:53:44 +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 e6f342300..67fce1486 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -220,7 +220,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
     else {
         if (models_enabled) {
           model_converter2model(m, mc.get(), md);
-          (*mc)(labels, 0);
+          if (mc)
+              (*mc)(labels, 0);
         }
         reason_unknown = "incomplete";
         return l_undef;