From 130a0c4aa0587ab679ec6fa5ea3b57f843f91373 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 6 Jan 2022 08:34:45 -0800
Subject: [PATCH] resurrect infinitesimals from maximization function #5720

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_solver.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 39a7bb032..f184a818c 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -259,6 +259,9 @@ namespace opt {
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
 
+        if (val > m_objective_values[i])
+            m_objective_values[i] = val;            
+
         //
         // retrieve value of objective from current model and update 
         // current optimal.
@@ -267,7 +270,7 @@ namespace opt {
             rational r;
             expr_ref value = (*m_last_model)(m_objective_terms.get(i));
             if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i])
-                m_objective_values[i] = inf_eps(r);            
+                m_objective_values[i] = inf_eps(r);   
         };
 
         update_objective();