diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 515edcbff..e863f4e89 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -98,13 +98,14 @@ namespace opt {
         lbool r = m_context.check(num_assumptions, assumptions);
         if (r == l_true && m_objective_enabled) {
             m_objective_values.reset();
+            smt::theory_opt& opt = get_optimizer();
             for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
                 smt::theory_var v = m_objective_vars[i];
-                bool is_bounded = get_optimizer().maximize(v);
+                bool is_bounded = opt.maximize(v);
                 if (is_bounded) {
-                    m_objective_values.push_back(get_optimizer().get_objective_value(v));
+                    m_objective_values.push_back(opt.get_objective_value(v));
                 } else {
-                    inf_eps_rational<inf_rational> r(rational(1), inf_rational(0));
+                    inf_eps r(rational(1), inf_rational(0));
                     m_objective_values.push_back(r);
                 }
             }
diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp
index 933de3201..f9ebe8b7b 100644
--- a/src/opt/optimize_objectives.cpp
+++ b/src/opt/optimize_objectives.cpp
@@ -44,6 +44,8 @@ Notes:
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
 #include "theory_arith.h"
+#include "ast_pp.h"
+#include "model_pp.h"
 
 namespace opt {
 
@@ -68,6 +70,7 @@ namespace opt {
         arith_util autil(m);
 
         opt_solver::scoped_push _push(*s);
+        opt_solver::toggle_objective _t(*s, true);
 
         for (unsigned i = 0; i < objectives.size(); ++i) {
             m_vars.push_back(s->add_objective(objectives[i].get()));
@@ -76,7 +79,6 @@ namespace opt {
         lbool is_sat = l_true;
         // ready to test: is_sat = update_upper();
         while (is_sat == l_true && !m_cancel) {
-            opt_solver::toggle_objective _t(*s, true);
             is_sat = update_lower();
         }      
         
@@ -89,12 +91,15 @@ namespace opt {
     lbool optimize_objectives::update_lower() {
         lbool is_sat = s->check_sat(0, 0); 
         if (is_sat == l_true) {
+            model_ref md;
+            s->get_model(md);
             set_max(m_lower, s->get_objective_values());
             IF_VERBOSE(1, 
                        for (unsigned i = 0; i < m_lower.size(); ++i) {
                            verbose_stream() << m_lower[i] << " ";
                        }
-                       verbose_stream() << "\n";);
+                       verbose_stream() << "\n";
+                       model_pp(verbose_stream(), *md););
             expr_ref_vector disj(m);
             expr_ref constraint(m);
             
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 179a04e9d..09ab33c93 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -979,6 +979,9 @@ namespace smt {
     template<typename Ext>
     bool theory_arith<Ext>::maximize(theory_var v) {
         bool r = max_min(v, true); 
+        if (!r && at_upper(v)) {
+            m_objective_value = get_value(v);
+        }
         return r || at_upper(v);
     }