diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index f3ceee9c8..a8d6d5ebe 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1347,7 +1347,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) {
             r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
             TRACE ("spacer", tout << "reachable "
                    << "is_concrete " << is_concrete << " rused: ";