diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b018d62c5..6e443d476 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1401,9 +1401,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     unsigned rlimit  = m_params.m_rlimit;
     scoped_watch sw(*this);
     lbool r;
+    bool was_pareto = false, was_opt = false;
 
     if (m_opt && !m_opt->empty()) {
-        bool was_pareto = false;
+        was_opt = true;
         m_check_sat_result = get_opt();
         cancel_eh<opt_wrapper> eh(*get_opt());
         scoped_ctrl_c ctrlc(eh);
@@ -1436,9 +1437,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             r = l_true;
         }
         get_opt()->set_status(r);
-        if (r != l_false && !was_pareto) {
-            get_opt()->display_assignment(regular_stream());
-        }
     }
     else if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
@@ -1465,6 +1463,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     validate_check_sat_result(r);
+    if (was_opt && r != l_false && !was_pareto) {
+        get_opt()->display_assignment(regular_stream());
+    }
+
     if (r == l_true) {
         validate_model();
         if (m_params.m_dump_models) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 1b4b1e7bc..265e3b7c8 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -167,6 +167,12 @@ namespace opt {
         m_hard_constraints.reset();
     }
 
+    void context::get_labels(svector<symbol> & r) {
+        if (m_solver) {
+            m_solver->get_labels(r);
+        }
+    }
+
     void context::set_hard_constraints(ptr_vector<expr>& fmls) {
         if (m_scoped_state.set(fmls)) {
             clear_state();
@@ -1121,16 +1127,20 @@ namespace opt {
     }
 
     void context::display_assignment(std::ostream& out) {
+        out << "(objectives\n";
         for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
             objective const& obj = m_scoped_state.m_objectives[i];
+            out << " (";
             display_objective(out, obj);
             if (get_lower_as_num(i) != get_upper_as_num(i)) {
-                out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
+                out << "  (" << get_lower(i) << " " << get_upper(i) << ")";
             }
             else {
-                out << " |-> " << get_lower(i) << "\n";
+                out << " " << get_lower(i);
             }
+            out << ")\n";
         }
+        out << ")\n";
     }
 
     void context::display_objective(std::ostream& out, objective const& obj) const {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 735dc6905..b364fe63e 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -184,7 +184,7 @@ namespace opt {
         virtual void fix_model(model_ref& _m);
         virtual void collect_statistics(statistics& stats) const;
         virtual proof* get_proof() { return 0; }
-        virtual void get_labels(svector<symbol> & r) {}
+        virtual void get_labels(svector<symbol> & r);
         virtual void get_unsat_core(ptr_vector<expr> & r) {}
         virtual std::string reason_unknown() const;