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: ";