diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp
index 89f82b33d..1f617a199 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.cpp
+++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp
@@ -98,17 +98,15 @@ namespace datalog {
         expr_ref_vector new_conjs(m);
         expr_ref tmp(m);
 
-
-        for (unsigned i = utsz; i < tsz; ++i)
+        for (unsigned i = 0; i < tsz; ++i)
             new_conjs.push_back(r.get_tail(i));
         flatten_and(new_conjs);
 
         expr_ref fml1(m), fml2(m), body(m), head(m);
 
         // blast ite
-        body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
+        body = mk_and(new_conjs);
         if (!has_term_ite(body)) {
-            TRACE("dl_term_ite", tout << "No term-ite, skipping a rule\n";);
             new_rules.add_rule(&r);
             return false;
         }
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index c1abd7bef..5ad3f67d2 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -582,13 +582,11 @@ namespace datalog {
     bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) {
         bool modified = false;
         rule_manager& rm = m_context.get_rule_manager();
-        rule_set::iterator rit = orig.begin();
-        rule_set::iterator rend = orig.end();
-        for (; rit!=rend; ++rit) {
+        for (rule * r : orig) {
             rule_ref new_rule(rm);
-            if (transform_rule(*rit, new_rule)) {
-                rm.mk_rule_rewrite_proof(**rit, *new_rule.get());
-                bool is_modified = *rit != new_rule;
+            if (transform_rule(r, new_rule)) {
+                rm.mk_rule_rewrite_proof(*r, *new_rule.get());
+                bool is_modified = r != new_rule;
                 modified |= is_modified;
                 tgt.add_rule(new_rule);
             }