From c0e74f946b28a83f94becab56a1565c49cb37141 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Apr 2021 12:23:01 -0700
Subject: [PATCH] patch to fix #5145

underlying issue is that model updates for multi-objective and single objective solving are too brittle to serve its use cases among different plugins.
For maxlex, the last model is always the best and it doesn't use multiple objectives.
---
 src/opt/opt_solver.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index abe256eaa..1e5941b39 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -191,6 +191,8 @@ namespace opt {
         r = adjust_result(r);
         if (r == l_true) {
             m_context.get_model(m_last_model);
+            if (m_models.size() == 1)
+                m_models.set(0, m_last_model.get());
         }
         m_first = false;
         if (dump_benchmarks()) {