From a19e469cc207e7aba6b0b7f5107422382f9405fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Apr 2021 13:27:41 -0700
Subject: [PATCH] fix #5212

---
 src/opt/opt_solver.cpp | 22 +++++++++++++---------
 src/opt/opt_solver.h   |  4 ++--
 src/opt/optsmt.cpp     |  6 ++++--
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 658c95ed9..42a92e128 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -202,12 +202,14 @@ namespace opt {
         return r;
     }
 
-    void opt_solver::maximize_objectives(expr_ref_vector& blockers) {
+    bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
         expr_ref blocker(m);
         for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
-            maximize_objective(i, blocker);
+            if (!maximize_objective(i, blocker))
+                return false;
             blockers.push_back(blocker);
         }
+        return true;
     }
 
     lbool opt_solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
@@ -238,7 +240,7 @@ namespace opt {
        Precondition: the state of the solver is satisfiable and such that a current model can be extracted.
        
     */
-    void opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
+    bool opt_solver::maximize_objective(unsigned i, expr_ref& blocker) {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         m_last_model = nullptr;
@@ -256,8 +258,9 @@ namespace opt {
             SASSERT(has_shared);
             decrement_value(i, val);
             if (l_true != m_context.check(0, nullptr))  
-                throw default_exception("maximization suspended");
-            m_context.get_model(m_last_model);            
+                return false;
+            m_context.get_model(m_last_model);      
+            return true;
         };
 
         if (!val.is_finite()) {
@@ -268,15 +271,15 @@ namespace opt {
             m_last_model = nullptr;
             m_context.get_model(m_last_model);
             if (has_shared && val != current_objective_value(i)) {
-                decrement();
+                if (!decrement())
+                    return false;
             }
             else {
                 m_models.set(i, m_last_model.get());
             }
         }
-        else {
-            decrement();
-        }
+        else if (!decrement())
+            return false;
         m_objective_values[i] = val;
         TRACE("opt", { 
                 tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
@@ -285,6 +288,7 @@ namespace opt {
                 if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); 
                 if (m_last_model) model_smt2_pp(tout << "last model:\n", m, *m_last_model, 0);
             });
+        return true;
     }
 
     lbool opt_solver::decrement_value(unsigned i, inf_eps& val) {
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index f22a90a2f..2a84734e4 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -119,8 +119,8 @@ namespace opt {
 
         smt::theory_var add_objective(app* term);
         void reset_objectives();
-        void maximize_objective(unsigned i, expr_ref& blocker);
-        void maximize_objectives(expr_ref_vector& blockers);
+        bool maximize_objective(unsigned i, expr_ref& blocker);
+        bool maximize_objectives1(expr_ref_vector& blockers);
         inf_eps const & saved_objective_value(unsigned obj_index);
         inf_eps current_objective_value(unsigned obj_index);
         model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 8c7a1c49a..f074f5fc1 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -321,7 +321,8 @@ namespace opt {
                 is_sat = m_s->check_sat(1,vars);
                 if (is_sat == l_true) {
                     disj.reset();
-                    m_s->maximize_objectives(disj);
+                    if (!m_s->maximize_objectives1(disj)) 
+                        return l_undef;
                     m_s->get_model(m_model);       
                     m_s->get_labels(m_labels);            
                     for (unsigned i = 0; i < ors.size(); ++i) {
@@ -395,7 +396,8 @@ namespace opt {
         expr_ref_vector disj(m);
         m_s->get_model(m_model);
         m_s->get_labels(m_labels);
-        m_s->maximize_objectives(disj);
+        if (!m_s->maximize_objectives1(disj))
+            return expr_ref(m.mk_true(), m);
         set_max(m_lower, m_s->get_objective_values(), disj);
         TRACE("opt", model_pp(tout << m_lower << "\n", *m_model););
         IF_VERBOSE(2, verbose_stream() << "(optsmt.lower " << m_lower << ")\n";);