From aa3749f678a83f717681600cf4c6c996acc6a18e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2020 10:34:38 -0700 Subject: [PATCH] fix #4231 --- src/smt/smt_context.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c0958dbfc..eac12c0d6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3646,7 +3646,10 @@ namespace smt { if (status == l_true && m_qmanager->has_quantifiers()) { // possible outcomes DONE l_true, DONE l_undef, CONTINUE mk_proto_model(); - quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); + quantifier_manager::check_model_result cmr = quantifier_manager::UNKNOWN; + if (m_proto_model.get()) { + cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); + } switch (cmr) { case quantifier_manager::SAT: return false;