diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index d81b4fa13..bba6db2b6 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -29,14 +29,15 @@ struct cofactor_elim_term_ite::imp {
     ast_manager &      m;
     params_ref         m_params;
     unsigned long long m_max_memory;
-    volatile bool m_cancel;
+    bool               m_cofactor_equalities;
+    volatile bool      m_cancel;
 
     void checkpoint() { 
         cooperate("cofactor ite");
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         if (m_cancel)
-            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            throw tactic_exception(TACTIC_CANCELED_MSG);
     }
 
     // Collect atoms that contain term if-then-else
@@ -111,7 +112,7 @@ struct cofactor_elim_term_ite::imp {
                 frame & fr    = m_frame_stack.back();
                 expr * t      = fr.m_t;
                 bool form_ctx = fr.m_form_ctx;
-                TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                TRACE("cofactor", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
 
                 m_owner.checkpoint();
                 
@@ -150,7 +151,7 @@ struct cofactor_elim_term_ite::imp {
                     }
                     if (i < num_args) {
                         m_has_term_ite.mark(t);
-                        TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                        TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
                         save_candidate(t, form_ctx);
                     }
                 }
@@ -167,6 +168,7 @@ struct cofactor_elim_term_ite::imp {
     };
 
     expr * get_first(expr * t) { 
+        TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
         typedef std::pair<expr *, unsigned> frame;
         expr_fast_mark1         visited;            
         sbuffer<frame>          stack;    
@@ -225,6 +227,7 @@ struct cofactor_elim_term_ite::imp {
        \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
     */
     expr * get_best(expr * t) {
+        TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
         typedef std::pair<expr *, unsigned> frame;
         obj_map<expr, unsigned> occs;
         expr_fast_mark1         visited;            
@@ -299,12 +302,17 @@ struct cofactor_elim_term_ite::imp {
             }
         }
         visited.reset();
-        CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
+        CTRACE("cofactor", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
         return best;
     }
 
     void updt_params(params_ref const & p) {
         m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+        m_cofactor_equalities = p.get_bool("cofactor_equalities", true);
+    }
+
+    void collect_param_descrs(param_descrs & r) {
+        r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.");
     }
 
     void set_cancel(bool f) {
@@ -354,16 +362,16 @@ struct cofactor_elim_term_ite::imp {
                 m_term = 0;
                 expr * lhs;
                 expr * rhs;
-                if (m.is_eq(t, lhs, rhs)) {
+                if (m_owner.m_cofactor_equalities && m.is_eq(t, lhs, rhs)) {
                     if (m.is_unique_value(lhs)) {
                         m_term  = rhs;
                         m_value = to_app(lhs); 
-                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                        TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
                     }
                     else if (m.is_unique_value(rhs)) {
                         m_term  = lhs;
                         m_value = to_app(rhs);
-                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                        TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
                     }
                 }
                 // TODO: bounds
@@ -467,7 +475,7 @@ struct cofactor_elim_term_ite::imp {
                     m_cofactor.set_cofactor_atom(neg_c);
                     m_cofactor(curr, neg_cofactor);
                     curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                    TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
                 }
             }
             return false;
@@ -522,7 +530,7 @@ struct cofactor_elim_term_ite::imp {
         
         void cofactor(expr * t, expr_ref & r) {
             unsigned step = 0;
-            TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
+            TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
             expr_ref curr(m);
             curr = t;
             while (true) {
@@ -543,21 +551,20 @@ struct cofactor_elim_term_ite::imp {
                 m_cofactor(curr, neg_cofactor);
                 if (pos_cofactor == neg_cofactor) {
                     curr = pos_cofactor;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
+                else if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
                     curr = c;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
+                else if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
                     curr = neg_c;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
-                TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                else {
+                    curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
+                }
+                TRACE("cofactor", 
+                      tout << "cofactor_ite step: " << step << "\n";
+                      tout << "co-factor: " << mk_ismt2_pp(c, m) << "\n";
+                      tout << mk_ismt2_pp(curr, m) << "\n";);
             }
         }
 
@@ -570,6 +577,7 @@ struct cofactor_elim_term_ite::imp {
         
         void operator()(expr * t, expr_ref & r) {
             ptr_vector<expr> new_args;
+            SASSERT(m_frames.empty());
             m_frames.push_back(frame(t, true));
             while (!m_frames.empty()) {
                 m_owner.checkpoint();
@@ -649,7 +657,8 @@ struct cofactor_elim_term_ite::imp {
 
     imp(ast_manager & _m, params_ref const & p):
         m(_m),
-        m_params(p) {
+        m_params(p),
+        m_cofactor_equalities(true) {
         m_cancel = false;
         updt_params(p);
     }
@@ -686,7 +695,8 @@ void cofactor_elim_term_ite::updt_params(params_ref const & p) {
     m_imp->updt_params(p);
 }
 
-void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) {
+void cofactor_elim_term_ite::collect_param_descrs(param_descrs & r) {
+    m_imp->collect_param_descrs(r);
 }
 
 void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h
index 9b325b1f0..ce2f31ea0 100644
--- a/src/tactic/core/cofactor_elim_term_ite.h
+++ b/src/tactic/core/cofactor_elim_term_ite.h
@@ -31,7 +31,7 @@ public:
     virtual ~cofactor_elim_term_ite();
 
     void updt_params(params_ref const & p);
-    static void get_param_descrs(param_descrs & r);
+    void collect_param_descrs(param_descrs & r);
 
     void operator()(expr * t, expr_ref & r);
     
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index 16b4d1ad4..bc719a85e 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -52,8 +52,7 @@ public:
 
     virtual ~cofactor_term_ite_tactic() {}
     virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
-    static  void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); }
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
+    virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); }
     
     virtual void operator()(goal_ref const & g, 
                             goal_ref_buffer & result,