From 122b0fec0f873c69db421a6ec0ed935dbaf82069 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Dec 2021 12:30:29 -0800
Subject: [PATCH] fix #5710

---
 src/opt/opt_solver.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index c1a4c68a9..39a7bb032 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -342,6 +342,11 @@ namespace opt {
     }
 
     void opt_solver::get_model_core(model_ref & m) {  
+        if (m_last_model.get()) {
+            m = m_last_model.get();
+            return;
+        }
+
         for (unsigned i = m_models.size(); i-- > 0; ) {
             auto* mdl = m_models[i];
             if (mdl) {