diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index d61c906be..d26c55fda 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -613,12 +613,12 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
 
     expr* cond2 = nullptr, *t2 = nullptr, *e2 = nullptr;
     if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
-        try_ite_value(to_app(t), val, result);
+        VERIFY(BR_FAILED != try_ite_value(to_app(t), val, result));
         result = m().mk_ite(cond, result, m().mk_eq(e, val));
         return BR_REWRITE2;
     }
     if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
-        try_ite_value(to_app(e), val, result);
+        VERIFY(BR_FAILED != try_ite_value(to_app(e), val, result));
         result = m().mk_ite(cond, m().mk_eq(t, val), result);
         return BR_REWRITE2;
     }
@@ -640,19 +640,21 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
 
     br_status r = BR_FAILED;
     
-    if (m().is_ite(lhs) && m().is_value(rhs)) {
-        r = try_ite_value(to_app(lhs), to_app(rhs), result);
-        CTRACE("try_ite_value", r != BR_FAILED,
-               tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";);
+
+    if (m_ite_extra_rules) {
+        if (m().is_ite(lhs) && m().is_value(rhs)) {
+            r = try_ite_value(to_app(lhs), to_app(rhs), result);
+            CTRACE("try_ite_value", r != BR_FAILED,
+                   tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";);
+        }
+        else if (m().is_ite(rhs) && m().is_value(lhs)) {
+            r = try_ite_value(to_app(rhs), to_app(lhs), result);
+            CTRACE("try_ite_value", r != BR_FAILED,
+                   tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";);
+        }
+        if (r != BR_FAILED)
+            return r;
     }
-    else if (m().is_ite(rhs) && m().is_value(lhs)) {
-        r = try_ite_value(to_app(rhs), to_app(lhs), result);
-        CTRACE("try_ite_value", r != BR_FAILED,
-               tout << mk_bounded_pp(lhs, m()) << "\n" << mk_bounded_pp(rhs, m()) << "\n--->\n" << mk_bounded_pp(result, m()) << "\n";);
-    }
-    if (r != BR_FAILED)
-        return r;
-    
 
     if (m().is_bool(lhs)) {
         bool unfolded = false;
diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index d1bb90f0c..d3e780d33 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1085,7 +1085,7 @@ namespace opt {
         if (D.is_zero()) {
             throw default_exception("modulo 0 is not defined");
         }
-        TRACE("opt", display(tout << "lcm: " << D << " tableau\n"););
+        TRACE("opt1", display(tout << "lcm: " << D << " x: v" << x << " tableau\n"););
         rational val_x = m_var2value[x];
         rational u = mod(val_x, D);
         SASSERT(u.is_nonneg() && u < D);
@@ -1093,6 +1093,7 @@ namespace opt {
             replace_var(idx, x, u);            
             SASSERT(invariant(idx, m_rows[idx]));
         }
+        TRACE("opt1", display(tout << "tableau after replace x under mod\n"););
         //
         // update inequalities such that u is added to t and
         // D is multiplied to coefficient of x.
@@ -1114,6 +1115,7 @@ namespace opt {
                 visited.insert(row_id);
             }
         }
+        TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
         def result = project(y, compute_def);
         if (compute_def) {
             result = (result * D) + u;