From 2b4d92821a1c333a79f652ba93d607308b5b82ae Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 27 Jun 2018 09:16:51 -0400
Subject: [PATCH] Avoid crashing on cancel

---
 src/muz/spacer/spacer_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 7b0fd8b57..3a20dc8ce 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1361,7 +1361,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
 
     if (is_sat == l_true || is_sat == l_undef) {
         if (core) { core->reset(); }
-        if (model) {
+        if (model && model->get()) {
             r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
             TRACE ("spacer", tout << "reachable "
                    << "is_concrete " << is_concrete << " rused: ";