diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index 099bdedec..a807237c5 100644
--- a/src/ast/rewriter/ast_counter.cpp
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -110,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;
         }
@@ -135,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;
         }
@@ -152,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/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 592c1ad4b..6aebf6e43 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"
@@ -227,6 +226,8 @@ namespace datalog {
         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),
@@ -302,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;
+            m_names.reset();
             m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
-            get_free_vars(result, sorts);
+            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()) { 
@@ -324,15 +326,15 @@ 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); 
+                q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result); 
                 m_elim_unused_vars(q, result);
             }
         }
@@ -608,28 +610,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());
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index aba8577e1..55b9f3010 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -46,6 +46,8 @@ Revision History:
 #include"smt_params.h"
 #include"dl_rule_transformer.h"
 #include"expr_abstract.h"
+#include"expr_functors.h"
+
 
 namespace datalog {
 
@@ -77,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;
@@ -87,10 +101,13 @@ namespace datalog {
         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;
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
index 8a9b1257a..afd586627 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
@@ -369,11 +369,14 @@ namespace datalog {
 
     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(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);
     }
@@ -404,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;
@@ -420,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)) {
@@ -431,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);
@@ -459,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);
                 }
             }
         }
@@ -504,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;
@@ -521,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;
         }
 
@@ -542,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 99e0b575a..5047e1c6e 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.h
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h
@@ -71,6 +71,12 @@ namespace datalog {
         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;
 
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 59d316ae7..e43445396 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -40,15 +40,18 @@ 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_body(m),
+          m_head(m),
+          m_args(m),
+          m_hnf(m),
+          m_qe(m),
           m_cfg(m),
           m_rwr(m, false, m_cfg) {}
 
@@ -179,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);
@@ -194,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) {
@@ -380,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";);
     }
 
@@ -565,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();
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 5abb64624..6335c506f 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -28,6 +28,8 @@ Revision History:
 #include"model_converter.h"
 #include"ast_counter.h"
 #include"rewriter.h"
+#include"hnf.h"
+#include"qe_lite.h"
 
 namespace datalog {
 
@@ -66,6 +68,12 @@ namespace datalog {
         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;
 
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);