diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 8c34325a4..79959d9bf 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -128,7 +128,8 @@ namespace datalog {
             func_decl * pred = r->get_decl();
             if (engine.get_fact(pred).is_reachable()) {
                 res->add_rule(r);
-            } else if (m_context.get_model_converter()) {
+            } 
+            else if (m_context.get_model_converter()) {
                 pruned_preds.insert(pred);
             }
         }
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index eccbd0921..fe9dee45e 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -608,7 +608,8 @@ namespace datalog {
             TRACE("dl",
                   source.display(tout);
                   res->display(tout););
-        } else {
+        } 
+        else {
             res = nullptr;
         }
         return res.detach();
diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp
index e277a93b4..d75ae0b46 100644
--- a/src/muz/transforms/dl_mk_subsumption_checker.cpp
+++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp
@@ -335,7 +335,7 @@ namespace datalog {
     rule_set * mk_subsumption_checker::operator()(rule_set const & source) {
         // TODO mc
         if (!m_context.get_params ().xform_subsumption_checker())
-          return nullptr;
+            return nullptr;
 
         m_have_new_total_rule = false;
         collect_ground_unconditional_rule_heads(source);
@@ -356,8 +356,7 @@ namespace datalog {
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
         while (m_have_new_total_rule) {
             m_have_new_total_rule = false;
-
-            scoped_ptr<rule_set> old = res;
+            scoped_ptr<rule_set> old = res.detach();
             res = alloc(rule_set, m_context);
             transform_rules(*old, *res);
         }
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 6be75fc2c..c9d4fd3c6 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -387,7 +387,7 @@ namespace datalog {
             }
         }
 
-        rule_set * result = static_cast<rule_set *>(nullptr);
+        scoped_ptr<rule_set> result;
         if (m_modified) {
             result = alloc(rule_set, m_context);
             unsigned fin_rule_cnt = m_rules.size();
@@ -397,7 +397,7 @@ namespace datalog {
             result->inherit_predicates(source);
         }
         reset();
-        return result;
+        return result.detach();
     }
 
 
diff --git a/src/muz/transforms/dl_mk_unfold.cpp b/src/muz/transforms/dl_mk_unfold.cpp
index c9b8becde..6a1ae1535 100644
--- a/src/muz/transforms/dl_mk_unfold.cpp
+++ b/src/muz/transforms/dl_mk_unfold.cpp
@@ -51,13 +51,12 @@ namespace datalog {
     }
         
     rule_set * mk_unfold::operator()(rule_set const & source) {
-        rule_set* rules = alloc(rule_set, m_ctx);
-        rule_set::iterator it = source.begin(), end = source.end();
-        for (; it != end; ++it) {
-            expand_tail(**it, 0, source, *rules);
+        scoped_ptr<rule_set> rules = alloc(rule_set, m_ctx);
+        for (rule* r : source) {
+            expand_tail(*r, 0, source, *rules);
         }
         rules->inherit_predicates(source);
-        return rules;
+        return rules.detach();
     }
 
 };