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) {