From 205d77d5919d5f3d25e68631d9a3dd2a252352b4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 3 Mar 2018 19:26:31 -0800
Subject: [PATCH] save last model to ensure it is available fixes #1514

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

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 715f45291..c5363816a 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -227,9 +227,13 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
+        get_model(m_model);
         inf_eps val2;
         m_valid_objectives[i] = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
+        if (!m_models[i]) {
+            set_model(i);
+        }
         if (m_context.get_context().update_model(has_shared)) {
             if (has_shared && val != current_objective_value(i)) {
                 decrement_value(i, val);
@@ -247,7 +251,7 @@ namespace opt {
                 tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
                 tout << "maximal value: " << val << "\n"; 
                 tout << "new condition: " << blocker << "\n";
-                model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
+                if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
     }
 
     void opt_solver::set_model(unsigned i) {
@@ -299,6 +303,7 @@ namespace opt {
 
     void opt_solver::get_model(model_ref & m) {
         m_context.get_model(m);
+        if (!m) m = m_model; else m_model = m;
     }
     
     proof * opt_solver::get_proof() {
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 41e9dee2d..ac9884770 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -73,6 +73,7 @@ namespace opt {
         filter_model_converter& m_fm;
         progress_callback * m_callback;
         symbol              m_logic;
+        model_ref           m_model;
         svector<smt::theory_var>  m_objective_vars;
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;