fix #4231

Z3Prover · May 7, 2020 · aa3749f · aa3749f
1 parent eda2eb5
commit aa3749f
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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;