diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index c542abb60..099bdedec 100644
--- a/src/ast/rewriter/ast_counter.cpp
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -93,7 +93,9 @@ void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
     unsigned n = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
         m_sorts.reset();
-        ::get_free_vars(pred->get_arg(i), m_sorts);
+        m_todo.reset();
+        m_mark.reset();
+        ::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
         for (unsigned j = 0; j < m_sorts.size(); ++j) {
             if (m_sorts[j]) {
                 update(j, coef);
diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h
index 2a581c302..e7251079f 100644
--- a/src/ast/rewriter/ast_counter.h
+++ b/src/ast/rewriter/ast_counter.h
@@ -38,6 +38,7 @@ public:
     
     counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
     
+    void reset() { m_data.reset(); }
     iterator begin() const { return m_data.begin(); }
     iterator end() const { return m_data.end(); }    
     void update(unsigned el, int delta);
@@ -71,6 +72,7 @@ protected:
     ptr_vector<sort> m_sorts;
     expr_fast_mark1  m_visited;
     ptr_vector<expr> m_todo;
+    ast_mark         m_mark;
     unsigned_vector  m_scopes;
     unsigned get_max_var(bool & has_var);    
 public:
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index 3ebc0b573..f7f0c8aef 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -17,7 +17,6 @@ Notes:
 
 --*/
 #include"var_subst.h"
-#include"used_vars.h"
 #include"ast_ll_pp.h"
 #include"ast_pp.h"
 #include"ast_smt2_pp.h"
@@ -40,7 +39,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
           tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
 }
 
-void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
+void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
     SASSERT(is_well_sorted(m, q));
     if (is_ground(q->get_expr())) {
         // ignore patterns if the body is a ground formula.
@@ -51,11 +50,11 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
         result = q;
         return;
     }
-    used_vars used;
-    used.process(q->get_expr());
+    m_used.reset();
+    m_used.process(q->get_expr());
     unsigned num_patterns = q->get_num_patterns();
     for (unsigned i = 0; i < num_patterns; i++)
-        used.process(q->get_pattern(i));
+        m_used.process(q->get_pattern(i));
     unsigned num_no_patterns = q->get_num_no_patterns();
     for (unsigned i = 0; i < num_no_patterns; i++)
         used.process(q->get_no_pattern(i));
@@ -110,9 +109,8 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
     std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size());
 
     expr_ref  new_expr(m);
-    var_subst subst(m);
     
-    subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
+    m_subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
     
     if (num_removed == num_decls) {
         result = new_expr;
@@ -145,7 +143,12 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
                              num_no_patterns,
                              new_no_patterns.c_ptr());
     to_quantifier(result)->set_no_unused_vars();
-    SASSERT(is_well_sorted(m, result));
+    SASSERT(is_well_sorted(m, result));    
+}
+
+void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
+    unused_vars_eliminator el(m);
+    el(q, result);
 }
 
 void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result) {
@@ -161,9 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
           tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
 }
 
