diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp
index fc3ad1b91..2c4c87306 100644
--- a/src/opt/maxcore.cpp
+++ b/src/opt/maxcore.cpp
@@ -859,7 +859,7 @@ public:
         pb_util pb(m);
         expr_ref am(pb.mk_at_most_k(es, bound), m);
         expr* r = nullptr;
-        if (m_at_mostk.find(am, r))
+        if (m_at_mostk.find(am, r)) 
             return r;
         r = mk_fresh_bool("r");
         m_trail.push_back(am);
@@ -877,6 +877,7 @@ public:
     void max_resolve_rc2(exprs const& core, rational weight) {
         expr_ref_vector ncore(m);
         for (expr* f : core) {
+            ncore.push_back(mk_not(m, f));
             bound_info b;
             if (!m_bounds.find(f, b))
                 continue;
@@ -886,7 +887,6 @@ public:
             expr_ref_vector es(m, b.es.size(), b.es.data());
             expr* amk = mk_atmost(es, b.k + 1, b.weight);
             new_assumption(amk, b.weight);
-            ncore.push_back(mk_not(m, f));
             m_unfold_upper -= b.weight;
         }
         if (core.size() > 1) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 25982e89e..85835f08d 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -703,25 +703,25 @@ namespace opt {
 
     void context::update_solver() {
         sat_params p(m_params);
-        if (p.euf())
+        if (!p.euf() && (!m_enable_sat || !probe_fd())) 
+            return;
+
+        if (m_maxsat_engine != symbol("maxres") &&
+            m_maxsat_engine != symbol("rc2") &&
+            m_maxsat_engine != symbol("maxres-bin") &&
+            m_maxsat_engine != symbol("maxres-bin-delay") &&
+            m_maxsat_engine != symbol("pd-maxres") &&
+            m_maxsat_engine != symbol("bcd2") &&
+            m_maxsat_engine != symbol("sls")) {
             return;
-        if (!p.euf()) {
-            if (!m_enable_sat || !probe_fd()) {
-                return;
-            }
-            if (m_maxsat_engine != symbol("maxres") &&
-                m_maxsat_engine != symbol("pd-maxres") &&
-                m_maxsat_engine != symbol("bcd2") &&
-                m_maxsat_engine != symbol("sls")) {
-                return;
-            }
-            if (opt_params(m_params).priority() == symbol("pareto")) {
-                return;
-            }
-            if (m.proofs_enabled()) {
-                return;
-            }
         }
+        
+        if (opt_params(m_params).priority() == symbol("pareto")) 
+            return;
+        
+        if (m.proofs_enabled()) 
+            return;
+        
         m_params.set_bool("minimize_core_partial", true);
         m_params.set_bool("minimize_core", true);
         m_sat_solver = mk_inc_sat_solver(m, m_params);
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 0e5806ec0..78102eb6e 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -33,9 +33,14 @@ static void display_model(std::ostream& out) {
         return;
     model_ref mdl;
     g_opt->get_model(mdl);
-    if (mdl) {
-        model_smt2_pp(out, g_opt->get_manager(), *mdl, 0); 
-    }
+    if (mdl) 
+        model_smt2_pp(out, g_opt->get_manager(), *mdl, 0);
+}
+
+static void display_objective() {
+    if (!g_opt)
+        return;
+    std::ostream& out = std::cout;
     for (unsigned h : g_handles) {
         expr_ref lo = g_opt->get_lower(h);
         expr_ref hi = g_opt->get_upper(h);
@@ -48,14 +53,12 @@ static void display_model(std::ostream& out) {
     }
 }
 
-static void display_model() {
-    if (g_display_model)
+
+static void display_model() {    
+    if (g_display_model) 
         display_model(std::cout);
 }
 
-static void display_results() {
-    IF_VERBOSE(1, display_model(verbose_stream()));
-}
 
 static void display_statistics() {
     lock_guard lock(*display_stats_mux);
@@ -66,8 +69,6 @@ static void display_statistics() {
         double end_time = static_cast<double>(clock());
         std::cout << "time:                " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n";
     }    
-
-    display_results();
 }
 
 static void STD_CALL on_ctrl_c(int) {
@@ -136,6 +137,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
     }
     display_statistics();
     display_model();
+    display_objective();
     g_opt = nullptr;
     return 0;
 }