From cb5fb390bcf9541edccbb03471af6c2cfafbb716 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 Dec 2025 09:44:13 -0800
Subject: [PATCH] fix #8102

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 4 ++++
 src/opt/opt_context.h   | 3 ++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2892376be..2156df4c9 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -458,6 +458,7 @@ namespace opt {
 
     void context::set_model(model_ref& m) { 
         m_model = m;
+        m_model_available = true;
         opt_params optp(m_params);
         symbol prefix = optp.solution_prefix();
         bool model2console = optp.dump_models();
@@ -490,6 +491,8 @@ namespace opt {
 
 
     void context::get_model_core(model_ref& mdl) {
+        if (!m_model_available)
+            throw default_exception("model is not available");
         mdl = m_model;
         CTRACE(opt, mdl, tout << *mdl;);
         fix_model(mdl);
@@ -1730,6 +1733,7 @@ namespace opt {
         m_model.reset();
         m_model_fixed.reset();
         m_core.reset();
+        m_model_available = false;
     }
 
     void context::set_pareto(pareto_base* p) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 4b18dde51..2d6c329c0 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -186,7 +186,8 @@ namespace opt {
         map_t               m_maxsmts;
         scoped_state        m_scoped_state;
         vector<objective>   m_objectives;
-        model_ref           m_model;         
+        model_ref           m_model;     
+        bool m_model_available = false;
         model_converter_ref          m_model_converter;
         generic_model_converter_ref  m_fm;
         sref_vector<model>           m_model_fixed;