From b7d7ff38cb4952f651f4954f8a6e5d732937c545 Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Fri, 22 May 2020 13:12:42 -0400 Subject: [PATCH] bug fix. Handle unknown without model (#4443) --- 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 4aa1ce645..e809a158f 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -3491,7 +3491,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r, reach_pred_used, num_reuse_reach); if (model) model->set_model_completion(false); - if (res == l_undef) res = handle_unknown(n, r, *model); + if (res == l_undef && model) res = handle_unknown(n, r, *model); checkpoint (); IF_VERBOSE (1, verbose_stream () << "." << std::flush;);