diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index bf8a9dd7f..6fb4ef542 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -31,6 +31,7 @@ Notes:
 #include "propagate_values_tactic.h"
 #include "solve_eqs_tactic.h"
 #include "elim_uncnstr_tactic.h"
+#include "elim_term_ite_tactic.h"
 #include "tactical.h"
 #include "model_smt2_pp.h"
 #include "card2bv_tactic.h"
@@ -650,17 +651,19 @@ namespace opt {
             and_then(mk_simplify_tactic(m), 
                      mk_propagate_values_tactic(m),
                      mk_solve_eqs_tactic(m),
+                     mk_elim_term_ite_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;
+        tactic_ref tac2, tac3, tac4;
         if (optp.elim_01()) {
             tac2 = mk_elim01_tactic(m);
             tac3 = mk_lia2card_tactic(m);
+            tac4 = mk_elim_term_ite_tactic(m);
             params_ref lia_p;
             lia_p.set_bool("compile_equality", optp.pb_compile_equality());
             tac3->updt_params(lia_p);
-            set_simplify(and_then(tac0.get(), tac2.get(), tac3.get()));
+            set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get()));
         }
         else {
             set_simplify(tac0.get());
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 6b061f9cd..02effa337 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -141,6 +141,7 @@ namespace opt {
                 ors.push_back(m_s->mk_ge(i, m_upper[i]));
             }
             
+            
             fml = m.mk_or(ors.size(), ors.c_ptr());
             tmp = m.mk_fresh_const("b", m.mk_bool_sort());
             fml = m.mk_implies(tmp, fml);
@@ -150,6 +151,7 @@ namespace opt {
             solver::scoped_push _push(*m_s);
             while (!m_cancel) {
                 m_s->assert_expr(fml);
+                TRACE("opt", tout << fml << "\n";);
                 is_sat = m_s->check_sat(1,vars);
                 if (is_sat == l_true) {
                     disj.reset();
@@ -343,6 +345,7 @@ namespace opt {
                     m_lower[i] = m_s->saved_objective_value(i);
                 }
             }
+            TRACE("opt", tout << "strengthen bound: " << block << "\n";);
             m_s->assert_expr(block);
             
             // TBD: only works for simplex