From 5d772c1eb101e2d967103665f0e355dea5740d42 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 6 Feb 2020 01:38:59 -0800
Subject: [PATCH] retrieve model before push

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

diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index ada5d0d14..0b2ab077a 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -33,12 +33,13 @@ namespace opt {
         lbool is_sat = m_solver->check_sat(0, nullptr);
         if (is_sat == l_true) {
             {
+                m_solver->get_model(m_model);
                 solver::scoped_push _s(*m_solver.get());
                 while (is_sat == l_true) {
                     if (m.canceled()) {
                         return l_undef;
                     }
-                    m_solver->get_model(m_model);
+                    
                     m_solver->get_labels(m_labels);
                     m_model->set_model_completion(true);
                     IF_VERBOSE(1,
@@ -48,6 +49,7 @@ namespace opt {
                     // TBD: we can also use local search to tune solution coordinate-wise.
                     mk_dominates();
                     is_sat = m_solver->check_sat(0, nullptr);
+                    if (is_sat == l_true) m_solver->get_model(m_model);
                 }
             }
             if (is_sat == l_undef) {