diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index 993831d64..bec80240f 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -260,39 +260,44 @@ expr_ref mk_distinct(expr_ref_vector const& args) {
 void flatten_and(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;
+    expr_fast_mark1 seen;
     for (unsigned i = 0; i < result.size(); ++i) {
-        if (m.is_and(result.get(i))) {
-            app* a = to_app(result.get(i));
+        expr* e = result.get(i);
+        if (seen.is_marked(e))
+            continue;
+        seen.mark(e);
+        if (m.is_and(e)) {
+            app* a = to_app(e);
             for (expr* arg : *a) result.push_back(arg);
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) {
+        else if (m.is_not(e, e1) && m.is_not(e1, e2)) {
             result[i] = e2;
             --i;
         }
-        else if (m.is_not(result.get(i), e1) && m.is_or(e1)) {
+        else if (m.is_not(e, e1) && m.is_or(e1)) {
             app* a = to_app(e1);
             for (expr* arg : *a) result.push_back(m.mk_not(arg));
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result.get(i), e1) && m.is_implies(e1,e2,e3)) {
+        else if (m.is_not(e, e1) && m.is_implies(e1, e2, e3)) {
             result.push_back(e2);
             result[i] = m.mk_not(e3);
             --i;
         }
-        else if (m.is_true(result.get(i)) ||
-                 (m.is_not(result.get(i), e1) &&
+        else if (m.is_true(e) ||
+                 (m.is_not(e, e1) &&
                   m.is_false(e1))) {
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_false(result.get(i)) ||
-                 (m.is_not(result.get(i), e1) &&
+        else if (m.is_false(e) ||
+                 (m.is_not(e, e1) &&
                   m.is_true(e1))) {
             result.reset();
             result.push_back(m.mk_false());
@@ -317,39 +322,44 @@ void flatten_and(expr_ref& fml) {
 void flatten_or(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;
+    expr_fast_mark1 seen;
     for (unsigned i = 0; i < result.size(); ++i) {
-        if (m.is_or(result.get(i))) {
-            app* a = to_app(result.get(i));
+        expr* e = result.get(i);
+        if (seen.is_marked(e))
+            continue;
+        seen.mark(e);
+        if (m.is_or(e)) {
+            app* a = to_app(e);
             for (expr* arg : *a) result.push_back(arg);
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) {
+        else if (m.is_not(e, e1) && m.is_not(e1, e2)) {
             result[i] = e2;
             --i;
         }
-        else if (m.is_not(result.get(i), e1) && m.is_and(e1)) {
+        else if (m.is_not(e, e1) && m.is_and(e1)) {
             app* a = to_app(e1);
             for (expr* arg : *a) result.push_back(m.mk_not(arg));
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_implies(result.get(i),e2,e3)) {
+        else if (m.is_implies(e,e2,e3)) {
             result.push_back(e3);
             result[i] = m.mk_not(e2);
             --i;
         }
-        else if (m.is_false(result.get(i)) ||
-                 (m.is_not(result.get(i), e1) &&
+        else if (m.is_false(e) ||
+                 (m.is_not(e, e1) &&
                   m.is_true(e1))) {
             result[i] = result.back();
             result.pop_back();
             --i;
         }
-        else if (m.is_true(result.get(i)) ||
-                 (m.is_not(result.get(i), e1) &&
+        else if (m.is_true(e) ||
+                 (m.is_not(e, e1) &&
                   m.is_false(e1))) {
             result.reset();
             result.push_back(m.mk_true());
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 2baaf57b9..9bd7a7adf 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -178,7 +178,7 @@ namespace datalog {
             m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
         }
         for (unsigned i = 0; i < fmls.size(); ++i) {
-            mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name);
+            mk_horn_rule(fmls.get(i), prs.get(i), rules, name);
         }
     }
 
@@ -190,12 +190,10 @@ namespace datalog {
         hoist_compound_predicates(index, m_head, m_body);
         TRACE("dl_rule",
               tout << mk_pp(m_head, m) << " :- ";
-              for (unsigned i = 0; i < m_body.size(); ++i) {
-                  tout << mk_pp(m_body[i].get(), m) << " ";
-              }
+              for (expr* b : m_body) 
+                  tout << mk_pp(b, m) << " ";              
               tout << "\n";);
 
-
         mk_negations(m_body, m_neg);
         check_valid_rule(m_head, m_body.size(), m_body.data());
 
@@ -241,9 +239,8 @@ namespace datalog {
             m_args.reset();
             head = ensure_app(e2);
             flatten_and(e1, m_args);
-            for (unsigned i = 0; i < m_args.size(); ++i) {
-                body.push_back(ensure_app(m_args[i].get()));
-            }
+            for (expr* a : m_args)
+                body.push_back(ensure_app(a));            
         }
         else {
             head = ensure_app(fml);
@@ -255,7 +252,7 @@ namespace datalog {
         unsigned sz = body.size();
         hoist_compound(index, head, body);
         for (unsigned i = 0; i < sz; ++i) {
-            app_ref b(body[i].get(), m);
+            app_ref b(body.get(i), m);
             hoist_compound(index, b, body);
             body[i] = b;
         }
@@ -949,7 +946,8 @@ namespace datalog {
     }
 
     bool rule::has_negation() const {
-        for (unsigned i = 0; i < get_uninterpreted_tail_size(); ++i) {
+        unsigned sz = get_uninterpreted_tail_size();
+        for (unsigned i = 0; i < sz; ++i) {
             if (is_neg_tail(i)) {
                 return true;
             }
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 044260f12..02d13c1ca 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -287,13 +287,12 @@ namespace datalog {
     class rule : public accounted_object {
         friend class rule_manager;
 
-        app*     m_head{ nullptr };
-        proof*   m_proof{ nullptr };
-        unsigned m_tail_size:20;
-        // unsigned m_reserve:12;
-        unsigned m_ref_cnt{ 0 };
-        unsigned m_positive_cnt{ 0 };
-        unsigned m_uninterp_cnt{ 0 };
+        app*     m_head = nullptr;
+        proof*   m_proof = nullptr;
+        unsigned m_tail_size = 0;
+        unsigned m_ref_cnt = 0;
+        unsigned m_positive_cnt = 0;
+        unsigned m_uninterp_cnt = 0;
         symbol   m_name;
         /**
            The following field is an array of tagged pointers.