diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp
index 6deb4bf45..0569eb360 100644
--- a/src/ast/expr_abstract.cpp
+++ b/src/ast/expr_abstract.cpp
@@ -20,52 +20,50 @@ Notes:
 #include "expr_abstract.h"
 #include "map.h"
 
-void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result) {
-    ast_ref_vector pinned(m);
-    ptr_vector<expr> stack;
-    obj_map<expr, expr*> map;
+void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
+    
     expr * curr = 0, *b = 0;
     SASSERT(n->get_ref_count() > 0);
 
-    stack.push_back(n);
+    m_stack.push_back(n);
 
     for (unsigned i = 0; i < num_bound; ++i) {
         b = bound[i];
         expr* v = m.mk_var(base + num_bound - i - 1, m.get_sort(b));
-        pinned.push_back(v);
-        map.insert(b, v);
+        m_pinned.push_back(v);
+        m_map.insert(b, v);
     }
 
-    while(!stack.empty()) {
-        curr = stack.back();
-        if (map.contains(curr)) {
-            stack.pop_back();
+    while(!m_stack.empty()) {
+        curr = m_stack.back();
+        if (m_map.contains(curr)) {
+            m_stack.pop_back();
             continue;
         }
         switch(curr->get_kind()) {
         case AST_VAR: {
-            map.insert(curr, curr);
-            stack.pop_back();
+            m_map.insert(curr, curr);
+            m_stack.pop_back();
             break;
         }
         case AST_APP: {
             app* a = to_app(curr);
             bool all_visited = true;
-            ptr_vector<expr> args;
+            m_args.reset();
             for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                if (!map.find(a->get_arg(i), b)) {
-                    stack.push_back(a->get_arg(i));
+                if (!m_map.find(a->get_arg(i), b)) {
+                    m_stack.push_back(a->get_arg(i));
                     all_visited = false;
                 }
                 else {
-                    args.push_back(b);
+                    m_args.push_back(b);
                 }
             }
             if (all_visited) {
-                b = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
-                pinned.push_back(b);
-                map.insert(curr, b);
-                stack.pop_back();
+                b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
+                m_pinned.push_back(b);
+                m_map.insert(curr, b);
+                m_stack.pop_back();
             }
             break;
         }
@@ -81,17 +79,24 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
             }
             expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1);
             b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get());
-            pinned.push_back(b);            
-            map.insert(curr, b);
-            stack.pop_back();            
+            m_pinned.push_back(b);            
+            m_map.insert(curr, b);
+            m_stack.pop_back();            
             break;
         }
         default:
             UNREACHABLE();
         }
     }
-    if (!map.find(n, b)) {
-        UNREACHABLE();
-    }
+    VERIFY (m_map.find(n, b));
     result = b;
+    m_pinned.reset();
+    m_map.reset();
+    m_stack.reset();
+    m_args.reset();   
+}
+
+void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result) {
+    expr_abstractor abs(m);
+    abs(base, num_bound, bound, n, result);
 }
diff --git a/src/ast/expr_abstract.h b/src/ast/expr_abstract.h
index c6ec7973b..3d9f3960f 100644
--- a/src/ast/expr_abstract.h
+++ b/src/ast/expr_abstract.h
@@ -21,6 +21,17 @@ Notes:
 
 #include"ast.h"
 
+class expr_abstractor {
+    ast_manager& m;
+    expr_ref_vector m_pinned;
+    ptr_vector<expr> m_stack, m_args;
+    obj_map<expr, expr*> m_map;
+    
+public:
+    expr_abstractor(ast_manager& m): m(m), m_pinned(m) {}
+    void operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result);
+};
+
 void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result);
 
 #endif
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index f7f0c8aef..930267dad 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -57,10 +57,10 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
         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));
+        m_used.process(q->get_no_pattern(i));
 
     unsigned num_decls = q->get_num_decls();
-    if (used.uses_all_vars(num_decls)) {
+    if (m_used.uses_all_vars(num_decls)) {
         q->set_no_unused_vars();
         result = q;
         return;
@@ -69,7 +69,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
     ptr_buffer<sort>  used_decl_sorts; 
     buffer<symbol>    used_decl_names;
     for (unsigned i = 0; i < num_decls; ++i) {
-        if (used.contains(num_decls - i - 1)) {
+        if (m_used.contains(num_decls - i - 1)) {
             used_decl_sorts.push_back(q->get_decl_sort(i));
             used_decl_names.push_back(q->get_decl_name(i));
         }
@@ -78,10 +78,10 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
     unsigned         num_removed = 0;
     expr_ref_buffer  var_mapping(m);
     int              next_idx = 0;
-    unsigned         sz = used.get_max_found_var_idx_plus_1();
+    unsigned         sz = m_used.get_max_found_var_idx_plus_1();
 
     for (unsigned i = 0; i < num_decls; ++i) {
-        sort * s = used.contains(i);
+        sort * s = m_used.contains(i);
         if (s) {
             var_mapping.push_back(m.mk_var(next_idx, s));
             next_idx++;
@@ -94,7 +94,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
     // (VAR 0) is in the first position of var_mapping.
 
     for (unsigned i = num_decls; i < sz; i++) {
-        sort * s = used.contains(i);
+        sort * s = m_used.contains(i);
         if (s)
             var_mapping.push_back(m.mk_var(i - num_removed, s));
         else
@@ -122,11 +122,11 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
     expr_ref_buffer new_no_patterns(m);
     
     for (unsigned i = 0; i < num_patterns; i++) {
-        subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
+        m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
         new_patterns.push_back(tmp);
     }
     for (unsigned i = 0; i < num_no_patterns; i++) {
-        subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
+        m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
         new_no_patterns.push_back(tmp);
     }
     
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index f283bd456..592c1ad4b 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -49,7 +49,6 @@ Revision History:
 #include"dl_mk_quantifier_abstraction.h"
 #include"dl_mk_quantifier_instantiation.h"
 #include"datatype_decl_plugin.h"
-#include"expr_abstract.h"
 
 
 namespace datalog {
@@ -227,6 +226,7 @@ namespace datalog {
         m_var_subst(m),
         m_rule_manager(*this),
         m_elim_unused_vars(m),
+        m_abstractor(m),
         m_transf(*this),
         m_trail(*this),
         m_pinned(m),
@@ -307,7 +307,7 @@ namespace datalog {
         }
         else {
             ptr_vector<sort> sorts;
-            expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
+            m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
             get_free_vars(result, sorts);
             if (sorts.empty()) {
                 result = fml;
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 2798ba8df..aba8577e1 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -45,6 +45,7 @@ Revision History:
 #include"model2expr.h"
 #include"smt_params.h"
 #include"dl_rule_transformer.h"
+#include"expr_abstract.h"
 
 namespace datalog {
 
@@ -85,6 +86,7 @@ namespace datalog {
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
         unused_vars_eliminator m_elim_unused_vars;
+        expr_abstractor        m_abstractor;
         rule_transformer   m_transf;
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index 74ac9ec97..21f2a0bf7 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -38,7 +38,6 @@ 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;