-static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sorts) {
-    ast_mark mark;
-    ptr_vector<expr> todo;
+static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
     todo.push_back(e);
     while (!todo.empty()) {
         e = todo.back();
@@ -175,7 +176,9 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
         switch(e->get_kind()) {
         case AST_QUANTIFIER: {
             quantifier* q = to_quantifier(e);
-            get_free_vars_offset(q->get_expr(), offset+q->get_num_decls(), sorts);
+            ast_mark mark1;
+            ptr_vector<expr> todo1;
+            get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
             break;
         }
         case AST_VAR: {
@@ -207,5 +210,11 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
 
 
 void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
-    get_free_vars_offset(e, 0, sorts);
+    ast_mark mark;
+    ptr_vector<expr> todo;
+    get_free_vars_offset(mark, todo, 0, e, sorts);
+}
+
+void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
+    get_free_vars_offset(mark, todo, 0, e, sorts);
 }
diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h
index 9f3c13c0c..ffc21e691 100644
--- a/src/ast/rewriter/var_subst.h
+++ b/src/ast/rewriter/var_subst.h
@@ -20,6 +20,7 @@ Notes:
 #define _VAR_SUBST_H_
 
 #include"rewriter.h"
+#include"used_vars.h"
 
 /**
    \brief Alias for var_shifter class.
@@ -53,6 +54,15 @@ public:
 /**
    \brief Eliminate the unused variables from \c q. Store the result in \c r.
 */
+class unused_vars_eliminator {
+    ast_manager& m;
+    var_subst    m_subst;
+    used_vars    m_used;
+public:
+    unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {}
+    void operator()(quantifier* q, expr_ref& r);
+};
+
 void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
 
 /**
@@ -73,6 +83,8 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
 */
 void get_free_vars(expr* e, ptr_vector<sort>& sorts);
 
+void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
+
 #endif
 
 
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 50915946a..f283bd456 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -226,6 +226,7 @@ namespace datalog {
         m_rewriter(m),
         m_var_subst(m),
         m_rule_manager(*this),
+        m_elim_unused_vars(m),
         m_transf(*this),
         m_trail(*this),
         m_pinned(m),
@@ -332,7 +333,7 @@ namespace datalog {
                 quantifier_ref q(m);
                 sorts.reverse();
                 q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); 
-                elim_unused_vars(m, q, result);
+                m_elim_unused_vars(q, result);
             }
         }
         return result;
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 74449940c..2798ba8df 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -84,6 +84,7 @@ namespace datalog {
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
+        unused_vars_eliminator m_elim_unused_vars;
         rule_transformer   m_transf;
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz_qe/dl_finite_product_relation.cpp
index 4880e6068..86fef433b 100644
--- a/src/muz_qe/dl_finite_product_relation.cpp
+++ b/src/muz_qe/dl_finite_product_relation.cpp
@@ -1291,8 +1291,8 @@ namespace datalog {
                 m_renaming_for_inner_rel(m_manager) {
             relation_manager & rmgr = r.get_manager();
 
-            idx_set cond_columns;
-            collect_vars(m_manager, m_cond, cond_columns);
+            rule_manager& rm = r.get_context().get_rule_manager();
+            idx_set& cond_columns = rm.collect_vars(m_cond);
 
             unsigned sig_sz = r.get_signature().size();
             for(unsigned i=0; i<sig_sz; i++) {
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index f0fdc6ab2..c1f0912c0 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -145,7 +145,6 @@ namespace datalog {
         expr_ref_vector conjs(m), new_conjs(m);
         expr_ref tmp(m);
         expr_safe_replace sub(m);
-        uint_set lhs_vars, rhs_vars;
         bool change = false;
         bool inserted = false;
 
@@ -161,10 +160,8 @@ namespace datalog {
             
             if (is_store_def(e, x, y)) {
                 // enforce topological order consistency:
-                uint_set lhs;
-                collect_vars(m, x, lhs_vars);
-                collect_vars(m, y, rhs_vars);
-                lhs = lhs_vars;
+                uint_set lhs = rm.collect_vars(x);
+                uint_set rhs_vars = rm.collect_vars(y);
                 lhs &= rhs_vars;
                 if (!lhs.empty()) {
                     TRACE("dl", tout << "unusable equality " << mk_pp(e, m) << "\n";);
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 21f2a0bf7..74ac9ec97 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -38,6 +38,7 @@ namespace datalog {
         rule_manager&   rm;
         params_ref      m_params;
         th_rewriter     m_rewriter;
+        ptr_vector<sort> m_vars;
         mk_interp_tail_simplifier m_simplifier;
 
         typedef obj_map<app, var*> defs_t;
diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp
index 932a644ab..ef89c9ffa 100644
--- a/src/muz_qe/dl_mk_filter_rules.cpp
+++ b/src/muz_qe/dl_mk_filter_rules.cpp
@@ -27,9 +27,10 @@ namespace datalog {
     mk_filter_rules::mk_filter_rules(context & ctx):
             plugin(2000),
             m_context(ctx),
-            m_manager(ctx.get_manager()),
+            m(ctx.get_manager()),
+            rm(ctx.get_rule_manager()),
             m_result(0), 
-            m_pinned(m_manager) {
+            m_pinned(m) {
     }
 
     mk_filter_rules::~mk_filter_rules() {
@@ -52,14 +53,14 @@ namespace datalog {
     */
     bool mk_filter_rules::is_candidate(app * pred) {
         if (!m_context.is_predicate(pred)) {
-            TRACE("mk_filter_rules", tout << mk_pp(pred, m_manager) << "\nis not a candidate because it is interpreted.\n";);
+            TRACE("mk_filter_rules", tout << mk_pp(pred, m) << "\nis not a candidate because it is interpreted.\n";);
             return false;
         }
         var_idx_set used_vars;
         unsigned n  = pred->get_num_args();
         for (unsigned i = 0; i < n; i++) {
             expr * arg = pred->get_arg(i);
-            if (m_manager.is_value(arg))
+            if (m.is_value(arg))
                 return true;
             SASSERT(is_var(arg));
             unsigned vidx = to_var(arg)->get_idx();
@@ -74,10 +75,10 @@ namespace datalog {
        \brief Create a "filter" (if it doesn't exist already) for the given predicate.
     */
     func_decl *  mk_filter_rules::mk_filter_decl(app * pred, var_idx_set const & non_local_vars) {
-        sort_ref_buffer filter_domain(m_manager);
+        sort_ref_buffer filter_domain(m);
 
-        filter_key * key = alloc(filter_key, m_manager);
-        mk_new_rule_tail(m_manager, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
+        filter_key * key = alloc(filter_key, m);
+        mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
         func_decl * filter_decl = 0;
         if (!m_tail2filter.find(key, filter_decl)) {
             filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"), 
@@ -85,8 +86,8 @@ namespace datalog {
 
             m_pinned.push_back(filter_decl);
             m_tail2filter.insert(key, filter_decl);
-            app_ref filter_head(m_manager);
-            filter_head = m_manager.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
+            app_ref filter_head(m);
+            filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
             app * filter_tail = key->new_pred;
             rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0);
             filter_rule->set_accounting_parent_object(m_context, m_current);
@@ -104,16 +105,15 @@ namespace datalog {
     void mk_filter_rules::process(rule * r) {
         m_current = r;
         app * new_head = r->get_head();
-        app_ref_vector new_tail(m_manager);
+        app_ref_vector new_tail(m);
         svector<bool>  new_is_negated;
         unsigned sz = r->get_tail_size();
         bool rule_modified = false;
         for (unsigned i = 0; i < sz; i++) {
             app * tail = r->get_tail(i);
             if (is_candidate(tail)) {
-                TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m_manager) << "\n";);
-                var_idx_set non_local_vars;
-                collect_non_local_vars(m_manager, r, tail, non_local_vars);
+                TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";);
+                var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail);
                 func_decl * filter_decl = mk_filter_decl(tail, non_local_vars);
                 ptr_buffer<expr> new_args;
                 var_idx_set used_vars;
@@ -129,7 +129,7 @@ namespace datalog {
                     }
                 }
                 SASSERT(new_args.size() == filter_decl->get_arity());
-                new_tail.push_back(m_manager.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
+                new_tail.push_back(m.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
                 rule_modified = true;
             }
             else {
diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h
index 91751f9b8..b51cb8e24 100644
--- a/src/muz_qe/dl_mk_filter_rules.h
+++ b/src/muz_qe/dl_mk_filter_rules.h
@@ -59,7 +59,8 @@ namespace datalog {
         typedef obj_map<filter_key, func_decl*> filter_cache;
 
         context &                                 m_context;
-        ast_manager &                             m_manager;
+        ast_manager &                             m;
+        rule_manager &                            rm;
         filter_cache                              m_tail2filter;
         rule_set *                                m_result;
         rule *                                    m_current;
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
index d0b94f582..8a9b1257a 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
@@ -67,24 +67,23 @@ namespace datalog {
     void mk_interp_tail_simplifier::rule_substitution::get_result(rule_ref & res) {
         SASSERT(m_rule);
 
-        app_ref new_head(m);
-        apply(m_rule->get_head(), new_head);
+        apply(m_rule->get_head(), m_head);
 
-        app_ref_vector tail(m);
-        svector<bool> tail_neg;
+        m_tail.reset();
+        m_neg.reset();
 
         unsigned tail_len = m_rule->get_tail_size();
         for (unsigned i=0; i<tail_len; i++) {
             app_ref new_tail_el(m);
             apply(m_rule->get_tail(i), new_tail_el);
-            tail.push_back(new_tail_el);
-            tail_neg.push_back(m_rule->is_neg_tail(i));
+            m_tail.push_back(new_tail_el);
+            m_neg.push_back(m_rule->is_neg_tail(i));
         }
 
-        mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
+        mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
 
-        SASSERT(tail.size() == tail_neg.size());
-        res = m_context.get_rule_manager().mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+        SASSERT(m_tail.size() == m_neg.size());
+        res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr());
         res->set_accounting_parent_object(m_context, m_rule);
         res->norm_vars(res.get_manager());
     }
@@ -362,14 +361,34 @@ namespace datalog {
         }
     };
 
+    class mk_interp_tail_simplifier::normalizer_rw : public rewriter_tpl<normalizer_cfg> {
+    public:
+        normalizer_rw(ast_manager& m, normalizer_cfg& cfg): rewriter_tpl<normalizer_cfg>(m, false, cfg) {}
+    };
+
+
+    mk_interp_tail_simplifier::mk_interp_tail_simplifier(context & ctx, unsigned priority)
+            : plugin(priority),
+            m(ctx.get_manager()),
+            m_context(ctx),
+            m_simp(ctx.get_rewriter()),
+            a(m),
+            m_rule_subst(ctx) {
+        m_cfg = alloc(normalizer_cfg, m);
+        m_rw = alloc(normalizer_rw, m, *m_cfg);
+    }
+
+    mk_interp_tail_simplifier::~mk_interp_tail_simplifier() {
+        dealloc(m_rw);
+        dealloc(m_cfg);
+    }
+    
+
     void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res)
     {
         expr_ref simp1_res(m);
         m_simp(a, simp1_res);
-        normalizer_cfg r_cfg(m);
-        rewriter_tpl<normalizer_cfg> rwr(m, false, r_cfg);
-        expr_ref dl_form_e(m);
-        rwr(simp1_res.get(), res);
+        (*m_rw)(simp1_res.get(), res);
 
         /*if (simp1_res.get()!=res.get()) {
             std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h
index 247b20755..99e0b575a 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.h
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h
@@ -34,15 +34,17 @@ namespace datalog {
         {
             ast_manager& m;
             context& m_context;
-            substitution m_subst;
-            unifier m_unif;
-
-            rule * m_rule;
+            substitution   m_subst;
+            unifier        m_unif;
+            app_ref        m_head;
+            app_ref_vector m_tail;
+            svector<bool>  m_neg;
+            rule *         m_rule;
 
             void apply(app * a, app_ref& res);
         public:
             rule_substitution(context & ctx)
-                : m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_rule(0) {}
+                : m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_head(m), m_tail(m), m_rule(0) {}
 
             /**
             Reset substitution and get it ready for working with rule r.
@@ -61,13 +63,17 @@ namespace datalog {
             }
         };
 
+        class normalizer_cfg;
+        class normalizer_rw;
+
         ast_manager &     m;
         context &         m_context;
         th_rewriter &     m_simp;
         arith_util        a;
         rule_substitution m_rule_subst;
+        normalizer_cfg*   m_cfg;
+        normalizer_rw*    m_rw;
 
-        class normalizer_cfg;
 
         void simplify_expr(app * a, expr_ref& res);
 
@@ -77,13 +83,8 @@ namespace datalog {
         /** Return true if something was modified */
         bool transform_rules(const rule_set & orig, rule_set & tgt);
     public:
-        mk_interp_tail_simplifier(context & ctx, unsigned priority=40000)
-            : plugin(priority),
-            m(ctx.get_manager()),
-            m_context(ctx),
-            m_simp(ctx.get_rewriter()),
-            a(m),
-            m_rule_subst(ctx) {}
+        mk_interp_tail_simplifier(context & ctx, unsigned priority=40000);
+        virtual ~mk_interp_tail_simplifier();
 
         /**If rule should be retained, assign transformed version to res and return true;
         if rule can be deleted, return false.
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp
index 54ffdc805..f6f79f348 100644
--- a/src/muz_qe/dl_mk_magic_sets.cpp
+++ b/src/muz_qe/dl_mk_magic_sets.cpp
@@ -28,6 +28,7 @@ namespace datalog {
         plugin(10000, true),
         m_context(ctx),
         m(ctx.get_manager()),
+        rm(ctx.get_rule_manager()),
         m_pinned(m), 
         m_goal(goal, m) {
     }
@@ -259,7 +260,7 @@ namespace datalog {
             }
             new_tail.push_back(curr);
             negations.push_back(r->is_neg_tail(curr_index));
-            collect_vars(m, curr, bound_vars);
+            bound_vars |= rm.collect_vars(curr);
         }
 
 
diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h
index dfc66e7ea..3496a5967 100644
--- a/src/muz_qe/dl_mk_magic_sets.h
+++ b/src/muz_qe/dl_mk_magic_sets.h
@@ -95,6 +95,7 @@ namespace datalog {
 
         context &	       m_context;
         ast_manager &          m;
+        rule_manager&          rm;
         ast_ref_vector         m_pinned;
         /**
            \brief Predicates from the original set that appear in a head of a rule
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index 5bbeb2378..4afc1d323 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -505,9 +505,6 @@ namespace datalog {
 
         unsigned head_arity = head_pred->get_arity();
 
-        //var_idx_set head_vars;
-        //var_idx_set same_strat_vars;
-        //collect_vars(m, r->get_head(), head_vars);
 
         unsigned pt_len = r->get_positive_tail_size();
         for (unsigned ti=0; ti<pt_len; ++ti) {
@@ -518,7 +515,6 @@ namespace datalog {
             SASSERT(pred_strat<=head_strat);
 
             if (pred_strat==head_strat) {
-                //collect_vars(m, r->get_head(), same_strat_vars);
                 if (pred->get_arity()>head_arity
                     || (pred->get_arity()==head_arity && pred->get_id()>=head_pred->get_id()) ) {
                     return false;
diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp
index 2fec78066..990125475 100644
--- a/src/muz_qe/dl_mk_simple_joins.cpp
+++ b/src/muz_qe/dl_mk_simple_joins.cpp
@@ -29,7 +29,8 @@ namespace datalog {
 
     mk_simple_joins::mk_simple_joins(context & ctx):
         plugin(1000),
-        m_context(ctx) {
+        m_context(ctx),
+        rm(ctx.get_rule_manager()) {
     }
 
     class join_planner {
@@ -120,6 +121,7 @@ namespace datalog {
 
         context & m_context;
         ast_manager & m;
+        rule_manager & rm;
         var_subst & m_var_subst;
         rule_set & m_rs_aux_copy; //reference to a rule_set that will allow to ask for stratum levels
 
@@ -130,10 +132,13 @@ namespace datalog {
         ptr_hashtable<rule, ptr_hash<rule>, ptr_eq<rule> > m_modified_rules;
 
         ast_ref_vector m_pinned;
+        mutable ptr_vector<sort> m_vars;
 
     public:
         join_planner(context & ctx, rule_set & rs_aux_copy)
-            : m_context(ctx), m(ctx.get_manager()), m_var_subst(ctx.get_var_subst()),
+            : m_context(ctx), m(ctx.get_manager()), 
+              rm(ctx.get_rule_manager()),
+              m_var_subst(ctx.get_var_subst()),
               m_rs_aux_copy(rs_aux_copy), 
               m_introduced_rules(ctx.get_rule_manager()),
               m_pinned(ctx.get_manager())
@@ -175,9 +180,7 @@ namespace datalog {
 
             unsigned max_var_idx = 0;
             {
-                var_idx_set orig_var_set;
-                collect_vars(m, t1, orig_var_set);
-                collect_vars(m, t2, orig_var_set);
+                var_idx_set& orig_var_set = rm.collect_vars(t1, t2);
                 var_idx_set::iterator ovit = orig_var_set.begin();
                 var_idx_set::iterator ovend = orig_var_set.end();
                 for(; ovit!=ovend; ++ovit) {
@@ -323,14 +326,13 @@ namespace datalog {
             }
             for(unsigned i=0; i<pos_tail_size; i++) {
                 app * t1 = r->get_tail(i);
-                var_idx_set t1_vars;
-                collect_vars(m, t1, t1_vars);
+                var_idx_set t1_vars = rm.collect_vars(t1);
                 counter.count_vars(m, 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
-                    var_idx_set scope_vars(t1_vars);
-                    collect_vars(m, t2, scope_vars);
+                    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
@@ -472,8 +474,7 @@ namespace datalog {
             while(!added_tails.empty()) {
                 app * a_tail = added_tails.back();  //added tail
 
-                var_idx_set a_tail_vars;
-                collect_vars(m, a_tail, a_tail_vars);
+                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
 
                 for(unsigned i=0; i<len; i++) {
@@ -484,8 +485,8 @@ namespace datalog {
                     }
 
                     counter.count_vars(m, o_tail, -1);  //temporarily remove o_tail variables from counter
-                    var_idx_set scope_vars(a_tail_vars);
-                    collect_vars(m, o_tail, scope_vars);
+                    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
diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz_qe/dl_mk_simple_joins.h
index 89832626f..36eb08dd5 100644
--- a/src/muz_qe/dl_mk_simple_joins.h
+++ b/src/muz_qe/dl_mk_simple_joins.h
@@ -49,7 +49,8 @@ namespace datalog {
        We say that a rule containing C_i's is a rule with a "big tail".
     */
     class mk_simple_joins : public rule_transformer::plugin {
-        context &							m_context;
+        context & 	    m_context;
+        rule_manager &      rm;
     public:
         mk_simple_joins(context & ctx);
         
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp
index eec0b991d..7eb6f829d 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.cpp
+++ b/src/muz_qe/dl_mk_unbound_compressor.cpp
@@ -27,7 +27,8 @@ namespace datalog {
         plugin(500),
         m_context(ctx),
         m(ctx.get_manager()),
-        m_rules(ctx.get_rule_manager()),
+        rm(ctx.get_rule_manager()),
+        m_rules(rm),
         m_pinned(m) {
     }
 
@@ -47,10 +48,7 @@ namespace datalog {
         }
         unsigned var_idx = to_var(head_arg)->get_idx();
 
-        var_idx_set tail_vars;
-        collect_tail_vars(m, r, tail_vars);
-
-        return tail_vars.contains(var_idx);
+        return rm.collect_tail_vars(r).contains(var_idx);
     }
 
     void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) {
@@ -83,8 +81,7 @@ namespace datalog {
 
     void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) {
         rule * r = m_rules.get(rule_index);
-        var_idx_set tail_vars;
-        collect_tail_vars(m, r, tail_vars);
+        var_idx_set& tail_vars = rm.collect_tail_vars(r);
 
         app * head = r->get_head();
         func_decl * head_pred = head->get_decl();
@@ -94,9 +91,9 @@ namespace datalog {
         }
 
         unsigned n = head_pred->get_arity();
-
-        var_counter head_var_counter;
-        head_var_counter.count_vars(m, head, 1);
+        
+        rm.get_counter().reset();
+        rm.get_counter().count_vars(m, head, 1);
 
         for (unsigned i=0; i<n; i++) {
             expr * arg = head->get_arg(i);
@@ -107,7 +104,7 @@ namespace datalog {
             if (!tail_vars.contains(var_idx)) {
                 //unbound
 
-                unsigned occurence_cnt = head_var_counter.get(var_idx);
+                unsigned occurence_cnt = rm.get_counter().get(var_idx);
                 SASSERT(occurence_cnt>0);
                 if (occurence_cnt == 1) {
                     TRACE("dl", r->display(m_context, tout << "Compress: "););
@@ -121,15 +118,14 @@ namespace datalog {
     void mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) {
     start:
         rule * r = m_rules.get(rule_index);
-        var_idx_set tail_vars;
-        collect_tail_vars(m, r, tail_vars);
+        var_idx_set& tail_vars = rm.collect_tail_vars(r);
         
         app * head = r->get_head();
         func_decl * head_pred = head->get_decl();
         unsigned head_arity = head_pred->get_arity();
 
-        var_counter head_var_counter;
-        head_var_counter.count_vars(m, head);
+        rm.get_counter().reset();
+        rm.get_counter().count_vars(m, head);
 
         unsigned arg_index;
         for (arg_index = 0; arg_index < head_arity; arg_index++) {
@@ -140,7 +136,7 @@ namespace datalog {
             unsigned var_idx = to_var(arg)->get_idx();
             if (!tail_vars.contains(var_idx)) {
                 //unbound
-                unsigned occurence_cnt = head_var_counter.get(var_idx);
+                unsigned occurence_cnt = rm.get_counter().get(var_idx);
                 SASSERT(occurence_cnt>0);
                 if ( occurence_cnt==1 && m_in_progress.contains(c_info(head_pred, arg_index)) ) {
                     //we have found what to compress
diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h
index 4e56a74fc..4e2ff0b3c 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.h
+++ b/src/muz_qe/dl_mk_unbound_compressor.h
@@ -52,6 +52,7 @@ namespace datalog {
 
         context &	    m_context;
         ast_manager &       m;
+        rule_manager &      rm;
         rule_ref_vector     m_rules;
         bool                m_modified;
         todo_stack          m_todo;
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 32f3a5fe8..59d316ae7 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -48,7 +48,9 @@ namespace datalog {
 
     rule_manager::rule_manager(context& ctx) 
         : m(ctx.get_manager()),
-          m_ctx(ctx) {}
+          m_ctx(ctx),
+          m_cfg(m),
+          m_rwr(m, false, m_cfg) {}
 
     void rule_manager::inc_ref(rule * r) {
         if (r) {
@@ -67,29 +69,20 @@ namespace datalog {
         }
     }
 
-    class remove_label_cfg : public default_rewriter_cfg {
-        family_id m_label_fid;
-    public:        
-        remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
-        virtual ~remove_label_cfg() {}
-
-        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
-            proof_ref & result_pr)
-        {
-            if (is_decl_of(f, m_label_fid, OP_LABEL)) {
-                SASSERT(num == 1);
-                result = args[0];
-                return BR_DONE;
-            }
-            return BR_FAILED;
+    br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
+                                                         proof_ref & result_pr)
+    {
+        if (is_decl_of(f, m_label_fid, OP_LABEL)) {
+            SASSERT(num == 1);
+            result = args[0];
+            return BR_DONE;
         }
-    };
+        return BR_FAILED;
+    }
 
     void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
         expr_ref tmp(m);
-        remove_label_cfg r_cfg(m);
-        rewriter_tpl<remove_label_cfg> rwr(m, false, r_cfg);
-        rwr(fml, tmp);
+        m_rwr(fml, tmp);
         if (pr && fml != tmp) {
             
             pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
@@ -97,6 +90,67 @@ namespace datalog {
         fml = tmp;
     }
 
+    var_idx_set& rule_manager::collect_vars(expr* e) {
+        return collect_vars(e, 0);
+    }
+
+    var_idx_set& rule_manager::collect_vars(expr* e1, expr* e2) {
+        reset_collect_vars();
+        if (e1) accumulate_vars(e1);
+        if (e2) accumulate_vars(e2);
+        return finalize_collect_vars();
+    }
+
+    void rule_manager::reset_collect_vars() {
+        m_vars.reset();
+        m_var_idx.reset();
+        m_todo.reset();
+        m_mark.reset();
+    }
+
+    var_idx_set& rule_manager::finalize_collect_vars() {
+        unsigned sz = m_vars.size();
+        for (unsigned i=0; i<sz; ++i) {
+            if (m_vars[i]) m_var_idx.insert(i); 
+        }
+        return m_var_idx;
+    }
+
+    var_idx_set& rule_manager::collect_tail_vars(rule * r) {
+        reset_collect_vars();
+        unsigned n = r->get_tail_size();
+        for (unsigned i=0;i<n;i++) {
+            accumulate_vars(r->get_tail(i));
+        }
+        return finalize_collect_vars();
+    }
+
+    var_idx_set& rule_manager::collect_rule_vars_ex(rule * r, app* t) {
+        reset_collect_vars();
+        unsigned n = r->get_tail_size();
+        accumulate_vars(r->get_head());
+        for (unsigned i=0;i<n;i++) {
+            if (r->get_tail(i) != t) {
+                accumulate_vars(r->get_tail(i));
+            }
+        }
+        return finalize_collect_vars();
+    }
+
+    var_idx_set& rule_manager::collect_rule_vars(rule * r) {
+        reset_collect_vars();
+        unsigned n = r->get_tail_size();
+        accumulate_vars(r->get_head());
+        for (unsigned i=0;i<n;i++) {
+            accumulate_vars(r->get_tail(i));
+        }
+        return finalize_collect_vars();
+    }
+
+    void rule_manager::accumulate_vars(expr* e) {
+        ::get_free_vars(m_mark, m_todo, e, m_vars);
+    }
+
 
     void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {              
         scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
@@ -570,15 +624,14 @@ namespace datalog {
             return;
         }
 
-        ptr_vector<sort> free_rule_vars;
         var_counter vctr;
         app_ref_vector tail(m);
         svector<bool> tail_neg;
         app_ref head(r->get_head(), m);
 
-        get_free_vars(r, free_rule_vars);
+        collect_rule_vars(r);
         vctr.count_vars(m, head);
-
+        ptr_vector<sort>& free_rule_vars = m_vars;
 
         for (unsigned i = 0; i < ut_len; i++) {
             app * t = r->get_tail(i);
@@ -906,7 +959,7 @@ namespace datalog {
     }
 
     void rule::norm_vars(rule_manager & rm) {
-        used_vars used;
+        used_vars& used = rm.reset_used();
         get_used_vars(used);
 
         unsigned first_unsused = used.get_max_found_var_idx_plus_1();
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 666ddbd50..5abb64624 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -27,6 +27,7 @@ Revision History:
 #include"proof_converter.h"
 #include"model_converter.h"
 #include"ast_counter.h"
+#include"rewriter.h"
 
 namespace datalog {
 
@@ -47,9 +48,27 @@ namespace datalog {
     */
     class rule_manager
     {
+        class remove_label_cfg : public default_rewriter_cfg {
+            family_id m_label_fid;
+        public:        
+        remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
+            virtual ~remove_label_cfg() {}
+            
+            br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
+                                 proof_ref & result_pr);
+        };
+    
         ast_manager&         m;
         context&             m_ctx;
         rule_counter         m_counter;
+        used_vars            m_used;
+        ptr_vector<sort>     m_vars;
+        var_idx_set          m_var_idx;
+        ptr_vector<expr>     m_todo;
+        ast_mark             m_mark;
+        remove_label_cfg               m_cfg;
+        rewriter_tpl<remove_label_cfg> m_rwr;
+
 
         // only the context can create a rule_manager
         friend class context;
@@ -90,6 +109,10 @@ namespace datalog {
          */
         void reduce_unbound_vars(rule_ref& r);
 
+        void reset_collect_vars();
+
+        var_idx_set& finalize_collect_vars();
+
     public:
 
         ast_manager& get_manager() const { return m; }
@@ -98,6 +121,24 @@ namespace datalog {
 
         void dec_ref(rule * r);
 
+        used_vars& reset_used() { m_used.reset(); return m_used; }
+
+        var_idx_set& collect_vars(expr * pred);
+
+        var_idx_set& collect_vars(expr * e1, expr* e2);
+
+        var_idx_set& collect_rule_vars(rule * r);
+
+        var_idx_set& collect_rule_vars_ex(rule * r, app* t);
+
+        var_idx_set& collect_tail_vars(rule * r);
+
+        void accumulate_vars(expr* pred);
+
+        ptr_vector<sort>& get_var_sorts() { return m_vars; }
+
+        var_idx_set&      get_var_idx() { return m_var_idx; }
+
         /**
            \brief Create a Datalog rule from a Horn formula.
            The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))
diff --git a/src/muz_qe/dl_sieve_relation.cpp b/src/muz_qe/dl_sieve_relation.cpp
index c3ea5a3d0..e80462900 100644
--- a/src/muz_qe/dl_sieve_relation.cpp
+++ b/src/muz_qe/dl_sieve_relation.cpp
@@ -567,8 +567,7 @@ namespace datalog {
         const relation_signature sig = r.get_signature();
         unsigned sz = sig.size();
 
-        var_idx_set cond_vars;
-        collect_vars(m, condition, cond_vars);
+        var_idx_set& cond_vars = get_context().get_rule_manager().collect_vars(condition);
         expr_ref_vector subst_vect(m);
         subst_vect.resize(sz);
         unsigned subst_ofs = sz-1;
diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp
index 95d268510..1b1042345 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz_qe/dl_util.cpp
@@ -158,36 +158,7 @@ namespace datalog {
         ::get_free_vars(trm, vars);
         return var_idx < vars.size() && vars[var_idx] != 0;
     }
-
-
-    void collect_vars(ast_manager & m, expr * e, var_idx_set & result) {
-        ptr_vector<sort> vars;
-        ::get_free_vars(e, vars);
-        unsigned sz = vars.size();
-        for(unsigned i=0; i<sz; ++i) {
-            if(vars[i]) { result.insert(i); }
-        }
-    }
     
-    void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result) {
-        unsigned n = r->get_tail_size();
-        for(unsigned i=0;i<n;i++) {
-            collect_vars(m, r->get_tail(i), result);
-        }
-    }
-
-    void get_free_tail_vars(rule * r, ptr_vector<sort>& sorts) {
-        unsigned n = r->get_tail_size();
-        for(unsigned i=0;i<n;i++) {
-            get_free_vars(r->get_tail(i), sorts);
-        }
-    }
-
-    void get_free_vars(rule * r, ptr_vector<sort>& sorts) {
-        get_free_vars(r->get_head(), sorts);
-        get_free_tail_vars(r, sorts);
-    }
-
     unsigned count_variable_arguments(app * pred)
     {
         SASSERT(is_uninterp(pred));
@@ -202,26 +173,6 @@ namespace datalog {
         return res;
     }
 
-    void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result) {
-        collect_vars(m, r->get_head(), result);
-        unsigned sz = r->get_tail_size();
-        for (unsigned i = 0; i < sz; i++) {
-            app * curr = r->get_tail(i);
-            if (curr != t)
-                collect_vars(m, curr, result);
-        }
-    }
-
-    void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result) {
-        collect_vars(m, r->get_head(), result);
-        unsigned sz = r->get_tail_size();
-        for (unsigned i = 0; i < sz; i++) {
-            app * curr = r->get_tail(i);
-            if (curr != t_1 && curr != t_2)
-                collect_vars(m, curr, result);
-        }
-    }
-
     void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var, 
                           sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
         expr_ref_buffer new_args(m);
@@ -404,6 +355,7 @@ namespace datalog {
 
     
     void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
+        reset();
         count_vars(m, r->get_head(), 1);
         unsigned n = r->get_tail_size();
         for (unsigned i = 0; i < n; i++) {
diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h
index 96bc8c326..70e34f91c 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -81,33 +81,13 @@ namespace datalog {
 
     void flatten_or(expr* fml, expr_ref_vector& result);
     
-
-
     bool contains_var(expr * trm, unsigned var_idx);
 
-    /**
-       \brief Collect the variables in \c pred. 
-       \pre \c pred must be a valid head or tail.
-    */
-    void collect_vars(ast_manager & m, expr * pred, var_idx_set & result);
-    void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result);
-
-    void get_free_vars(rule * r, ptr_vector<sort>& sorts);
-
     /**
        \brief Return number of arguments of \c pred that are variables
     */
     unsigned count_variable_arguments(app * pred);
 
-    /**
-       \brief Store in \c result the set of variables used by \c r when ignoring the tail \c t.
-    */
-    void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result);
-
-    /**
-       \brief Store in \c result the set of variables used by \c r when ignoring the tail elements \c t_1 and \c t_2.
-    */
-    void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result);
 
     template<typename T>
     void copy_nonvariables(app * src, T& tgt)
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index ff49584ff..50c3347ee 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -2525,15 +2525,15 @@ public:
         m_params(p) {
         m_imp = alloc(imp, m, p);
     }
-
-    virtual tactic * translate(ast_manager & m) {
-        return alloc(qe_lite_tactic, m, m_params);
-    }
         
     virtual ~qe_lite_tactic() {
         dealloc(m_imp);
     }
 
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(qe_lite_tactic, m, m_params);
+    }
+
     virtual void updt_params(params_ref const & p) {
         m_params = p;
         // m_imp->updt_params(p);
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 9c80d8c34..3e1fef906 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -316,7 +316,7 @@ namespace smt {
             m_nc_functor(*this) {
         }            
 
-        ~theory_diff_logic() {
+        virtual ~theory_diff_logic() {
             reset_eh();
         }
 
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index f5e5fa9fa..3f2e224d9 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -231,9 +231,8 @@ void * memory::allocate(size_t s) {
         return 0;
     s = s + sizeof(size_t); // we allocate an extra field!
     void * r = malloc(s);
-    if (r == 0) {
+    if (r == 0) 
         throw_out_of_memory();
-    }
     *(static_cast<size_t*>(r)) = s;
     g_memory_thread_alloc_size += s;
     if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {