diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index f1ec03528..f2c8cabf7 100644
--- a/src/ast/rewriter/ast_counter.cpp
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -86,7 +86,7 @@ int counter::get_max_counter_value() const {
     return res;
 }
 
-void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
+void var_counter::count_vars(const app * pred, int coef) {
     unsigned n = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
         m_fv(pred->get_arg(i));
diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h
index 8b3ec3bbd..a362c235b 100644
--- a/src/ast/rewriter/ast_counter.h
+++ b/src/ast/rewriter/ast_counter.h
@@ -76,7 +76,7 @@ protected:
     unsigned get_max_var(bool & has_var);    
 public:
     var_counter() {}
-    void count_vars(ast_manager & m, const app * t, int coef = 1);
+    void count_vars(const app * t, int coef = 1);
     unsigned get_max_var(expr* e);
     unsigned get_next_var(expr* e);
 };
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index b846bc06a..eabe1d551 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -682,11 +682,11 @@ namespace datalog {
         svector<bool> tail_neg;
         app_ref head(r->get_head(), m);
 
-        vctr.count_vars(m, head);
+        vctr.count_vars(head);
 
         for (unsigned i = 0; i < ut_len; i++) {
             app * t = r->get_tail(i);
-            vctr.count_vars(m, t);
+            vctr.count_vars(t);
             tail.push_back(t);
             tail_neg.push_back(r->is_neg_tail(i));
         }
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 2f60ddec8..0f254ee0a 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -256,12 +256,12 @@ namespace datalog {
     }
 
     
-    void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
+    void rule_counter::count_rule_vars(const rule * r, int coef) {
         reset();
-        count_vars(m, r->get_head(), 1);
+        count_vars(r->get_head(), 1);
         unsigned n = r->get_tail_size();
         for (unsigned i = 0; i < n; i++) {
-            count_vars(m, r->get_tail(i), coef);
+            count_vars(r->get_tail(i), coef);
         }
     }
 
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index bf5c225ef..513add584 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -347,7 +347,7 @@ namespace datalog {
     class rule_counter : public var_counter {        
     public:
         rule_counter(){}
-        void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
+        void count_rule_vars(const rule * r, int coef = 1);
         unsigned get_max_rule_var(const rule& r);
     };
 
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 204a8f316..9e8ead241 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -411,17 +411,16 @@ namespace datalog {
 
     void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
         SASSERT(r->get_positive_tail_size()==2);
-        ast_manager & m = m_context.get_manager();
         rule_counter counter;
         // leave one column copy per var in the head (avoids later duplication)
-        counter.count_vars(m, r->get_head(), -1);
+        counter.count_vars(r->get_head(), -1);
 
         // take interp & neg preds into account (at least 1 column copy if referenced)
         unsigned n = r->get_tail_size();
         if (n > 2) {
           rule_counter counter_tail;
           for (unsigned i = 2; i < n; ++i) {
-            counter_tail.count_vars(m, r->get_tail(i));
+            counter_tail.count_vars(r->get_tail(i));
           }
 
           rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end();
@@ -434,8 +433,8 @@ namespace datalog {
 
         app * t1 = r->get_tail(0);
         app * t2 = r->get_tail(1);
-        counter.count_vars(m, t1);
-        counter.count_vars(m, t2);
+        counter.count_vars(t1);
+        counter.count_vars(t2);
 
         get_local_indexes_for_projection(t1, counter, 0, res);
         get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 0e788ebff..1338a6de6 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -705,7 +705,7 @@ namespace datalog {
 
     rule * mk_explanations::get_e_rule(rule * r) {
         rule_counter ctr;
-        ctr.count_rule_vars(m_manager, r);
+        ctr.count_rule_vars(r);
         unsigned max_var;
         unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
         unsigned head_var = next_var++;
diff --git a/src/muz/rel/dl_mk_similarity_compressor.cpp b/src/muz/rel/dl_mk_similarity_compressor.cpp
index aa2fe8ab9..75caba6ae 100644
--- a/src/muz/rel/dl_mk_similarity_compressor.cpp
+++ b/src/muz/rel/dl_mk_similarity_compressor.cpp
@@ -381,7 +381,7 @@ namespace datalog {
         }
 
         rule_counter ctr;
-        ctr.count_rule_vars(m_manager, r);
+        ctr.count_rule_vars(r);
         unsigned max_var_idx, new_var_idx_base;
         if (ctr.get_max_positive(max_var_idx)) {
             new_var_idx_base = max_var_idx+1;
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index e33de8c6d..e76b3a25b 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -316,7 +316,7 @@ namespace datalog {
 
         void register_rule(rule * r) {
             rule_counter counter;
-            counter.count_rule_vars(m, r, 1);
+            counter.count_rule_vars(r, 1);
 
             ptr_vector<app> & rule_content = 
                 m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;
@@ -329,19 +329,19 @@ namespace datalog {
             for(unsigned i=0; i+1 < pos_tail_size; i++) {
                 app * t1 = r->get_tail(i);
                 var_idx_set t1_vars = rm.collect_vars(t1);
-                counter.count_vars(m, t1, -1);  //temporarily remove t1 variables from counter
+                counter.count_vars(t1, -1);  //temporarily remove t1 variables from counter
                 for(unsigned j=i+1; j<pos_tail_size; j++) {
                     app * t2 = r->get_tail(j);
-                    counter.count_vars(m, t2, -1);  //temporarily remove t2 variables from counter
+                    counter.count_vars(t2, -1);  //temporarily remove t2 variables from counter
                     var_idx_set scope_vars = rm.collect_vars(t2);
                     scope_vars |= t1_vars;
                     var_idx_set non_local_vars;
                     counter.collect_positive(non_local_vars);
-                    counter.count_vars(m, t2, 1);  //restore t2 variables in counter
+                    counter.count_vars(t2, 1);  //restore t2 variables in counter
                     set_intersection(non_local_vars, scope_vars);
                     register_pair(t1, t2, r, non_local_vars);
                 }
-                counter.count_vars(m, t1, 1);  //restore t1 variables in counter
+                counter.count_vars(t1, 1);  //restore t1 variables in counter
             }
         }
 
@@ -460,16 +460,16 @@ namespace datalog {
             app * head = r->get_head();
 
             var_counter counter;
-            counter.count_vars(m, head, 1);
+            counter.count_vars(head, 1);
 
             unsigned tail_size=r->get_tail_size();
             unsigned pos_tail_size=r->get_positive_tail_size();
 
             for(unsigned i=pos_tail_size; i<tail_size; i++) {
-                counter.count_vars(m, r->get_tail(i), 1);
+                counter.count_vars(r->get_tail(i), 1);
             }
             for(unsigned i=0; i<len; i++) {
-                counter.count_vars(m, rule_content[i], 1);
+                counter.count_vars(rule_content[i], 1);
             }
 
             //add edges that contain added tails
@@ -477,7 +477,7 @@ namespace datalog {
                 app * a_tail = added_tails.back();  //added tail
 
                 var_idx_set a_tail_vars = rm.collect_vars(a_tail);
-                counter.count_vars(m, a_tail, -1);  //temporarily remove a_tail variables from counter
+                counter.count_vars(a_tail, -1);  //temporarily remove a_tail variables from counter
 
                 for(unsigned i=0; i<len; i++) {
                     app * o_tail = rule_content[i]; //other tail
@@ -486,17 +486,17 @@ namespace datalog {
                         continue;
                     }
 
-                    counter.count_vars(m, o_tail, -1);  //temporarily remove o_tail variables from counter
+                    counter.count_vars(o_tail, -1);  //temporarily remove o_tail variables from counter
                     var_idx_set scope_vars = rm.collect_vars(o_tail);
                     scope_vars |= a_tail_vars;
                     var_idx_set non_local_vars;
                     counter.collect_positive(non_local_vars);
-                    counter.count_vars(m, o_tail, 1);  //restore o_tail variables in counter
+                    counter.count_vars(o_tail, 1);  //restore o_tail variables in counter
                     set_intersection(non_local_vars, scope_vars);
 
                     register_pair(o_tail, a_tail, r, non_local_vars);
                 }
-                counter.count_vars(m, a_tail, 1);  //restore t1 variables in counter
+                counter.count_vars(a_tail, 1);  //restore t1 variables in counter
                 added_tails.pop_back();
             }
         }
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 68c35e2c9..99a3b80f9 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -93,7 +93,7 @@ namespace datalog {
         unsigned n = head_pred->get_arity();
         
         rm.get_counter().reset();
-        rm.get_counter().count_vars(m, head, 1);
+        rm.get_counter().count_vars(head, 1);
 
         for (unsigned i=0; i<n; i++) {
             expr * arg = head->get_arg(i);
@@ -125,7 +125,7 @@ namespace datalog {
         unsigned head_arity = head_pred->get_arity();
 
         rm.get_counter().reset();
-        rm.get_counter().count_vars(m, head);
+        rm.get_counter().count_vars(head);
 
         unsigned arg_index;
         for (arg_index = 0; arg_index < head_arity; arg_index++) {