From da0239d20026051cdf952725101e9639e6152e35 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 25 May 2018 21:21:27 -0700
Subject: [PATCH] fix #1655

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

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8fc74ec83..2850dd59c 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -128,7 +128,7 @@ namespace opt {
         m_optsmt(m),
         m_scoped_state(m),
         m_fm(alloc(generic_model_converter, m, "opt")),
-        m_model_fixed(false),
+        m_model_fixed(),
         m_objective_refs(m),
         m_enable_sat(false),
         m_is_clausal(false),
@@ -340,10 +340,10 @@ namespace opt {
     }
 
     void context::fix_model(model_ref& mdl) {
-        if (mdl && !m_model_fixed) {
+        if (mdl && !m_model_fixed.contains(mdl.get())) {
             (*m_fm)(mdl);
             apply(m_model_converter, mdl);
-            m_model_fixed = true;
+            m_model_fixed.push_back(mdl.get());
         }
     }
 
@@ -444,13 +444,11 @@ namespace opt {
     lbool context::execute_box() {
         if (m_box_index < m_box_models.size()) {
             m_model = m_box_models[m_box_index];
-            m_model_fixed = false;
             ++m_box_index;           
             return l_true;
         }
         if (m_box_index < m_objectives.size()) {
             m_model = nullptr;
-            m_model_fixed = false;
             ++m_box_index;
             return l_undef;
         }
@@ -475,7 +473,6 @@ namespace opt {
         }
         if (r == l_true && m_box_models.size() > 0) {
             m_model = m_box_models[0];
-            m_model_fixed = false;
         }
         return r;
     }
@@ -563,7 +560,6 @@ namespace opt {
     void context::yield() {
         SASSERT (m_pareto);
         m_pareto->get_model(m_model, m_labels);
-        m_model_fixed = false;
         update_bound(true);
         update_bound(false);
         TRACE("opt", model_smt2_pp(tout, m, *m_model.get(), 0););
@@ -1410,7 +1406,7 @@ namespace opt {
         m_pareto = nullptr;
         m_box_index = UINT_MAX;
         m_model.reset();
-        m_model_fixed = false;
+        m_model_fixed.reset();
     }
 
     void context::set_pareto(pareto_base* p) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 51ea6cc71..29b327855 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -159,7 +159,7 @@ namespace opt {
         model_ref           m_model;         
         model_converter_ref          m_model_converter;
         generic_model_converter_ref  m_fm;
-        bool                         m_model_fixed;
+        sref_vector<model>           m_model_fixed;
         unsigned                     m_model_counter;
         obj_map<func_decl, unsigned> m_objective_fns;
         obj_map<func_decl, expr*>    m_objective_orig;