From 0a3719447e3e3fca8095bf953fb779367c97c640 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Apr 2025 18:39:48 -0700
Subject: [PATCH] fix #7609

---
 src/api/api_goal.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index cbb67f2a2..7ef619c9b 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -158,7 +158,10 @@ extern "C" {
         model_ref new_m;
         Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         mk_c(c)->save_object(m_ref);
-        if (m) m_ref->m_model = to_model_ref(m)->copy(); 
+        if (m)
+            m_ref->m_model = to_model_ref(m)->copy();
+        else
+            m_ref->m_model = alloc(model, mk_c(c)->m());
         if (to_goal_ref(g)->mc()) 
             (*to_goal_ref(g)->mc())(m_ref->m_model);
         RETURN_Z3(of_model(m_ref));