diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp
index f1071d106..f9c6c49c3 100644
--- a/lib/dl_bmc_engine.cpp
+++ b/lib/dl_bmc_engine.cpp
@@ -215,6 +215,7 @@ namespace datalog {
     lbool bmc::check_linear() {
         for (unsigned i = 0; ; ++i) {
             IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); 
+            checkpoint();
             compile_linear(i);
             lbool res = check_linear(i);
             if (res == l_undef) {
diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp
index b2b54fe38..04ad64851 100644
--- a/lib/pdr_util.cpp
+++ b/lib/pdr_util.cpp
@@ -290,7 +290,7 @@ void ternary_model_evaluator::minimize_model(ptr_vector<expr> const & formulas,
         for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; 
     );
 
-    prune_cone_of_influence(formulas, model);
+    prune_by_cone_of_influence(formulas, model);
 
     // prune_by_probing(formulas, model);
 
@@ -335,7 +335,7 @@ void ternary_model_evaluator::prune_by_probing(ptr_vector<expr> const& formulas,
     TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";);
 }
 
-void ternary_model_evaluator::prune_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model) {
+void ternary_model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model) {
     ptr_vector<expr> todo, tocollect;
     todo.append(formulas);
     m_visited.reset();
@@ -364,28 +364,35 @@ void ternary_model_evaluator::prune_cone_of_influence(ptr_vector<expr> const & f
             case OP_EQ:
             case OP_IFF:
                 if (e->get_arg(0) == e->get_arg(1)) {
-                    break;
+                    // no-op                    
                 }
-                if (!m.is_bool(e->get_arg(0))) {
+                else if (!m.is_bool(e->get_arg(0))) {
                     tocollect.push_back(e);
-                    break;
                 }
-                todo.append(sz, args);
-                break;
-                              
+                else {
+                    todo.append(sz, args);
+                }
+                break;                              
             case OP_DISTINCT:
                 tocollect.push_back(e);
                 break;
             case OP_ITE:
-                if (e->get_arg(1) == e->get_arg(2)) {
-                    break;
+                if (args[1] == args[2]) {
+                    // 
                 }
-                todo.push_back(args[0]);
-                if (is_true(args[0])) {
+                else if (is_true(args[1]) && is_true(args[2])) {
+                    todo.append(2, args+1);
+                }
+                else if (is_false(args[2]) && is_false(args[2])) {
+                    todo.append(2, args+1);
+                }
+                else if (is_true(args[0])) {
+                    todo.push_back(args[0]);
                     todo.push_back(args[1]);
                 }
                 else {
                     SASSERT(is_false(args[0]));
+                    todo.push_back(args[0]);
                     todo.push_back(args[2]);
                 }
                 break;
@@ -395,8 +402,11 @@ void ternary_model_evaluator::prune_cone_of_influence(ptr_vector<expr> const & f
                 }
                 else {
                     unsigned i = 0;
-                    for (; !is_false(args[i]) && i < sz; ++i);
-                    SASSERT(i < sz);
+                    for (; !is_false(args[i]) && i < sz; ++i);     
+                    if (i == sz) {
+                        fatal_error(1);
+                    }
+                    VERIFY(i < sz);
                     todo.push_back(args[i]);
                 }
                 break;
@@ -404,7 +414,10 @@ void ternary_model_evaluator::prune_cone_of_influence(ptr_vector<expr> const & f
                 if (v) {
                     unsigned i = 0;
                     for (; !is_true(args[i]) && i < sz; ++i);
-                    SASSERT(i < sz);
+                    if (i == sz) {
+                        fatal_error(1);
+                    }
+                    VERIFY(i < sz);
                     todo.push_back(args[i]);
                 }
                 else {
diff --git a/lib/pdr_util.h b/lib/pdr_util.h
index 217f66735..f3cddd130 100644
--- a/lib/pdr_util.h
+++ b/lib/pdr_util.h
@@ -214,7 +214,7 @@ class ternary_model_evaluator  : public model_evaluator_base {
     void del_model(expr* e);
     
     bool get_assignment(expr* e, expr*& var, expr*& val);
-    void prune_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
+    void prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
     void prune_by_probing(ptr_vector<expr> const & formulas, expr_ref_vector& model);
 
     //00 -- non-visited
@@ -246,7 +246,8 @@ public:
     ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {}
     virtual void minimize_model(ptr_vector<expr> const & formulas, expr_ref_vector & model);
 
-    void operator()(expr* e) { m_visited.mark(e, true); }
+    // for_each_expr visitor.
+    void operator()(expr* e) {} 
 };
 
 void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);