diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index f8a26d687..e72223118 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -53,7 +53,7 @@ namespace opt {
         if (m_msolver) {
             m_msolver->updt_params(m_params);
             is_sat = (*m_msolver)();
-            if (is_sat == l_true) {
+            if (is_sat != l_false) {
                 m_msolver->get_model(m_model);
             }
         }
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 88cfd20dd..7a87ac6ca 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -295,18 +295,7 @@ public:
         switch(r) {
         case l_true: {
             ctx.regular_stream() << "sat\n";
-            opt.display_assignment(ctx.regular_stream());
-            opt_params optp(p);
-            if (optp.print_model()) {
-                model_ref mdl;
-                opt.get_model(mdl);
-                if (mdl) {
-                    ctx.regular_stream() << "(model " << std::endl;
-                    model_smt2_pp(ctx.regular_stream(), ctx, *(mdl.get()), 2);
-                    // m->display(ctx.regular_stream());
-                    ctx.regular_stream() << ")" << std::endl;                    
-                }
-            }
+            display_result(ctx);
             break;
         }
         case l_false:
@@ -314,13 +303,30 @@ public:
             break;
         case l_undef:
             ctx.regular_stream() << "unknown\n";
-            opt.display_assignment(ctx.regular_stream());
+            display_result(ctx);
             break;
         }
         if (p.get_bool("print_statistics", false)) {
             display_statistics(ctx);
         }
     }
+
+    void display_result(cmd_context & ctx) {
+        params_ref p = ctx.params().merge_default_params(ps());
+        opt::context& opt = m_opt_ctx();
+        opt.display_assignment(ctx.regular_stream());
+        opt_params optp(p);
+        if (optp.print_model()) {
+            model_ref mdl;
+            opt.get_model(mdl);
+            if (mdl) {
+                ctx.regular_stream() << "(model " << std::endl;
+                model_smt2_pp(ctx.regular_stream(), ctx, *(mdl.get()), 2);
+                // m->display(ctx.regular_stream());
+                ctx.regular_stream() << ")" << std::endl;                    
+            }
+        }
+    }
 private:
 
     void display_statistics(cmd_context& ctx) {
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2e5a0f53f..6c9df93b0 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -139,10 +139,11 @@ namespace opt {
     }
 
     lbool context::execute_maxsat(symbol const& id, bool committed) {
+        model_ref tmp;
         maxsmt& ms = *m_maxsmts.find(id);
         lbool result = ms(get_solver());
         if (result == l_true && committed) ms.commit_assignment();
-        if (result == l_true) ms.get_model(m_model);
+        if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
         return result;
     }