From a32fabf5ee59cdcfa1d23cc19b8b5b9258ce6c96 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Jun 2020 12:13:39 -0700
Subject: [PATCH] fix #4403

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp | 11 +++++++++--
 src/opt/optsmt.cpp      |  5 ++++-
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8423bb1b9..d86893199 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -367,6 +367,7 @@ namespace opt {
     void context::fix_model(model_ref& mdl) {
         if (mdl && !m_model_fixed.contains(mdl.get())) {
             TRACE("opt", m_fm->display(tout << "fix-model\n");
+                  tout << *mdl << "\n";
                   if (m_model_converter) m_model_converter->display(tout););
             (*m_fm)(mdl);
             apply(m_model_converter, mdl);
@@ -482,6 +483,7 @@ namespace opt {
     lbool context::execute_box() {
         if (m_box_index < m_box_models.size()) {
             m_model = m_box_models[m_box_index];
+            CTRACE("opt", m_model, tout << *m_model << "\n";);
             ++m_box_index;           
             return l_true;
         }
@@ -505,12 +507,15 @@ namespace opt {
                 m_box_models.push_back(m_model.get());
             }
             else {
-                m_box_models.push_back(m_optsmt.get_model(j));
+                model* mdl = m_optsmt.get_model(j);
+                if (!mdl) mdl = m_model.get();
+                m_box_models.push_back(mdl);
                 ++j;
             }
         }
         if (r == l_true && !m_box_models.empty()) {
             m_model = m_box_models[0];
+            CTRACE("opt", m_model, tout << *m_model << "\n";);
         }
         return r;
     }
@@ -787,6 +792,7 @@ namespace opt {
 
     void context::normalize(expr_ref_vector const& asms) {
         expr_ref_vector fmls(m);
+        m_model_converter = nullptr;
         to_fmls(fmls);
         simplify_fmls(fmls, asms);
         from_fmls(fmls);
@@ -1248,7 +1254,7 @@ namespace opt {
             case O_MAXSMT: {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
                 for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
-                    ms.add(obj.m_terms[j].get(), obj.m_weights[j]);        
+                    ms.add(obj.m_terms.get(j), obj.m_weights[j]);        
                 }
                 break;
             }
@@ -1468,6 +1474,7 @@ namespace opt {
     void context::clear_state() {
         m_pareto = nullptr;
         m_box_index = UINT_MAX;
+        m_box_models.reset();
         m_model.reset();
         m_model_fixed.reset();
         m_core.reset();
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 8dff3f924..c8c254179 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -469,6 +469,7 @@ namespace opt {
         return l_true;
     }
 
+
     void optsmt::setup(opt_solver& solver) {
         m_s = &solver;
         solver.reset_objectives();
@@ -577,7 +578,9 @@ namespace opt {
         m_upper.reset();
         m_objs.reset();
         m_vars.reset();
-        m_model.reset();
+        m_model.reset();       
+        m_best_model = nullptr; 
+        m_models.reset();
         m_lower_fmls.reset();
         m_s = nullptr;
     }