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));