diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 5819e3930..f684879ae 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -260,6 +260,7 @@ class smt_printer {
         else {
             m_out << sym << "[";
         }
+
         for (unsigned i = 0; i < num_params; ++i) {
             parameter const& p = params[i];
             if (p.is_ast()) {
@@ -642,9 +643,7 @@ class smt_printer {
             m_out << m_var_names[m_num_var_names - idx - 1];
         }
         else {
-            if (!m_is_smt2) {
-                m_out << "?" << idx;
-            }
+            m_out << "?" << idx;
         }
     }
 
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/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index c542abb60..a807237c5 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);
@@ -108,24 +110,27 @@ unsigned var_counter::get_max_var(bool& has_var) {
     unsigned max_var = 0;
     while (!m_todo.empty()) {
         expr* e = m_todo.back();
-        unsigned scope = m_scopes.back();
         m_todo.pop_back();
-        m_scopes.pop_back();
         if (m_visited.is_marked(e)) {
             continue;
         }
         m_visited.mark(e, true);
         switch(e->get_kind()) {
         case AST_QUANTIFIER: {
+            var_counter aux_counter;
             quantifier* q = to_quantifier(e);
-            m_todo.push_back(q->get_expr());
-            m_scopes.push_back(scope + q->get_num_decls());
+            bool has_var1 = false;
+            unsigned max_v = aux_counter.get_max_var(has_var1);
+            if (max_v > max_var + q->get_num_decls()) {
+                max_var = max_v - q->get_num_decls();
+                has_var = true;
+            }
             break;                 
         }
         case AST_VAR: {
-            if (to_var(e)->get_idx() >= scope + max_var) {
+            if (to_var(e)->get_idx() >= max_var) {
                 has_var = true;
-                max_var = to_var(e)->get_idx() - scope;
+                max_var = to_var(e)->get_idx();
             }
             break;
         }
@@ -133,7 +138,6 @@ unsigned var_counter::get_max_var(bool& has_var) {
             app* a = to_app(e);
             for (unsigned i = 0; i < a->get_num_args(); ++i) {
                 m_todo.push_back(a->get_arg(i));
-                m_scopes.push_back(scope);                    
             }
             break;
         }
@@ -150,14 +154,12 @@ unsigned var_counter::get_max_var(bool& has_var) {
 unsigned var_counter::get_max_var(expr* e) {
     bool has_var = false;
     m_todo.push_back(e);
-    m_scopes.push_back(0);
     return get_max_var(has_var);
 }
 
 unsigned var_counter::get_next_var(expr* e) {
     bool has_var = false;
     m_todo.push_back(e);
-    m_scopes.push_back(0);
     unsigned mv = get_max_var(has_var);
     if (has_var) mv++;
     return mv;
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..930267dad 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,17 +50,17 @@ 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));
+        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;
@@ -70,7 +69,7 @@ void elim_unused_vars(ast_manager & m, 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));
         }
@@ -79,10 +78,10 @@ void elim_unused_vars(ast_manager & m, 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++;
@@ -95,7 +94,7 @@ void elim_unused_vars(ast_manager & m, 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
@@ -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;
@@ -124,11 +122,11 @@ void elim_unused_vars(ast_manager & m, 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);
     }
     
@@ -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/clp_context.cpp b/src/muz_qe/clp_context.cpp
new file mode 100644
index 000000000..25ea1455b
--- /dev/null
+++ b/src/muz_qe/clp_context.cpp
@@ -0,0 +1,226 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    clp_context.cpp
+
+Abstract:
+
+    Bounded CLP (symbolic simulation using Z3) context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-04-26
+
+Revision History:
+
+--*/
+
+#include "clp_context.h"
+#include "dl_context.h"
+#include "unifier.h"
+#include "var_subst.h"
+#include "substitution.h"
+
+namespace datalog {
+
+    class clp::imp {
+        struct stats {
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+            unsigned m_num_unfold;
+            unsigned m_num_no_unfold;
+            unsigned m_num_subsumed;
+        };
+
+        context&               m_ctx;
+        ast_manager&           m;
+        rule_manager&          rm;
+        smt_params             m_fparams;
+        smt::kernel            m_solver;
+        var_subst              m_var_subst;
+        expr_ref_vector        m_ground;
+        app_ref_vector         m_goals;
+        volatile bool          m_cancel;
+        stats                  m_stats;
+    public:
+        imp(context& ctx):
+            m_ctx(ctx), 
+            m(ctx.get_manager()),
+            rm(ctx.get_rule_manager()),
+            m_solver(m, m_fparams),      // TBD: can be replaced by efficient BV solver.
+            m_var_subst(m, false),
+            m_ground(m),
+            m_goals(m),
+            m_cancel(false)
+        {
+            // m_fparams.m_relevancy_lvl = 0;
+            m_fparams.m_mbqi = false;
+            m_fparams.m_soft_timeout = 1000;
+        }
+
+        ~imp() {}        
+
+        lbool query(expr* query) {
+            m_ctx.ensure_opened();
+            m_solver.reset();
+            m_goals.reset();
+            rm.mk_query(query, m_ctx.get_rules());
+            expr_ref head(m);
+            head = m_ctx.get_rules().last()->get_head();
+            ground(head);
+            m_goals.push_back(to_app(head));
+            return search(20, 0);
+        }
+    
+        void cancel() {
+            m_cancel = true;
+            m_solver.cancel();
+        }
+        
+        void cleanup() {
+            m_cancel = false;
+            m_goals.reset();
+            m_solver.reset_cancel();
+        }
+
+        void reset_statistics() {
+            m_stats.reset();
+        }
+
+        void collect_statistics(statistics& st) const {
+            //st.update("tab.num_unfold", m_stats.m_num_unfold);
+            //st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold);
+            //st.update("tab.num_subsumed", m_stats.m_num_subsumed);
+        }
+
+        void display_certificate(std::ostream& out) const {
+            expr_ref ans = get_answer();
+            out << mk_pp(ans, m) << "\n";    
+
+        }
+
+        expr_ref get_answer() const {
+            return expr_ref(m.mk_true(), m);
+        }
+
+    private:
+
+        void reset_ground() {
+            m_ground.reset();
+        }
+        
+        void ground(expr_ref& e) {
+            ptr_vector<sort> sorts;
+            get_free_vars(e, sorts);
+            if (m_ground.size() < sorts.size()) {
+                m_ground.resize(sorts.size());
+            }
+            for (unsigned i = 0; i < sorts.size(); ++i) {
+                if (sorts[i] && !m_ground[i].get()) {
+                    m_ground[i] = m.mk_fresh_const("c",sorts[i]);
+                }
+            }
+            m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
+        }
+
+        lbool search(unsigned depth, unsigned index) {
+            if (index == m_goals.size()) {
+                return l_true;
+            }
+            if (depth == 0) {
+                return l_undef;
+            }
+            IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";);
+            unsigned num_goals = m_goals.size();
+            app* head = m_goals[index].get();
+            rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl());
+            lbool status = l_false;
+            for (unsigned i = 0; i < rules.size(); ++i) {
+                rule* r = rules[i];
+                m_solver.push();
+                reset_ground();
+                expr_ref tmp(m);
+                tmp = r->get_head();
+                IF_VERBOSE(2, verbose_stream() << index << " " << mk_pp(tmp, m) << "\n";);
+                ground(tmp);
+                for (unsigned j = 0; j < head->get_num_args(); ++j) {
+                    expr_ref eq(m);
+                    eq = m.mk_eq(head->get_arg(j), to_app(tmp)->get_arg(j));
+                    m_solver.assert_expr(eq);
+                }
+                for (unsigned j = r->get_uninterpreted_tail_size(); j < r->get_tail_size(); ++j) {
+                    tmp = r->get_tail(j);
+                    ground(tmp);
+                    m_solver.assert_expr(tmp);
+                }
+                lbool is_sat = m_solver.check();
+                switch (is_sat) {
+                case l_false:
+                    break;
+                case l_true:
+                    if (depth == 1 && (index+1 > m_goals.size() || r->get_uninterpreted_tail_size() > 0)) {
+                        status = l_undef;
+                        break;
+                    }
+                    for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) {
+                        tmp = r->get_tail(j);
+                        ground(tmp);
+                        m_goals.push_back(to_app(tmp));
+                    }
+                    switch(search(depth-1, index+1)) {
+                    case l_undef:
+                        status = l_undef;
+                        // fallthrough
+                    case l_false:
+                        m_goals.resize(num_goals);   
+                        break;
+                    case l_true:
+                        return l_true;
+                    }
+                    break;
+                case l_undef:
+                    status = l_undef;
+                    throw default_exception("undef");
+                }
+                m_solver.pop(1);
+            }
+            return status;
+        }
+    
+    
+        proof_ref get_proof() const {
+            return proof_ref(0, m);
+        }
+    };
+    
+    clp::clp(context& ctx):
+        m_imp(alloc(imp, ctx)) {        
+    }
+    clp::~clp() {
+        dealloc(m_imp);
+    }    
+    lbool clp::query(expr* query) {
+        return m_imp->query(query);
+    }
+    void clp::cancel() {
+        m_imp->cancel();
+    }
+    void clp::cleanup() {
+        m_imp->cleanup();
+    }
+    void clp::reset_statistics() {
+        m_imp->reset_statistics();
+    }
+    void clp::collect_statistics(statistics& st) const {
+        m_imp->collect_statistics(st);
+    }
+    void clp::display_certificate(std::ostream& out) const {
+        m_imp->display_certificate(out);
+    }
+    expr_ref clp::get_answer() {
+        return m_imp->get_answer();
+    }
+
+};
diff --git a/src/muz_qe/clp_context.h b/src/muz_qe/clp_context.h
new file mode 100644
index 000000000..635891205
--- /dev/null
+++ b/src/muz_qe/clp_context.h
@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    clp_context.h
+
+Abstract:
+
+    Bounded CLP (symbolic simulation using Z3) context.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-04-26
+
+Revision History:
+
+--*/
+#ifndef _CLP_CONTEXT_H_
+#define _CLP_CONTEXT_H_
+
+#include "ast.h"
+#include "lbool.h"
+#include "statistics.h"
+
+namespace datalog {
+    class context;
+
+    class clp {
+        class imp;
+        imp* m_imp;
+    public:
+        clp(context& ctx);
+        ~clp();
+        lbool query(expr* query);
+        void cancel();
+        void cleanup();
+        void reset_statistics();
+        void collect_statistics(statistics& st) const;
+        void display_certificate(std::ostream& out) const;        
+        expr_ref get_answer();
+    };
+};
+
+#endif
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 50915946a..0099b16f9 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -41,7 +41,6 @@ Revision History:
 #include"for_each_expr.h"
 #include"ast_smt_pp.h"
 #include"ast_smt2_pp.h"
-#include"expr_functors.h"
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_array_blast.h"
@@ -49,7 +48,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 {
@@ -226,6 +224,10 @@ namespace datalog {
         m_rewriter(m),
         m_var_subst(m),
         m_rule_manager(*this),
+        m_elim_unused_vars(m),
+        m_abstractor(m),
+        m_contains_p(*this),
+        m_check_pred(m_contains_p, m),
         m_transf(*this),
         m_trail(*this),
         m_pinned(m),
@@ -301,18 +303,19 @@ namespace datalog {
     expr_ref context::bind_variables(expr* fml, bool is_forall) {
         expr_ref result(m);
         app_ref_vector const & vars = m_vars;
+        rule_manager& rm = get_rule_manager();
         if (vars.empty()) {
             result = fml;
         }
         else {
-            ptr_vector<sort> sorts;
-            expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
-            get_free_vars(result, sorts);
+            m_names.reset();
+            m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
+            rm.collect_vars(result);
+            ptr_vector<sort>& sorts = rm.get_var_sorts();
             if (sorts.empty()) {
                 result = fml;
             }
             else {
-                svector<symbol> names;
                 for (unsigned i = 0; i < sorts.size(); ++i) {
                     if (!sorts[i]) {
                         if (i < vars.size()) { 
@@ -323,16 +326,16 @@ namespace datalog {
                         }
                     }
                     if (i < vars.size()) {
-                        names.push_back(vars[i]->get_decl()->get_name());
+                        m_names.push_back(vars[i]->get_decl()->get_name());
                     }
                     else {
-                        names.push_back(symbol(i));
+                        m_names.push_back(symbol(i));
                     }
                 }
                 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);
+                q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result); 
+                m_elim_unused_vars(q, result);
             }
         }
         return result;
@@ -544,6 +547,8 @@ namespace datalog {
             throw default_exception("get_num_levels is not supported for bmc");
         case TAB_ENGINE:
             throw default_exception("get_num_levels is not supported for tab");
+        case CLP_ENGINE:
+            throw default_exception("get_num_levels is not supported for clp");
         default:
             throw default_exception("unknown engine");
         } 
@@ -562,6 +567,8 @@ namespace datalog {
             throw default_exception("operation is not supported for BMC engine");
         case TAB_ENGINE:
             throw default_exception("operation is not supported for TAB engine");
+        case CLP_ENGINE:
+            throw default_exception("operation is not supported for CLP engine");
         default:
             throw default_exception("unknown engine");
         } 
@@ -581,6 +588,8 @@ namespace datalog {
             throw default_exception("operation is not supported for BMC engine");
         case TAB_ENGINE:
             throw default_exception("operation is not supported for TAB engine");
+        case CLP_ENGINE:
+            throw default_exception("operation is not supported for CLP engine");
         default:
             throw default_exception("unknown engine");
         } 
@@ -607,28 +616,16 @@ namespace datalog {
         }
     }
 
-    class context::contains_pred : public i_expr_pred {
-        context const& ctx;
-    public:
-        contains_pred(context& ctx): ctx(ctx) {}
-        virtual ~contains_pred() {}
-
-        virtual bool operator()(expr* e) {
-            return ctx.is_predicate(e);
-        }
-    };
 
     void context::check_existential_tail(rule_ref& r) {
         unsigned ut_size = r->get_uninterpreted_tail_size();
         unsigned t_size  = r->get_tail_size();   
-        contains_pred contains_p(*this);
-        check_pred check_pred(contains_p, get_manager());
         
         TRACE("dl", r->display_smt2(get_manager(), tout); tout << "\n";);
         for (unsigned i = ut_size; i < t_size; ++i) {
             app* t = r->get_tail(i);
             TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
-            if (check_pred(t)) {
+            if (m_check_pred(t)) {
                 std::ostringstream out;
                 out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate";
                 throw default_exception(out.str());
@@ -720,6 +717,10 @@ namespace datalog {
             check_existential_tail(r);
             check_positive_predicates(r);
             break;
+        case CLP_ENGINE:
+            check_existential_tail(r);
+            check_positive_predicates(r);
+            break;
         default:
             UNREACHABLE();
             break;
@@ -993,6 +994,9 @@ namespace datalog {
         else if (e == symbol("tab")) {
             m_engine = TAB_ENGINE;
         }
+        else if (e == symbol("clp")) {
+            m_engine = CLP_ENGINE;
+        }
 
         if (m_engine == LAST_ENGINE) {
             expr_fast_mark1 mark;
@@ -1028,6 +1032,8 @@ namespace datalog {
             return bmc_query(query);
         case TAB_ENGINE:
             return tab_query(query);
+        case CLP_ENGINE:
+            return clp_query(query);
         default:
             UNREACHABLE();
             return rel_query(query);
@@ -1092,11 +1098,22 @@ namespace datalog {
         }
     }
 
+    void context::ensure_clp() {
+        if (!m_clp.get()) {
+            m_clp = alloc(clp, *this);
+        }
+    }
+
     lbool context::tab_query(expr* query) {
         ensure_tab();
         return m_tab->query(query);
     }
 
+    lbool context::clp_query(expr* query) {
+        ensure_clp();
+        return m_clp->query(query);
+    }
+
     void context::ensure_rel() {
         if (!m_rel.get()) {
             m_rel = alloc(rel_context, *this);
@@ -1137,6 +1154,10 @@ namespace datalog {
             ensure_tab();
             m_last_answer = m_tab->get_answer();
             return m_last_answer.get();
+        case CLP_ENGINE:
+            ensure_clp();
+            m_last_answer = m_clp->get_answer();
+            return m_last_answer.get();
         default:
             UNREACHABLE();
         }
@@ -1162,6 +1183,10 @@ namespace datalog {
             ensure_tab();
             m_tab->display_certificate(out);
             return true;
+        case CLP_ENGINE:
+            ensure_clp();
+            m_clp->display_certificate(out);
+            return true;
         default: 
             return false;
         }        
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 74449940c..0a01b3e01 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -45,6 +45,9 @@ Revision History:
 #include"model2expr.h"
 #include"smt_params.h"
 #include"dl_rule_transformer.h"
+#include"expr_abstract.h"
+#include"expr_functors.h"
+#include"clp_context.h"
 
 namespace datalog {
 
@@ -76,6 +79,18 @@ namespace datalog {
         typedef obj_map<const func_decl, svector<symbol> > pred2syms;
         typedef obj_map<const sort, sort_domain*> sort_domain_map;
 
+        class contains_pred : public i_expr_pred {
+            context const& ctx;
+        public:
+            contains_pred(context& ctx): ctx(ctx) {}
+            virtual ~contains_pred() {}
+            
+            virtual bool operator()(expr* e) {
+                return ctx.is_predicate(e);
+            }
+        };
+
+
         ast_manager &      m;
         smt_params &       m_fparams;
         params_ref         m_params_ref;
@@ -84,10 +99,15 @@ namespace datalog {
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
+        unused_vars_eliminator m_elim_unused_vars;
+        expr_abstractor        m_abstractor;
+        contains_pred      m_contains_p;
+        check_pred         m_check_pred;
         rule_transformer   m_transf;
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
         app_ref_vector     m_vars;
+        svector<symbol>    m_names;
         sort_domain_map    m_sorts;
         func_decl_set      m_preds;
         sym2decl           m_preds_by_name;
@@ -104,6 +124,7 @@ namespace datalog {
         scoped_ptr<bmc>                 m_bmc;
         scoped_ptr<rel_context>         m_rel;
         scoped_ptr<tab>                 m_tab;
+        scoped_ptr<clp>                 m_clp;
 
         bool               m_closed;
         bool               m_saturation_was_run;
@@ -457,6 +478,8 @@ namespace datalog {
 
         void ensure_tab();
 
+        void ensure_clp();
+
         void ensure_rel();
 
         void new_query();
@@ -469,6 +492,8 @@ namespace datalog {
 
         lbool tab_query(expr* query);
 
+        lbool clp_query(expr* query);
+
         void check_quantifier_free(rule_ref& r);        
         void check_uninterpreted_free(rule_ref& r);
         void check_existential_tail(rule_ref& r);
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_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..afd586627 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,37 @@ 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_tail(m), 
+              m_itail_members(m),
+              m_conj(m) {
+        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";
@@ -385,15 +407,15 @@ namespace datalog {
             return false;
         }
 
-        ptr_vector<expr> todo;
+        m_todo.reset();
+        m_leqs.reset();
         for (unsigned i = u_len; i < len; i++) {
-            todo.push_back(r->get_tail(i));
+            m_todo.push_back(r->get_tail(i));
             SASSERT(!r->is_neg_tail(i));
         }
 
         m_rule_subst.reset(r);
 
-        obj_hashtable<expr> leqs;
         expr_ref_vector trail(m);
         expr_ref tmp1(m), tmp2(m);
         bool found_something = false;
@@ -401,10 +423,10 @@ namespace datalog {
 #define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; }
 #define IS_FLEX(_x) (is_var(_x) || m.is_value(_x))
 
-        while (!todo.empty()) {
+        while (!m_todo.empty()) {
             expr * arg1, *arg2;
-            expr * t0 = todo.back();
-            todo.pop_back();
+            expr * t0 = m_todo.back();
+            m_todo.pop_back();
             expr* t = t0;
             bool neg = m.is_not(t, t);
             if (is_var(t)) {
@@ -412,7 +434,7 @@ namespace datalog {
             }
             else if (!neg && m.is_and(t)) {
                 app* a = to_app(t);
-                todo.append(a->get_num_args(), a->get_args());
+                m_todo.append(a->get_num_args(), a->get_args());
             }
             else if (!neg && m.is_eq(t, arg1, arg2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
                 TRY_UNIFY(arg1, arg2);
@@ -440,12 +462,12 @@ namespace datalog {
             else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) {
                 tmp1 = a.mk_sub(arg1, arg2);
                 tmp2 = a.mk_sub(arg2, arg1);
-                if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
+                if (false && m_leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
                     TRY_UNIFY(arg1, arg2);
                 }
                 else {
                     trail.push_back(tmp1);
-                    leqs.insert(tmp1);
+                    m_leqs.insert(tmp1);
                 }
             }
         }
@@ -485,12 +507,12 @@ namespace datalog {
         }
         app_ref head(r->get_head(), m);
 
-        app_ref_vector tail(m);
-        svector<bool> tail_neg;
+        m_tail.reset();
+        m_tail_neg.reset();
 
         for (unsigned i=0; i<u_len; i++) {
-            tail.push_back(r->get_tail(i));
-            tail_neg.push_back(r->is_neg_tail(i));
+            m_tail.push_back(r->get_tail(i));
+            m_tail_neg.push_back(r->is_neg_tail(i));
         }
 
         bool modified = false;
@@ -502,12 +524,12 @@ namespace datalog {
             SASSERT(!r->is_neg_tail(u_len));
         }
         else {
-            expr_ref_vector itail_members(m);
+            m_itail_members.reset();
             for (unsigned i=u_len; i<len; i++) {
-                itail_members.push_back(r->get_tail(i));
+                m_itail_members.push_back(r->get_tail(i));
                 SASSERT(!r->is_neg_tail(i));
             }
-            itail = m.mk_and(itail_members.size(), itail_members.c_ptr());
+            itail = m.mk_and(m_itail_members.size(), m_itail_members.c_ptr());
             modified = true;
         }
 
@@ -523,21 +545,21 @@ namespace datalog {
         SASSERT(m.is_bool(simp_res));
 
         if (modified) {
-            expr_ref_vector conjs(m);
-            flatten_and(simp_res, conjs);
-            for (unsigned i = 0; i < conjs.size(); ++i) {
-                expr* e = conjs[i].get();
+            m_conj.reset();
+            flatten_and(simp_res, m_conj);
+            for (unsigned i = 0; i < m_conj.size(); ++i) {
+                expr* e = m_conj[i].get();
                 if (is_app(e)) {
-                    tail.push_back(to_app(e));
+                    m_tail.push_back(to_app(e));
                 }
                 else {
-                    tail.push_back(m.mk_eq(e, m.mk_true()));
+                    m_tail.push_back(m.mk_eq(e, m.mk_true()));
                 }
-                tail_neg.push_back(false);
+                m_tail_neg.push_back(false);
             }
 
-            SASSERT(tail.size() == tail_neg.size());
-            res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+            SASSERT(m_tail.size() == m_tail_neg.size());
+            res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr());
             res->set_accounting_parent_object(m_context, r);
         }
         else {
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h
index 247b20755..5047e1c6e 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,23 @@ 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;
+        ptr_vector<expr> m_todo;
+        obj_hashtable<expr> m_leqs;
+        app_ref_vector    m_tail;
+        expr_ref_vector   m_itail_members;
+        expr_ref_vector   m_conj;
+        svector<bool>     m_tail_neg;
+        normalizer_cfg*   m_cfg;
+        normalizer_rw*    m_rw;
 
-        class normalizer_cfg;
 
         void simplify_expr(app * a, expr_ref& res);
 
@@ -77,13 +89,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 8428d9049..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;
@@ -709,8 +705,7 @@ namespace datalog {
 
 #define PRT(_x_) ((_x_)?"T":"F")
 
-    bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
-        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
+    bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
         bool done_something = false;        
         unsigned sz = rules->get_num_rules();
 
@@ -731,7 +726,7 @@ namespace datalog {
         svector<bool>& can_expand = m_head_visitor.can_expand();
 
         for (unsigned i = 0; i < sz; ++i) {
-            add_rule(source, acc[i].get(), i);
+            add_rule(*rules, acc[i].get(), i);
         }
 
         // initialize substitution.
@@ -808,7 +803,7 @@ namespace datalog {
                 TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
 
                 del_rule(r, i);
-                add_rule(source, rl_res.get(), i);
+                add_rule(*rules, rl_res.get(), i);
                 
 
                 r = rl_res;
@@ -828,13 +823,15 @@ namespace datalog {
             }
         }
         if (done_something) {
-            rules = alloc(rule_set, m_context);
+            scoped_ptr<rule_set> res = alloc(rule_set, m_context);
             for (unsigned i = 0; i < sz; ++i) {
                 if (valid.get(i)) {
-                    rules->add_rule(acc[i].get());
+                    res->add_rule(acc[i].get());
                 }
             }
-            TRACE("dl", rules->display(tout););
+            res->inherit_predicates(*rules);
+            TRACE("dl", res->display(tout););
+            rules = res.detach();
         }        
         return done_something;
     }
@@ -871,11 +868,17 @@ namespace datalog {
             // try eager inlining
             if (do_eager_inlining(res)) {
                 something_done = true;
-            }
+            }            
             TRACE("dl", res->display(tout << "after eager inlining\n"););
+        }    
+        if (something_done) {
+            res->inherit_predicates(source);
+        }
+        else {
+            res = alloc(rule_set, source);
         }
 
-        if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
+        if (m_context.get_params().inline_linear() && inline_linear(res)) {
             something_done = true;
         }
 
@@ -883,7 +886,6 @@ namespace datalog {
             res = 0;
         }
         else {
-            res->inherit_predicates(source);
             m_context.add_model_converter(hsmc.get());
         }
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index 476c6b4b0..3a933f990 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -172,7 +172,7 @@ namespace datalog {
         /**
            Inline predicates that are known to not be join-points.
          */
-        bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
+        bool inline_linear(scoped_ptr<rule_set>& rules);
 
         void add_rule(rule_set const& rule_set, rule* r, unsigned i);
         void del_rule(rule* r, unsigned i);
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_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 21c3486b3..89804447b 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -725,6 +725,9 @@ namespace datalog {
                     m_mc->add_predicate(p, f);
                 }
             }
+            else if (src.is_output_predicate(p)) {
+                dst.set_output_predicate(p);
+            }
         }
     }
 
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp
index 0e94ba3b9..8c9e7e69f 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.cpp
+++ b/src/muz_qe/dl_mk_subsumption_checker.cpp
@@ -241,6 +241,7 @@ namespace datalog {
             tgt.add_rule(new_rule);
             subs_index.add(new_rule);
         }
+        tgt.inherit_predicates(orig);
         TRACE("dl",
             tout << "original set size: "<<orig.get_num_rules()<<"\n"
                  << "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
@@ -338,7 +339,7 @@ namespace datalog {
         rule_set * res = alloc(rule_set, m_context);
         bool modified = transform_rules(source, *res);
 
-        if(!m_have_new_total_rule && !modified) {
+        if (!m_have_new_total_rule && !modified) {
             dealloc(res);
             return 0;
         }
@@ -347,7 +348,7 @@ namespace datalog {
         //During the construction of the new set we may discover new total relations
         //(by quantifier elimination on the uninterpreted tails).
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
-        while(m_have_new_total_rule) {
+        while (m_have_new_total_rule) {
             m_have_new_total_rule = false;
 
             rule_set * old = res;
@@ -355,7 +356,6 @@ namespace datalog {
             transform_rules(*old, *res);
             dealloc(old);
         }
-        res->inherit_predicates(source);
 
         return res;
     }
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 92f504bcc..e43445396 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -40,15 +40,20 @@ Revision History:
 #include"quant_hoist.h"
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
-#include"qe_lite.h"
 #include"expr_safe_replace.h"
-#include"hnf.h"
 
 namespace datalog {
 
     rule_manager::rule_manager(context& ctx) 
         : m(ctx.get_manager()),
-          m_ctx(ctx) {}
+          m_ctx(ctx),
+          m_body(m),
+          m_head(m),
+          m_args(m),
+          m_hnf(m),
+          m_qe(m),
+          m_cfg(m),
+          m_rwr(m, false, m_cfg) {}
 
     void rule_manager::inc_ref(rule * r) {
         if (r) {
@@ -67,29 +72,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 +93,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);
@@ -125,13 +182,13 @@ namespace datalog {
     }
 
     void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
-        hnf h(m);
         expr_ref_vector fmls(m);
         proof_ref_vector prs(m);
-        h.set_name(name);
-        h(fml, p, fmls, prs);
-        for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
-            m_ctx.register_predicate(h.get_fresh_predicates()[i], false);
+        m_hnf.reset();
+        m_hnf.set_name(name);
+        m_hnf(fml, p, fmls, prs);
+        for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) {
+            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);
@@ -140,24 +197,23 @@ namespace datalog {
 
     void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
         
-        app_ref_vector body(m);
-        app_ref head(m);
-        svector<bool> is_negated;
-        unsigned index = extract_horn(fml, body, head);
-        hoist_compound_predicates(index, head, body);
+        m_body.reset();
+        m_neg.reset();
+        unsigned index = extract_horn(fml, m_body, m_head);
+        hoist_compound_predicates(index, m_head, m_body);
         TRACE("dl_rule",
               tout << mk_pp(head, m) << " :- ";
-              for (unsigned i = 0; i < body.size(); ++i) {
-                  tout << mk_pp(body[i].get(), m) << " ";
+              for (unsigned i = 0; i < m_body.size(); ++i) {
+                  tout << mk_pp(m_body[i].get(), m) << " ";
               }
               tout << "\n";);
 
 
-        mk_negations(body, is_negated);
-        check_valid_rule(head, body.size(), body.c_ptr());
+        mk_negations(m_body, m_neg);
+        check_valid_rule(m_head, m_body.size(), m_body.c_ptr());
 
         rule_ref r(*this);
-        r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
+        r = mk(m_head.get(), m_body.size(), m_body.c_ptr(), m_neg.c_ptr(), name);
 
         expr_ref fml1(m);
         if (p) {
@@ -326,28 +382,28 @@ namespace datalog {
             fml = m.mk_not(fml);
             return;
         }
-        expr_ref_vector args(m);
         if (!m_ctx.is_predicate(fml)) {
             return;
         }
+        m_args.reset();
         for (unsigned i = 0; i < fml->get_num_args(); ++i) {
             e = fml->get_arg(i);
             if (!is_app(e)) {
-                args.push_back(e);
+                m_args.push_back(e);
                 continue;
             }
             app* b = to_app(e);
 
             if (m.is_value(b)) {
-                args.push_back(e);
+                m_args.push_back(e);
             }
             else {
                 var* v = m.mk_var(num_bound++, m.get_sort(b));
-                args.push_back(v);
+                m_args.push_back(v);
                 body.push_back(m.mk_eq(v, b));
             }
         }
-        fml = m.mk_app(fml->get_decl(), args.size(), args.c_ptr());
+        fml = m.mk_app(fml->get_decl(), m_args.size(), m_args.c_ptr());
         TRACE("dl_rule", tout << mk_pp(fml.get(), m) << "\n";);
     }
 
@@ -511,29 +567,22 @@ namespace datalog {
     void rule_manager::reduce_unbound_vars(rule_ref& r) {
         unsigned ut_len = r->get_uninterpreted_tail_size();
         unsigned t_len = r->get_tail_size();
-        ptr_vector<sort> vars;
-        uint_set index_set;
-        qe_lite qe(m);
         expr_ref_vector conjs(m);
 
         if (ut_len == t_len) {
             return;
         }
 
-        get_free_vars(r->get_head(), vars);
+        reset_collect_vars();
+        accumulate_vars(r->get_head());
         for (unsigned i = 0; i < ut_len; ++i) {
-            get_free_vars(r->get_tail(i), vars);
+            accumulate_vars(r->get_tail(i));
         }
+        var_idx_set& index_set = finalize_collect_vars();
         for (unsigned i = ut_len; i < t_len; ++i) {
             conjs.push_back(r->get_tail(i));
         }
-
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            if (vars[i]) {
-                index_set.insert(i);
-            }
-        }
-        qe(index_set, false, conjs);
+        m_qe(index_set, false, conjs);
         bool change = conjs.size() != t_len - ut_len;
         for (unsigned i = 0; !change && i < conjs.size(); ++i) {
             change = r->get_tail(ut_len+i) != conjs[i].get();
@@ -570,15 +619,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 +954,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();
@@ -1004,16 +1052,14 @@ namespace datalog {
         }
         svector<symbol> names;
         used_symbols<> us;
-        
-        us(fml);
-        sorts.reverse();
-        
         for (unsigned i = 0; i < sorts.size(); ++i) {
             if (!sorts[i]) {
                 sorts[i] = m.mk_bool_sort();
             }
         }
-
+               
+        us(fml);
+        sorts.reverse();
         for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
             for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
                 func_decl_ref f(m);
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 666ddbd50..6335c506f 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -27,6 +27,9 @@ Revision History:
 #include"proof_converter.h"
 #include"model_converter.h"
 #include"ast_counter.h"
+#include"rewriter.h"
+#include"hnf.h"
+#include"qe_lite.h"
 
 namespace datalog {
 
@@ -47,9 +50,33 @@ 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;
+        app_ref_vector       m_body;
+        app_ref              m_head;
+        expr_ref_vector      m_args;
+        svector<bool>        m_neg;
+        hnf                  m_hnf;
+        qe_lite              m_qe;
+        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 +117,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 +129,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..ea2def025 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -54,6 +54,7 @@ namespace datalog {
         BMC_ENGINE,
         QBMC_ENGINE,
         TAB_ENGINE,
+        CLP_ENGINE,
         LAST_ENGINE
     };
 
@@ -81,33 +82,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/hnf.cpp b/src/muz_qe/hnf.cpp
index 5a7d1c4ba..764d31bb6 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz_qe/hnf.cpp
@@ -71,6 +71,9 @@ class hnf::imp {
     obj_map<expr, app*>   m_memoize_disj;
     obj_map<expr, proof*> m_memoize_proof;
     func_decl_ref_vector  m_fresh_predicates;
+    expr_ref_vector       m_body;
+    proof_ref_vector      m_defs;
+
 
 public:
     imp(ast_manager & m):
@@ -82,7 +85,9 @@ public:
         m_refs(m), 
         m_name("P"),
         m_qh(m),
-        m_fresh_predicates(m) {
+        m_fresh_predicates(m),
+        m_body(m),
+        m_defs(m) {
     }
 
     void operator()(expr * n, 
@@ -182,13 +187,13 @@ private:
 
     void mk_horn(expr_ref& fml, proof_ref& premise) {
         expr* e1, *e2;
-        expr_ref_vector body(m);
-        proof_ref_vector defs(m);
         expr_ref fml0(m), fml1(m), fml2(m), head(m);
         proof_ref p(m);
         fml0 = fml;
         m_names.reset();
         m_sorts.reset();
+        m_body.reset();
+        m_defs.reset();
         m_qh.pull_quantifier(true, fml0, &m_sorts, &m_names);
         if (premise){
             fml1 = bind_variables(fml0);
@@ -199,12 +204,12 @@ private:
         }
         head = fml0;
         while (m.is_implies(head, e1, e2)) {
-            body.push_back(e1);
+            m_body.push_back(e1);
             head = e2;
         }
-        datalog::flatten_and(body);
+        datalog::flatten_and(m_body);
         if (premise) {
-            p = m.mk_rewrite(fml0, mk_implies(body, head));
+            p = m.mk_rewrite(fml0, mk_implies(m_body, head));
         }
 
         //
@@ -214,8 +219,8 @@ private:
         // A -> C
         // B -> C
         // 
-        if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
-            app* _or = to_app(body[0].get());
+        if (m_body.size() == 1 && m.is_or(m_body[0].get()) && contains_predicate(m_body[0].get())) {
+            app* _or = to_app(m_body[0].get());
             unsigned sz = _or->get_num_args();
             expr* const* args = _or->get_args();
             for (unsigned i = 0; i < sz; ++i) {
@@ -224,7 +229,7 @@ private:
             } 
 
             if (premise) {
-                expr_ref f1 = bind_variables(mk_implies(body, head));
+                expr_ref f1 = bind_variables(mk_implies(m_body, head));
                 expr* f2 = m.mk_and(sz, m_todo.c_ptr()+m_todo.size()-sz);
                 proof_ref p2(m), p3(m);
                 p2 = m.mk_def_axiom(m.mk_iff(f1, f2));
@@ -240,13 +245,13 @@ private:
         }
 
 
-        eliminate_disjunctions(body, defs);
-        p = mk_congruence(p, body, head, defs);
+        eliminate_disjunctions(m_body, m_defs);
+        p = mk_congruence(p, m_body, head, m_defs);
 
-        eliminate_quantifier_body(body, defs);
-        p = mk_congruence(p, body, head, defs);          
+        eliminate_quantifier_body(m_body, m_defs);
+        p = mk_congruence(p, m_body, head, m_defs);          
 
-        fml2 = mk_implies(body, head);
+        fml2 = mk_implies(m_body, head);
 
         fml = bind_variables(fml2);
 
diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp
index 374333a9c..ced4e657b 100644
--- a/src/muz_qe/horn_subsume_model_converter.cpp
+++ b/src/muz_qe/horn_subsume_model_converter.cpp
@@ -28,10 +28,8 @@ Revision History:
 #include "well_sorted.h"
 
 void horn_subsume_model_converter::insert(app* head, expr* body) {
-    func_decl_ref pred(m);
-    expr_ref      body_res(m);
-    VERIFY(mk_horn(head, body, pred, body_res));
-    insert(pred.get(), body_res.get());
+    m_delay_head.push_back(head);
+    m_delay_body.push_back(body);
 }
 
 void horn_subsume_model_converter::insert(app* head, unsigned sz, expr* const* body) {
@@ -148,6 +146,7 @@ bool horn_subsume_model_converter::mk_horn(
 }
 
 void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
+
     //
     // predicates that have not been assigned values 
     // in the Horn model are assumed false.
@@ -174,6 +173,16 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
 
 
 void horn_subsume_model_converter::operator()(model_ref& mr) {
+
+    func_decl_ref pred(m);
+    expr_ref      body_res(m);
+    for (unsigned i = 0; i < m_delay_head.size(); ++i) {
+        VERIFY(mk_horn(m_delay_head[i].get(), m_delay_body[i].get(), pred, body_res));
+        insert(pred.get(), body_res.get());
+    }
+    m_delay_head.reset();
+    m_delay_body.reset();
+
     TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
     for (unsigned i = m_funcs.size(); i > 0; ) {
         --i;
diff --git a/src/muz_qe/horn_subsume_model_converter.h b/src/muz_qe/horn_subsume_model_converter.h
index edde02b19..993f29cc9 100644
--- a/src/muz_qe/horn_subsume_model_converter.h
+++ b/src/muz_qe/horn_subsume_model_converter.h
@@ -43,6 +43,8 @@ class horn_subsume_model_converter : public model_converter {
     func_decl_ref_vector m_funcs;
     expr_ref_vector      m_bodies;
     th_rewriter          m_rewrite;
+    app_ref_vector       m_delay_head;
+    expr_ref_vector      m_delay_body;
 
     void add_default_false_interpretation(expr* e, model_ref& md);
 
@@ -56,7 +58,9 @@ class horn_subsume_model_converter : public model_converter {
 
 public:
 
-    horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m), m_rewrite(m) {}
+ horn_subsume_model_converter(ast_manager& m): 
+    m(m), m_funcs(m), m_bodies(m), m_rewrite(m),
+        m_delay_head(m), m_delay_body(m) {}
 
     bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body);
 
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 1a8f562d9..5db4f1a00 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -125,12 +125,13 @@ class horn_tactic : public tactic {
         enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
 
         formula_kind get_formula_kind(expr_ref& f) {
-            normalize(f);
+            expr_ref tmp(f);
+            normalize(tmp);
             ast_mark mark;
             expr_ref_vector args(m), body(m);
             expr_ref head(m);
             expr* a = 0, *a1 = 0;
-            datalog::flatten_or(f, args);
+            datalog::flatten_or(tmp, args);
             for (unsigned i = 0; i < args.size(); ++i) {
                 a = args[i].get(); 
                 check_predicate(mark, a);
@@ -147,12 +148,12 @@ class horn_tactic : public tactic {
                     body.push_back(m.mk_not(a));
                 }
             }
-            f = m.mk_and(body.size(), body.c_ptr());
             if (head) {
-                f = m.mk_implies(f, head);
+                // f = m.mk_implies(f, head);
                 return IS_RULE;
             }
             else {
+                f = m.mk_and(body.size(), body.c_ptr());
                 return IS_QUERY;
             }
         }
@@ -171,7 +172,7 @@ class horn_tactic : public tactic {
             tactic_report report("horn", *g);
             bool produce_proofs = g->proofs_enabled();
 
-            if (produce_proofs) {
+            if (produce_proofs) {                
                 if (!m_ctx.get_params().generate_proof_trace()) {
                     params_ref params = m_ctx.get_params().p;
                     params.set_bool("generate_proof_trace", true);
@@ -239,10 +240,13 @@ class horn_tactic : public tactic {
             switch (is_reachable) {
             case l_true: {
                 // goal is unsat
-                g->assert_expr(m.mk_false());
                 if (produce_proofs) {
                     proof_ref proof = m_ctx.get_proof();
                     pc = proof2proof_converter(m, proof);
+                    g->assert_expr(m.mk_false(), proof, 0);
+                }
+                else {
+                    g->assert_expr(m.mk_false());
                 }
                 break;    
             }
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index a240a9aef..62b119538 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -43,6 +43,7 @@ Notes:
 #include "ast_ll_pp.h"
 #include "proof_checker.h"
 #include "smt_value_sort.h"
+#include "proof_utils.h"
 
 namespace pdr {
 
@@ -275,7 +276,7 @@ namespace pdr {
                 src.pop_back();
             }
             else if (is_invariant(tgt_level, curr, false, assumes_level)) {
-                
+
                 add_property(curr, assumes_level?tgt_level:infty_level);
                 TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);              
                 src[i] = src.back();
@@ -1225,6 +1226,7 @@ namespace pdr {
           m_search(m_params.bfs_model_search()),
           m_last_result(l_undef),
           m_inductive_lvl(0),
+          m_expanded_lvl(0),
           m_cancel(false)
     {
     }
@@ -1680,6 +1682,9 @@ namespace pdr {
         proof = m_search.get_proof_trace(*this);
         TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
         apply(m, m_pc.get(), proof);
+        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        // proof_utils::push_instantiations_up(proof);
+        // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
         return proof;
     }
 
@@ -1711,6 +1716,7 @@ namespace pdr {
         bool reachable;
         while (true) {
             checkpoint();
+            m_expanded_lvl = lvl;
             reachable = check_reachability(lvl);
             if (reachable) {
                 throw model_exception();
@@ -1769,6 +1775,10 @@ namespace pdr {
     void context::expand_node(model_node& n) {
         SASSERT(n.is_open());
         expr_ref_vector cube(m);
+        
+        if (n.level() < m_expanded_lvl) {
+            m_expanded_lvl = n.level();
+        }
 
         if (n.pt().is_reachable(n.state())) {
             TRACE("pdr", tout << "reachable\n";);
@@ -1835,7 +1845,7 @@ namespace pdr {
         if (m_params.simplify_formulas_pre()) {
             simplify_formulas();
         }
-        for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
+        for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
             checkpoint();
             bool all_propagated = true;
             decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 6aa02ef10..b5652d1b6 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -303,6 +303,7 @@ namespace pdr {
         mutable model_search m_search;
         lbool                m_last_result;
         unsigned             m_inductive_lvl;
+        unsigned             m_expanded_lvl;
         ptr_vector<core_generalizer>  m_core_generalizers;
         stats                m_stats;
         volatile bool        m_cancel;
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 237cf9415..62185f1d2 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -1081,6 +1081,7 @@ namespace pdr {
         arith_util a;
         bv_util    bv;
         bool m_is_dl;
+        bool m_test_for_utvpi;
 
         bool is_numeric(expr* e) const {
             if (a.is_numeral(e)) {
@@ -1115,6 +1116,16 @@ namespace pdr {
                 }
                 return false;
             }
+            if (m_test_for_utvpi) {
+                if (a.is_mul(e, e1, e2)) {
+                    if (is_minus_one(e1)) {
+                        return is_offset(e2);
+                    }
+                    if (is_minus_one(e2)) {
+                        return is_offset(e1);
+                    }
+                }
+            }
             return !is_arith_expr(e);
         }
 
@@ -1140,6 +1151,9 @@ namespace pdr {
             if (!a.is_add(lhs, arg1, arg2)) 
                 return false;    
             // x
+            if (m_test_for_utvpi) {
+                return is_offset(arg1) && is_offset(arg2);
+            }
             if (is_arith_expr(arg1)) 
                 std::swap(arg1, arg2);
             if (is_arith_expr(arg1))
@@ -1209,8 +1223,10 @@ namespace pdr {
         }
 
     public:
-        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
-        
+        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
+       
+        void test_for_utvpi() { m_test_for_utvpi = true; }
+
         void operator()(expr* e) {
             if (!m_is_dl) {
                 return;
@@ -1248,6 +1264,16 @@ namespace pdr {
         return test.is_dl();
     }  
 
+    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
+        test_diff_logic test(m);
+        test.test_for_utvpi();
+        expr_fast_mark1 mark;
+        for (unsigned i = 0; i < num_fmls; ++i) {
+            quick_for_each_expr(test, mark, fmls[i]);
+        } 
+        return test.is_dl();
+    }  
+
 }
 
 template class rewriter_tpl<pdr::ite_hoister_cfg>;
diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h
index ddbf0d122..5f2d22b76 100644
--- a/src/muz_qe/pdr_util.h
+++ b/src/muz_qe/pdr_util.h
@@ -151,6 +151,8 @@ namespace pdr {
 
     bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
 
+    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
+
 }
 
 #endif
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index 369c3aae6..36e721b5c 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -1,6 +1,7 @@
 #include "dl_util.h"
 #include "proof_utils.h"
 #include "ast_smt2_pp.h"
+#include "var_subst.h"
 
 class reduce_hypotheses {
     typedef obj_hashtable<expr> expr_set;
@@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) {
     obj_map<proof,proof*> cache;
     ::permute_unit_resolution(refs, cache, pr);
 }
+
+class push_instantiations_up_cl {
+    ast_manager& m;
+public:
+    push_instantiations_up_cl(ast_manager& m): m(m) {}
+
+    void operator()(proof_ref& p) {
+        expr_ref_vector s0(m);
+        p = push(p, s0);
+    }
+
+private:
+
+    proof* push(proof* p, expr_ref_vector const& sub) {
+        proof_ref_vector premises(m);
+        expr_ref conclusion(m);
+        svector<std::pair<unsigned, unsigned> >  positions;
+        vector<expr_ref_vector> substs;
+
+        if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
+            for (unsigned i = 0; i < premises.size(); ++i) {
+                compose(substs[i], sub);
+                premises[i] = push(premises[i].get(), substs[i]);
+                substs[i].reset();
+            }
+            instantiate(sub, conclusion);
+            return 
+                m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, 
+                                   positions, 
+                                   substs);
+        }        
+        if (sub.empty()) {
+            return p;
+        }
+        if (m.is_modus_ponens(p)) {
+            SASSERT(m.get_num_parents(p) == 2);
+            proof* p0 = m.get_parent(p, 0);
+            proof* p1 = m.get_parent(p, 1);
+            if (m.get_fact(p0) == m.get_fact(p)) {
+                return push(p0, sub);
+            }
+            expr* e1, *e2;
+            if (m.is_rewrite(p1, e1, e2) && 
+                is_quantifier(e1) && is_quantifier(e2) &&
+                to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
+                expr_ref r1(e1,m), r2(e2,m);
+                instantiate(sub, r1);
+                instantiate(sub, r2);
+                p1 = m.mk_rewrite(r1, r2);
+                return m.mk_modus_ponens(push(p0, sub), p1);
+            }
+        }
+        premises.push_back(p);
+        substs.push_back(sub);
+        conclusion = m.get_fact(p);
+        instantiate(sub, conclusion);
+        return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
+    }
+
+    void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
+        for (unsigned i = 0; i < sub.size(); ++i) {
+            expr_ref e(m);
+            var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
+            sub[i] = e;            
+        }
+    }
+
+    void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
+        if (sub.empty()) {
+            return;
+        }
+        if (!is_forall(fml)) {
+            return;
+        }
+        quantifier* q = to_quantifier(fml);
+        if (q->get_num_decls() != sub.size()) {
+            TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
+                  tout << mk_pp(q, m) << "\n";
+                  tout << sub.size() << "\n";);
+            return;
+        }
+        var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
+    }
+
+};
+
+void proof_utils::push_instantiations_up(proof_ref& pr) {
+    push_instantiations_up_cl push(pr.get_manager());
+    push(pr);
+}
diff --git a/src/muz_qe/proof_utils.h b/src/muz_qe/proof_utils.h
index 53a38592e..dc3cdc3ef 100644
--- a/src/muz_qe/proof_utils.h
+++ b/src/muz_qe/proof_utils.h
@@ -36,6 +36,12 @@ public:
     */
     static void permute_unit_resolution(proof_ref& pr);
 
+    /**
+       \brief Push instantiations created in hyper-resolutions up to leaves.
+       This produces a "ground" proof where leaves are annotated by instantiations.
+    */
+    static void push_instantiations_up(proof_ref& pr);
+
 };
 
 #endif
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/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 0698f4eaf..b5af6353e 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1159,7 +1159,7 @@ namespace smt2 {
             m_num_expr_frames++;
             unsigned num_vars = parse_sorted_vars();
             if (num_vars == 0)
-                throw parser_exception("invalied quantifier, list of sorted variables is empty");
+                throw parser_exception("invalid quantifier, list of sorted variables is empty");
         }
 
         symbol parse_indexed_identifier_core() {
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 55512f677..ae79446e3 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -94,7 +94,6 @@ public:
     smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {}
     
     virtual ~smt_strategic_solver_factory() {}
-    
     virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) {
         symbol l;
         if (m_logic != symbol::null)
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) {