diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index b040efc0c..bea672265 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -323,7 +323,6 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
     if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) ||
         (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ)))
         return reduce_power(arg1, arg2, kind, result);
-    CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
     br_status st = cancel_monomials(arg1, arg2, m_arith_lhs, new_arg1, new_arg2);
     TRACE("mk_le_bug", tout << "st: " << st << "\n";);
     if (st != BR_FAILED) {
@@ -335,6 +334,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
     if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) {
         arg1 = new_new_arg1;
         arg2 = new_new_arg2;
+        CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
         if (st == BR_FAILED)
             st = BR_DONE;
     }
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index dda38e566..83d83fdb5 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -137,6 +137,7 @@ namespace opt {
         params_ref p;
         p.set_bool("model", true);
         p.set_bool("unsat_core", true);
+        p.set_bool("elim_to_real", true);
         updt_params(p);
     }
 
@@ -661,7 +662,7 @@ namespace opt {
             g->assert_expr(fmls[i].get());
         }
         tactic_ref tac0 = 
-            and_then(mk_simplify_tactic(m), 
+            and_then(mk_simplify_tactic(m, m_params), 
                      mk_propagate_values_tactic(m),
                      mk_solve_eqs_tactic(m),
                      // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints