diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4e3ac1b19..03f0f016f 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -218,6 +218,7 @@ namespace opt {
         }
         IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
         s.get_model(m_model);
+        TRACE("opt", model_smt2_pp(tout, m, *m_model, 0););
         m_optsmt.setup(*m_opt_solver.get());
         update_lower();
         switch (m_objectives.size()) {
@@ -566,7 +567,7 @@ namespace opt {
             and_then(mk_simplify_tactic(m), 
                      mk_propagate_values_tactic(m),
                      mk_solve_eqs_tactic(m),
-                     mk_elim_uncnstr_tactic(m),
+                     // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);
         tactic_ref tac2, tac3;
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 951a0a8ef..f0ef78c77 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -124,14 +124,14 @@ namespace opt {
 
 
         expr_ref_vector ors(m), disj(m);
-        expr_ref or(m), bound(m.mk_true(), m);
+        expr_ref fml(m), bound(m.mk_true(), m);
         for (unsigned i = 0; i < m_upper.size(); ++i) {
             ors.push_back(m_s->mk_ge(i, m_upper[i]));
         }
         {
             solver::scoped_push _push(*m_s);
-            or = m.mk_or(ors.size(), ors.c_ptr());
-            m_s->assert_expr(or);
+            fml = m.mk_or(ors.size(), ors.c_ptr());
+            m_s->assert_expr(fml);
             lbool is_sat = l_true;
             while (!m_cancel) {
                 is_sat = m_s->check_sat(0,0);
@@ -149,8 +149,8 @@ namespace opt {
                         }
                     }
                     set_max(m_lower, m_s->get_objective_values(), disj);
-                    or = m.mk_or(ors.size(), ors.c_ptr());
-                    m_s->assert_expr(or);
+                    fml = m.mk_or(ors.size(), ors.c_ptr());
+                    m_s->assert_expr(fml);
                 }
                 else if (is_sat == l_undef) {
                     return l_undef;