diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index d4b28ab2f..5347fa1b2 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -29,6 +29,8 @@ Notes:
 #include "scoped_ctrl_c.h"
 #include "scoped_timer.h"
 #include "parametric_cmd.h"
+#include "opt_params.hpp"
+#include "model_smt2_pp.h"
 
 class opt_context {
     cmd_context& ctx;
@@ -291,10 +293,22 @@ public:
             }
         }
         switch(r) {
-        case l_true:
+        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;                    
+                }
+            }
             break;
+        }
         case l_false:
             ctx.regular_stream() << "unsat\n";
             break;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2db52795c..6501ef51b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -28,7 +28,6 @@ Notes:
 #include "lia2card_tactic.h"
 #include "elim01_tactic.h"
 #include "tactical.h"
-#include "th_rewriter.h"
 
 namespace opt {
 
@@ -65,14 +64,9 @@ namespace opt {
     }
 
     unsigned context::add_objective(app* t, bool is_max) {
-        expr_ref tr(t, m);
-        app_ref  ar(m);
-        th_rewriter rewrite(m);
-        rewrite(tr);
-        SASSERT(is_app(tr));
-        ar = to_app(tr);
+        app_ref tr(t, m);
         unsigned index = m_objectives.size();
-        m_objectives.push_back(objective(is_max, ar, index));
+        m_objectives.push_back(objective(is_max, tr, index));
         return index;
     }
 
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 40ff00a89..868906858 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -3,9 +3,10 @@ def_module_params('opt',
                   export=True,
                   params=(('timeout', UINT, UINT_MAX, 'set timeout'),
                           ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
-	                      ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"),
+	                  ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
+                          ('print_model', BOOL, False, 'display model for satisfiable constraints'),
                           ('debug_conflict', BOOL, False, 'debug conflict resolution'),
                           ))
 
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index ec16d825d..d870d5675 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -126,15 +126,14 @@ namespace opt {
     }
 
     void optsmt::update_lower() {
-        model_ref md;
-        m_s->get_model(md);
+        m_s->get_model(m_model);
         set_max(m_lower, m_s->get_objective_values());
         IF_VERBOSE(1, 
                    for (unsigned i = 0; i < m_lower.size(); ++i) {
                        verbose_stream() << m_lower[i] << " ";
                    }
                    verbose_stream() << "\n";
-                   model_pp(verbose_stream(), *md);
+                   model_pp(verbose_stream(), *m_model);
                    );
         expr_ref_vector disj(m);
         expr_ref constraint(m);