diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index ea3b05e40..6d59cf650 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -701,7 +701,7 @@ typedef enum
        over Boolean connectives 'and' and 'or'.
 
     
-   - Z3_OP_PR_NFF_NEG: Proof for a (negative) NNF step. Examples:
+   - Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples:
           \nicebox{
           T1: (not s_1) ~ r_1
           ...
diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
new file mode 100644
index 000000000..c542abb60
--- /dev/null
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -0,0 +1,165 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    ast_counter.cpp
+
+Abstract:
+
+    Routines for counting features of terms, such as free variables.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-18.
+
+Revision History:
+
+--*/
+
+#include "ast_counter.h"
+#include "var_subst.h"
+
+void counter::update(unsigned el, int delta) {
+    int & counter = get(el);
+    SASSERT(!m_stay_non_negative || counter>=0);
+    SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
+    counter += delta;
+}
+
+int & counter::get(unsigned el) {
+    return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+}
+
+counter & counter::count(unsigned sz, const unsigned * els, int delta) {
+    for(unsigned i=0; i<sz; i++) {
+        update(els[i], delta);
+    }
+    return *this;
+}
+
+unsigned counter::get_positive_count() const {
+    unsigned cnt = 0;
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if( eit->m_value>0 ) { 
+            cnt++;
+        }
+    }
+    return cnt;
+}
+
+void counter::collect_positive(uint_set & acc) const {
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if(eit->m_value>0) { acc.insert(eit->m_key); }
+    }
+}
+
+bool counter::get_max_positive(unsigned & res) const {
+    bool found = false;
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if( eit->m_value>0 && (!found || eit->m_key>res) ) { 
+            found = true;
+            res = eit->m_key;
+        }
+    }
+    return found;
+}
+
+unsigned counter::get_max_positive() const {
+    unsigned max_pos;
+    VERIFY(get_max_positive(max_pos));
+    return max_pos;
+}
+
+int counter::get_max_counter_value() const {
+    int res = 0;
+    iterator eit = begin();
+    iterator eend = end();
+    for (; eit!=eend; ++eit) {
+        if( eit->m_value>res ) { 
+            res = eit->m_value;
+        }
+    }
+    return res;
+}
+
+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);
+        for (unsigned j = 0; j < m_sorts.size(); ++j) {
+            if (m_sorts[j]) {
+                update(j, coef);
+            }
+        }
+    }
+}
+
+
+unsigned var_counter::get_max_var(bool& has_var) {
+    has_var = false;
+    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: {
+            quantifier* q = to_quantifier(e);
+            m_todo.push_back(q->get_expr());
+            m_scopes.push_back(scope + q->get_num_decls());
+            break;                 
+        }
+        case AST_VAR: {
+            if (to_var(e)->get_idx() >= scope + max_var) {
+                has_var = true;
+                max_var = to_var(e)->get_idx() - scope;
+            }
+            break;
+        }
+        case AST_APP: {
+            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;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+    m_visited.reset();
+    return max_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
new file mode 100644
index 000000000..2a581c302
--- /dev/null
+++ b/src/ast/rewriter/ast_counter.h
@@ -0,0 +1,107 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    ast_counter.h
+
+Abstract:
+
+    Routines for counting features of terms, such as free variables.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-18.
+    Krystof Hoder (t-khoder) 2010-10-10.
+
+Revision History:
+
+    Hoisted from dl_util.h 2013-03-18.
+
+--*/
+
+
+#ifndef _AST_COUNTER_H_
+#define _AST_COUNTER_H_
+
+#include "ast.h"
+#include "map.h"
+#include "uint_set.h"
+
+class counter {
+protected:
+    typedef u_map<int> map_impl;
+    map_impl m_data;
+    const bool m_stay_non_negative;
+public:
+    typedef map_impl::iterator iterator;
+    
+    counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    
+    iterator begin() const { return m_data.begin(); }
+    iterator end() const { return m_data.end(); }    
+    void update(unsigned el, int delta);
+    int & get(unsigned el);
+
+    /**
+       \brief Increase values of elements in \c els by \c delta.
+       
+       The function returns a reference to \c *this to allow for expressions like
+       counter().count(sz, arr).get_positive_count()
+    */
+    counter & count(unsigned sz, const unsigned * els, int delta = 1);
+    counter & count(const unsigned_vector & els, int delta = 1) {
+        return count(els.size(), els.c_ptr(), delta);
+    }
+    
+    void collect_positive(uint_set & acc) const;
+    unsigned get_positive_count() const;
+
+    bool get_max_positive(unsigned & res) const;
+    unsigned get_max_positive() const;
+
+    /**
+       Since the default counter value of a counter is zero, the result is never negative.
+    */
+    int get_max_counter_value() const;
+};
+
+class var_counter : public counter {
+protected:
+    ptr_vector<sort> m_sorts;
+    expr_fast_mark1  m_visited;
+    ptr_vector<expr> m_todo;
+    unsigned_vector  m_scopes;
+    unsigned get_max_var(bool & has_var);    
+public:
+    var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
+    void count_vars(ast_manager & m, const app * t, int coef = 1);
+    unsigned get_max_var(expr* e);
+    unsigned get_next_var(expr* e);
+};
+
+class ast_counter {
+    typedef obj_map<ast, int> map_impl;
+    map_impl m_data;
+    bool     m_stay_non_negative;
+ public:
+    typedef map_impl::iterator iterator;
+    
+    ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    
+    iterator begin() const { return m_data.begin(); }
+    iterator end() const { return m_data.end(); }
+    
+    int & get(ast * el) {
+        return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+    }
+    void update(ast * el, int delta){
+        get(el) += delta;
+        SASSERT(!m_stay_non_negative || get(el) >= 0);
+    }
+    
+    void inc(ast * el) { update(el, 1); }
+    void dec(ast * el) { update(el, -1); }
+};
+
+#endif
diff --git a/src/muz_qe/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
similarity index 100%
rename from src/muz_qe/expr_safe_replace.cpp
rename to src/ast/rewriter/expr_safe_replace.cpp
diff --git a/src/muz_qe/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h
similarity index 100%
rename from src/muz_qe/expr_safe_replace.h
rename to src/ast/rewriter/expr_safe_replace.h
diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index e4275ab9c..dd9062828 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "var_subst.h"
 #include "ast_pp.h"
 #include "ast_counter.h"
+#include "expr_safe_replace.h"
 
 //
 // Bring quantifiers of common type into prenex form.
@@ -42,7 +43,7 @@ public:
     
     void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
         quantifier_type qt = Q_none_pos;
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -52,7 +53,7 @@ public:
     
     void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
         quantifier_type qt = Q_exists_pos;
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -61,7 +62,7 @@ public:
     void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
         quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
         expr_ref result(m);
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -78,7 +79,57 @@ public:
         expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
         instantiate(m, q, exprs, result);
     }
-    
+
+    unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
+        unsigned index = var_counter().get_next_var(fml);
+        while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
+            quantifier* q = to_quantifier(fml);
+            index += q->get_num_decls();
+            if (names) {
+                names->append(q->get_num_decls(), q->get_decl_names());
+            }
+            if (sorts) {
+                sorts->append(q->get_num_decls(), q->get_decl_sorts());
+            }
+            fml = q->get_expr();
+        }
+        if (!has_quantifiers(fml)) {
+            return index;
+        }
+        app_ref_vector vars(m);
+        pull_quantifier(is_forall, fml, vars);
+        if (vars.empty()) {
+            return index;
+        }
+        // replace vars by de-bruijn indices
+        expr_safe_replace rep(m);
+        svector<symbol> bound_names;
+        ptr_vector<sort> bound_sorts;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            app* v = vars[i].get();
+            if (names) {
+                bound_names.push_back(v->get_decl()->get_name());
+            }                
+            if (sorts) {
+                bound_sorts.push_back(m.get_sort(v));
+            }
+            rep.insert(v, m.mk_var(index++, m.get_sort(v)));
+        }
+        if (names && !bound_names.empty()) {
+            bound_names.reverse();
+            bound_names.append(*names);
+            names->reset();
+            names->append(bound_names);
+        }
+        if (sorts && !bound_sorts.empty()) {
+            bound_sorts.reverse();
+            bound_sorts.append(*sorts);
+            sorts->reset();
+            sorts->append(bound_sorts);
+        }
+        rep(fml);
+        return index;
+    }    
     
 private:
     
@@ -143,7 +194,7 @@ private:
     }
     
     
-    void pull_quantifiers(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
+    void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
         
         if (!has_quantifiers(fml)) {
             result = fml;
@@ -159,7 +210,7 @@ private:
             if (m.is_and(fml)) {
                 num_args = a->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifiers(a->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(a->get_arg(i), qt, vars, tmp);
                     args.push_back(tmp);
                 }
                 m_rewriter.mk_and(args.size(), args.c_ptr(), result);
@@ -167,25 +218,25 @@ private:
             else if (m.is_or(fml)) {
                 num_args = to_app(fml)->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifiers(to_app(fml)->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
                     args.push_back(tmp);
                 }
                 m_rewriter.mk_or(args.size(), args.c_ptr(), result);
             }
             else if (m.is_not(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
                 negate(qt);
                 result = m.mk_not(tmp);
             }
             else if (m.is_implies(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
                 negate(qt);
-                pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, result);
+                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, result);
                 result = m.mk_implies(tmp, result);
             }
             else if (m.is_ite(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, tmp);
-                pull_quantifiers(to_app(fml)->get_arg(2), qt, vars, result);
+                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(2), qt, vars, result);
                 result = m.mk_ite(to_app(fml)->get_arg(0), tmp, result);
             }
             else {
@@ -203,7 +254,7 @@ private:
             }
             set_quantifier_type(qt, q->is_forall());
             extract_quantifier(q, vars, tmp);
-            pull_quantifiers(tmp, qt, vars, result);
+            pull_quantifier(tmp, qt, vars, result);
             break;
         }
         case AST_VAR:
@@ -216,36 +267,6 @@ private:
         }
     }
 
-    unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
-        unsigned index = var_counter().get_next_var(fml);
-        while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
-            quantifier* q = to_quantifier(fml);
-            index += q->get_num_decls();
-            if (names) {
-                names->append(q->get_num_decls(), q->get_decl_names());
-            }
-            fml = q->get_expr();
-        }
-        if (!has_quantifiers(fml)) {
-            return index;
-        }
-        app_ref_vector vars(m);
-        pull_quantifier(is_forall, fml, vars);
-        if (vars.empty()) {
-            return index;
-        }
-        // replace vars by de-bruijn indices
-        expr_safe_replace rep(m);
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            app* v = vars[i].get();
-            if (names) {
-                names->push_back(v->get_decl()->get_name());
-            }                
-            rep.insert(v, m.mk_var(index++,m.get_sort(v)));
-        }
-        rep(fml);
-        return index;
-    }
 };   
 
 quantifier_hoister::quantifier_hoister(ast_manager& m) {
@@ -268,7 +289,6 @@ void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_
     m_impl->pull_quantifier(is_forall, fml, vars);
 }
 
-unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
-    return m_impl->pull_quantifier(is_forall, fml, names);
+unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
+    return m_impl->pull_quantifier(is_forall, fml, sorts, names);
 }
-
diff --git a/src/ast/rewriter/quant_hoist.h b/src/ast/rewriter/quant_hoist.h
index 70a79a0e2..df643950a 100644
--- a/src/ast/rewriter/quant_hoist.h
+++ b/src/ast/rewriter/quant_hoist.h
@@ -67,6 +67,7 @@ public:
     */
 
     unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
+
 };
 
 #endif
diff --git a/src/muz_qe/dl_base.cpp b/src/muz_qe/dl_base.cpp
index dd817754f..0f250d76c 100644
--- a/src/muz_qe/dl_base.cpp
+++ b/src/muz_qe/dl_base.cpp
@@ -233,7 +233,7 @@ namespace datalog {
         table_fact row;
         for(; it!=iend; ++it) {
             it->get_fact(row);
-            to_remove.append(row);
+            to_remove.push_back(row);
         }
         remove_facts(to_remove.size(), to_remove.c_ptr());
     }
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp
index a7c1bf7eb..959a11605 100644
--- a/src/muz_qe/dl_bmc_engine.cpp
+++ b/src/muz_qe/dl_bmc_engine.cpp
@@ -307,7 +307,7 @@ namespace datalog {
                     r1->to_formula(concl);
                     scoped_proof _sp(m);
                     
-                    proof* p = m.mk_asserted(fml);
+                    proof* p = r->get_proof();
                     proof* premises[2] = { pr, p };
                     
                     positions.push_back(std::make_pair(0, 1));
@@ -320,7 +320,7 @@ namespace datalog {
                 else {
                     r2->to_formula(concl);
                     scoped_proof _sp(m);
-                    proof* p = m.mk_asserted(fml);
+                    proof* p = r->get_proof();
                     if (sub.empty()) {
                         pr = p;
                     }
@@ -340,7 +340,7 @@ namespace datalog {
                 pred = r->get_decl(0);
             }
             scoped_proof _sp(m);
-            apply(m, b.m_pc.get(), pr);
+            apply(m, b.m_ctx.get_proof_converter().get(), pr);
             b.m_answer = pr;
             return l_true;
         }
@@ -474,6 +474,9 @@ namespace datalog {
         }
 
         proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
+            if (b.m_cancel) {
+                return proof_ref(0, m);
+            }
             TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
 
             expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m);
@@ -497,7 +500,7 @@ namespace datalog {
             SASSERT(r);
             r->to_formula(fml);
             IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";);
-            prs.push_back(m.mk_asserted(fml));
+            prs.push_back(r->get_proof());
             unsigned sz = r->get_uninterpreted_tail_size();
 
             ptr_vector<sort> rule_vars;
@@ -536,8 +539,9 @@ namespace datalog {
             model_ref md;
             b.m_solver.get_model(md);
             IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
-            proof_ref pr = get_proof(md, b.m_query_pred, to_app(level_query), level);
-            apply(m, b.m_pc.get(), pr);
+            proof_ref pr(m);
+            pr = get_proof(md, b.m_query_pred, to_app(level_query), level);
+            apply(m, b.m_ctx.get_proof_converter().get(), pr);
             b.m_answer = pr;
         }
 
@@ -1034,7 +1038,7 @@ namespace datalog {
                     var_subst vs(m, false);
                     mk_subst(*rules[i], path, trace, sub);
                     rules[i]->to_formula(fml);
-                    prs.push_back(m.mk_asserted(fml));
+                    prs.push_back(rules[i]->get_proof());
                     unsigned sz = trace->get_num_args();
                     if (sub.empty() && sz == 0) {
                         pr = prs[0].get();
@@ -1112,7 +1116,6 @@ namespace datalog {
         }
         
         void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) {                
-            proof_ref pr(m);            
             IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
             md->eval(trace, trace);
             md->eval(path, path);
@@ -1120,7 +1123,11 @@ namespace datalog {
                        for (unsigned i = 0; i < b.m_solver.size(); ++i) {
                            verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n";
                        });
-            b.m_answer = get_proof(md, to_app(trace), to_app(path));
+            scoped_proof _sp(m);
+            proof_ref pr(m);
+            pr = get_proof(md, to_app(trace), to_app(path));
+            apply(m, b.m_ctx.get_proof_converter().get(), pr);
+            b.m_answer = pr;
         }
        
     };
@@ -1155,6 +1162,9 @@ namespace datalog {
     private:
 
         void get_model(unsigned level) {
+            if (b.m_cancel) {
+                return;
+            }
             rule_manager& rm = b.m_ctx.get_rule_manager();
             expr_ref level_query = mk_level_predicate(b.m_query_pred, level);
             model_ref md;
@@ -1212,7 +1222,7 @@ namespace datalog {
                     r1->to_formula(concl);
                     scoped_proof _sp(m);
                     
-                    proof* p = m.mk_asserted(fml);
+                    proof* p = r->get_proof();
                     proof* premises[2] = { pr, p };
                     
                     positions.push_back(std::make_pair(0, 1));
@@ -1225,7 +1235,7 @@ namespace datalog {
                 else {
                     r2->to_formula(concl);
                     scoped_proof _sp(m);
-                    proof* p = m.mk_asserted(fml);
+                    proof* p = r->get_proof();
                     if (sub.empty()) {
                         pr = p;
                     }
@@ -1245,7 +1255,7 @@ namespace datalog {
                 pred = r->get_decl(0);
             }
             scoped_proof _sp(m);
-            apply(m, b.m_pc.get(), pr);
+            apply(m, b.m_ctx.get_proof_converter().get(), pr);
             b.m_answer = pr;
         }
         
@@ -1409,18 +1419,15 @@ namespace datalog {
 
         m_ctx.ensure_opened();
         m_rules.reset();
+
         datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
         datalog::rule_set        old_rules(m_ctx.get_rules());
         datalog::rule_ref_vector query_rules(rule_manager);
         datalog::rule_ref        query_rule(rule_manager);
-        model_converter_ref mc = datalog::mk_skip_model_converter();
-        m_pc = datalog::mk_skip_proof_converter();
-        m_ctx.set_model_converter(mc);
-        m_ctx.set_proof_converter(m_pc);
         rule_manager.mk_query(query, m_query_pred, query_rules, query_rule);
         m_ctx.add_rules(query_rules);
-        expr_ref bg_assertion = m_ctx.get_background_assertion();        
-
+        expr_ref bg_assertion = m_ctx.get_background_assertion();
+        
         m_ctx.set_output_predicate(m_query_pred);
         m_ctx.apply_default_transformation();
         
diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h
index 06901a160..5911f5f72 100644
--- a/src/muz_qe/dl_bmc_engine.h
+++ b/src/muz_qe/dl_bmc_engine.h
@@ -39,7 +39,6 @@ namespace datalog {
         func_decl_ref    m_query_pred;
         expr_ref         m_answer;
         volatile bool    m_cancel;
-        proof_converter_ref m_pc;
 
         void checkpoint();
 
diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp
index d7dfbe1ae..5081654b5 100644
--- a/src/muz_qe/dl_check_table.cpp
+++ b/src/muz_qe/dl_check_table.cpp
@@ -287,9 +287,6 @@ namespace datalog {
 
     bool check_table::well_formed() const {
         get_plugin().m_count++;
-        if (get_plugin().m_count == 497) {
-            std::cout << "here\n";
-        }
         iterator it = m_tocheck->begin(), end = m_tocheck->end();
         for (; it != end; ++it) {
             table_fact fact;
@@ -354,8 +351,8 @@ namespace datalog {
         return result;
     }
 
-    table_base * check_table::complement(func_decl* p) const {
-        check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
+    table_base * check_table::complement(func_decl* p, const table_element * func_columns) const {
+        check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p, func_columns), m_checker->complement(p, func_columns));
         return result;
     }
 
diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h
index 6f098f8bc..7126bde66 100644
--- a/src/muz_qe/dl_check_table.h
+++ b/src/muz_qe/dl_check_table.h
@@ -119,7 +119,7 @@ namespace datalog {
         virtual void add_fact(const table_fact & f);
         virtual void remove_fact(const table_element*  fact);
         virtual bool contains_fact(const table_fact & f) const;       
-        virtual table_base * complement(func_decl* p) const;
+        virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const;
         virtual table_base * clone() const;
 
         virtual iterator begin() const { SASSERT(well_formed()); return m_tocheck->begin(); }
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index c88e7346e..d49a8a671 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -262,8 +262,10 @@ public:
                 
             case datalog::OK: 
                 break;
+
             default:
-                UNREACHABLE();
+                // exception was raised.
+                break;
             }
             break;
         }
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index 44a449779..cc56df4b7 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -384,8 +384,8 @@ namespace datalog {
     void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
         SASSERT(r->get_positive_tail_size()==2);
         ast_manager & m = m_context.get_manager();
-        var_counter counter;
-        counter.count_vars(m, r);
+        rule_counter counter;
+        counter.count_rule_vars(m, r);
         app * t1 = r->get_tail(0);
         app * t2 = r->get_tail(1);
         counter.count_vars(m, t1, -1);
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index eb782aac8..89f2fcf4a 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -231,6 +231,7 @@ namespace datalog {
         m_rule_set(*this),
         m_rule_fmls(m),
         m_background(m),
+        m_mc(0),
         m_closed(false),
         m_saturation_was_run(false),
         m_last_answer(m),
@@ -474,10 +475,11 @@ namespace datalog {
     void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
         datalog::rule_ref_vector rules(rm);
-        rm.set_model_converter(m_mc);
-        rm.set_proof_converter(m_pc);
+        scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
-            rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
+            expr* fml = m_rule_fmls[i].get();
+            proof* p = generate_proof_trace()?m.mk_asserted(fml):0;
+            rm.mk_rule(fml, p, rules, m_rule_names[i]);
         }
         add_rules(rules);
         m_rule_fmls.reset();
@@ -491,7 +493,11 @@ namespace datalog {
     void context::update_rule(expr* rl, symbol const& name) {
         datalog::rule_manager& rm = get_rule_manager();
         datalog::rule_ref_vector rules(rm);
-        rm.mk_rule(rl, rules, name);
+        proof* p = 0;
+        if (generate_proof_trace()) {
+            p = m.mk_asserted(rl);
+        }
+        rm.mk_rule(rl, p, rules, name);
         if (rules.size() != 1) {
             std::stringstream strm;
             strm << "Rule " << name << " has a non-trivial body. It cannot be modified";
@@ -685,7 +691,7 @@ namespace datalog {
                 todo.push_back(e2);
             }
             else if (is_quantifier(e)) {
-                todo.append(to_quantifier(e)->get_expr());
+                todo.push_back(to_quantifier(e)->get_expr());
             }
             else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && 
                      m.is_true(e1)) {
@@ -739,6 +745,9 @@ namespace datalog {
             UNREACHABLE();
             break;
         }
+        if (generate_proof_trace() && !r->get_proof()) {
+            m_rule_manager.mk_rule_asserted_proof(*r.get());
+        }
     }
 
     void context::add_rule(rule_ref& r) {
@@ -849,7 +858,7 @@ namespace datalog {
     void context::transform_rules(rule_transformer& transf) {
         SASSERT(m_closed); //we must finish adding rules before we start transforming them
         TRACE("dl", display_rules(tout););
-        if (transf(m_rule_set, m_mc, m_pc)) {
+        if (transf(m_rule_set, m_mc)) {
             //we have already ensured the negation is stratified and transformations
             //should not break the stratification
             m_rule_set.ensure_closed();
@@ -1037,6 +1046,8 @@ namespace datalog {
     }
 
     void context::new_query() {
+        m_mc = mk_skip_model_converter();
+
         flush_add_rules();
         m_last_status = OK;
         m_last_answer = 0;
@@ -1148,6 +1159,7 @@ namespace datalog {
         switch(get_engine()) {
         case DATALOG_ENGINE:            
             return false;
+        case PDR_ENGINE: 
         case QPDR_ENGINE: 
             ensure_pdr();
             m_pdr->display_certificate(out);
@@ -1241,7 +1253,7 @@ namespace datalog {
             ptr_vector<sort> sorts;
             get_free_vars(m_rule_fmls[i].get(), sorts);
             if (!sorts.empty()) {
-                rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]);
+                rm.mk_rule(m_rule_fmls[i].get(), 0, rule_refs, m_rule_names[i]);
                 m_rule_fmls[i] = m_rule_fmls.back();
                 m_rule_names[i] = m_rule_names.back();
                 m_rule_fmls.pop_back();
@@ -1258,7 +1270,7 @@ namespace datalog {
         }
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
             rules.push_back(m_rule_fmls[i].get());
-            names.push_back(m_rule_names[i]);
+            names.push_back(m_rule_names[i]);            
         }
     }
  
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 7ca6b278c..d278d3abc 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -42,7 +42,6 @@ Revision History:
 #include"params.h"
 #include"trail.h"
 #include"model_converter.h"
-#include"proof_converter.h"
 #include"model2expr.h"
 #include"smt_params.h"
 #include"dl_rule_transformer.h"
@@ -85,9 +84,6 @@ namespace datalog {
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
         rule_transformer   m_transf;
-        model_converter_ref m_mc;
-        proof_converter_ref m_pc;
-
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
         app_ref_vector     m_vars;
@@ -99,6 +95,8 @@ namespace datalog {
         expr_ref_vector    m_rule_fmls;
         svector<symbol>    m_rule_names;
         expr_ref_vector    m_background;
+        model_converter_ref m_mc;
+        proof_converter_ref m_pc;
 
         scoped_ptr<pdr::dl_interface>   m_pdr;
         scoped_ptr<bmc>                 m_bmc;
@@ -144,6 +142,7 @@ namespace datalog {
         var_subst & get_var_subst() { return m_var_subst; }
         dl_decl_util & get_decl_util()  { return m_decl_util; }
 
+        bool generate_proof_trace() const { return m_params.generate_proof_trace(); }
         bool output_profile() const { return m_params.output_profile(); }
         bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
         symbol default_table() const { return m_params.default_table(); }
@@ -317,15 +316,15 @@ namespace datalog {
         void reopen();
         void ensure_opened();
 
-        void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
-        void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
+        model_converter_ref& get_model_converter() { return m_mc; }
+        proof_converter_ref& get_proof_converter() { return m_pc; }
+        void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); }
 
-        void transform_rules();
-        void transform_rules(rule_transformer::plugin* plugin);
-        void transform_rules(rule_transformer& transf);
+        void transform_rules(); 
+        void transform_rules(rule_transformer& transf); 
         void replace_rules(rule_set & rs);
 
-        void apply_default_transformation();
+        void apply_default_transformation(); 
 
         void collect_params(param_descrs& r);
         
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index b22fdf7ef..537b0b5ac 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -197,25 +197,18 @@ namespace datalog {
         }
 
         fml2 = m.mk_implies(body, head);
-        rm.mk_rule(fml2, new_rules, r.name());
+        proof_ref p(m);
+        rm.mk_rule(fml2, p, new_rules, r.name());
         SASSERT(new_rules.size() == 1);
 
         TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
         
         rules.add_rule(new_rules[0].get());
-        if (m_pc) {
-            new_rules[0]->to_formula(fml2);
-            m_pc->insert(fml1, fml2);
-        }
+        rm.mk_rule_rewrite_proof(r, *new_rules[0].get());
         return true;
     }
     
-    rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        ref<equiv_proof_converter> epc;
-        if (pc) {
-            epc = alloc(equiv_proof_converter, m);
-        }
-        m_pc = epc.get();
+    rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc) {
 
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::iterator it = source.begin(), end = source.end();
@@ -227,9 +220,6 @@ namespace datalog {
             dealloc(rules);
             rules = 0;
         }        
-        if (pc) {
-            pc = concat(pc.get(), epc.get());
-        }
         return rules;        
     }
 
diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h
index c0bb39da0..94eb64601 100644
--- a/src/muz_qe/dl_mk_array_blast.h
+++ b/src/muz_qe/dl_mk_array_blast.h
@@ -37,7 +37,6 @@ namespace datalog {
         rule_manager&   rm;
         params_ref      m_params;
         th_rewriter     m_rewriter;
-        equiv_proof_converter* m_pc;
 
         typedef obj_map<app, var*> defs_t;
 
@@ -55,7 +54,7 @@ namespace datalog {
 
         virtual ~mk_array_blast();
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
     };
 
diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp
index 1fa93a0ca..1e984f254 100644
--- a/src/muz_qe/dl_mk_bit_blast.cpp
+++ b/src/muz_qe/dl_mk_bit_blast.cpp
@@ -21,7 +21,8 @@ Revision History:
 #include "bit_blaster_rewriter.h"
 #include "rewriter_def.h"
 #include "ast_pp.h"
-
+#include "expr_safe_replace.h"
+#include "filter_model_converter.h"
 
 namespace datalog {
 
@@ -35,6 +36,73 @@ namespace datalog {
     // P(bv(x,y)) :- P_bv(x,y)
     // Query
 
+    // this model converter should be composed with a filter converter
+    // that gets rid of the new functions.
+    class bit_blast_model_converter : public model_converter {
+        ast_manager& m;
+        bv_util      m_bv;
+        func_decl_ref_vector m_old_funcs;
+        func_decl_ref_vector m_new_funcs;
+    public:
+        bit_blast_model_converter(ast_manager& m):
+            m(m),
+            m_bv(m),
+            m_old_funcs(m), 
+            m_new_funcs(m) {}
+
+        void insert(func_decl* old_f, func_decl* new_f) {
+            m_old_funcs.push_back(old_f);
+            m_new_funcs.push_back(new_f);
+        }
+
+        virtual model_converter * translate(ast_translation & translator) { 
+            return alloc(bit_blast_model_converter, m);
+        }
+
+        virtual void operator()(model_ref & model) {
+            for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
+                func_decl* p = m_new_funcs[i].get();
+                func_decl* q = m_old_funcs[i].get();
+                func_interp* f = model->get_func_interp(p);
+                expr_ref body(m);                
+                unsigned arity_p = p->get_arity();
+                unsigned arity_q = q->get_arity();
+                SASSERT(0 < arity_p);
+                model->register_decl(p, f);
+                func_interp* g = alloc(func_interp, m, arity_q);
+
+                if (f) {
+                    body = f->get_interp();
+                    SASSERT(!f->is_partial());
+                    SASSERT(body);                    
+                }
+                else {
+                    body = m.mk_false();  
+                }
+                unsigned idx = 0;
+                expr_ref arg(m), proj(m);
+                expr_safe_replace sub(m);
+                for (unsigned j = 0; j < arity_q; ++j) {
+                    sort* s = q->get_domain(j);
+                    arg = m.mk_var(j, s);
+                    if (m_bv.is_bv_sort(s)) {
+                        expr* args[1] = { arg };
+                        unsigned sz = m_bv.get_bv_size(s);
+                        for (unsigned k = 0; k < sz; ++k) {
+                            proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
+                            sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); 
+                        }
+                    }
+                    else {
+                        sub.insert(m.mk_var(idx++, s), arg);
+                    }
+                }
+                sub(body);                
+                g->set_else(body);
+                model->register_decl(q, g);
+            }                        
+        }        
+    };
 
     class expand_mkbv_cfg : public default_rewriter_cfg {
 
@@ -43,7 +111,8 @@ namespace datalog {
         ast_manager&         m;
         bv_util              m_util;
         expr_ref_vector      m_args, m_f_vars, m_g_vars;
-        func_decl_ref_vector m_pinned;
+        func_decl_ref_vector m_old_funcs;
+        func_decl_ref_vector m_new_funcs;
         obj_map<func_decl,func_decl*> m_pred2blast;
 
 
@@ -57,10 +126,14 @@ namespace datalog {
             m_args(m), 
             m_f_vars(m),
             m_g_vars(m),
-            m_pinned(m) 
+            m_old_funcs(m),
+            m_new_funcs(m)
         {}
 
         ~expand_mkbv_cfg() {}
+
+        func_decl_ref_vector const& old_funcs() const { return m_old_funcs; }
+        func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
         
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { 
             rule_manager& rm = m_context.get_rule_manager();
@@ -105,13 +178,18 @@ namespace datalog {
                     domain.push_back(m.get_sort(m_args[i].get()));
                 }
                 g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f);
-                m_pinned.push_back(g);
+                m_old_funcs.push_back(f);
+                m_new_funcs.push_back(g);
                 m_pred2blast.insert(f, g);
 
                 // Create rule f(mk_mkbv(args)) :- g(args)
 
                 fml = m.mk_implies(m.mk_app(g, m_g_vars.size(), m_g_vars.c_ptr()), m.mk_app(f, m_f_vars.size(), m_f_vars.c_ptr()));
-                rm.mk_rule(fml, m_rules, g->get_name());
+                proof_ref pr(m);
+                if (m_context.generate_proof_trace()) {
+                    pr = m.mk_asserted(fml); // or a def?
+                }
+                rm.mk_rule(fml, pr, m_rules, g->get_name());
             }
             result = m.mk_app(g, m_args.size(), m_args.c_ptr());
             result_pr = 0;
@@ -170,14 +248,11 @@ namespace datalog {
             m_blaster.updt_params(m_params);
         }
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-            // TODO mc, pc
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc) {
+            // TODO pc
             if (!m_context.get_params().bit_blast()) {
                 return 0;
             }
-            if (m_context.get_engine() != PDR_ENGINE) {
-                return 0;
-            }
             rule_manager& rm = m_context.get_rule_manager();
             unsigned sz = source.get_num_rules();
             expr_ref fml(m);            
@@ -185,9 +260,13 @@ namespace datalog {
             rule_set * result = alloc(rule_set, m_context);        
             for (unsigned i = 0; i < sz; ++i) {
                 rule * r = source.get_rule(i);
-                r->to_formula(fml);
+                r->to_formula(fml);                
                 if (blast(fml)) {
-                    rm.mk_rule(fml, m_rules, r->name()); 
+                    proof_ref pr(m);
+                    if (m_context.generate_proof_trace()) {
+                        pr = m.mk_asserted(fml); // loses original proof of r.
+                    }
+                    rm.mk_rule(fml, pr, m_rules, r->name()); 
                 }
                 else {
                     m_rules.push_back(r);
@@ -197,6 +276,18 @@ namespace datalog {
             for (unsigned i = 0; i < m_rules.size(); ++i) {
                 result->add_rule(m_rules.get(i));
             }
+
+            if (mc) {               
+                filter_model_converter* fmc = alloc(filter_model_converter, m);
+                bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m);
+                func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs();
+                func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs();
+                for (unsigned i = 0; i < old_funcs.size(); ++i) {
+                    fmc->insert(new_funcs[i]);
+                    bvmc->insert(old_funcs[i], new_funcs[i]);
+                }
+                mc = concat(mc.get(), concat(bvmc, fmc));
+            }
             
             return result;
         }
@@ -210,8 +301,8 @@ namespace datalog {
         dealloc(m_impl);
     }
 
-    rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        return (*m_impl)(source, mc, pc);
+    rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc) {
+        return (*m_impl)(source, mc);
     }        
 
 };
diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz_qe/dl_mk_bit_blast.h
index e16c2058b..3a6de75e3 100644
--- a/src/muz_qe/dl_mk_bit_blast.h
+++ b/src/muz_qe/dl_mk_bit_blast.h
@@ -44,7 +44,7 @@ namespace datalog {
         mk_bit_blast(context & ctx, unsigned priority = 35000);
         ~mk_bit_blast();
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp
index 222881bc4..de5388312 100644
--- a/src/muz_qe/dl_mk_coalesce.cpp
+++ b/src/muz_qe/dl_mk_coalesce.cpp
@@ -133,7 +133,7 @@ namespace datalog {
         tail.push_back(to_app(fml));
         is_neg.push_back(false);
         res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
-        if (m_pc) {
+        if (m_ctx.generate_proof_trace()) {
             src.to_formula(fml1);
             tgt->to_formula(fml2);
             res->to_formula(fml);
@@ -142,12 +142,13 @@ namespace datalog {
             sort* domain[3] = { ps, ps, m.mk_bool_sort() };
             func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps);  // TBD: ad-hoc proof rule
             expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml };
-            m_pc->insert(m.mk_app(merge, 3, args));
+            // ...m_pc->insert(m.mk_app(merge, 3, args));
 #else
             svector<std::pair<unsigned, unsigned> > pos;
             vector<expr_ref_vector> substs;
-            proof* p = m.mk_asserted(fml1);
-            m_pc->insert(m.mk_hyper_resolve(1, &p, fml, pos, substs));
+            proof* p = src.get_proof();
+            p = m.mk_hyper_resolve(1, &p, fml, pos, substs);
+            res->set_proof(m, p);
 #endif
         }
         tgt = res;
@@ -170,13 +171,7 @@ namespace datalog {
         return true;
     }    
         
-    rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        m_pc = 0;
-        ref<replace_proof_converter> rpc;
-        if (pc) {
-            rpc = alloc(replace_proof_converter, m);
-            m_pc = rpc.get();
-        }
+    rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc) {
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
         for (; it != end; ++it) {
@@ -195,9 +190,6 @@ namespace datalog {
                 rules->add_rule(r1.get());
             }
         }
-        if (pc) {
-            pc = concat(pc.get(), rpc.get());
-        }
         return rules;
     }
 
diff --git a/src/muz_qe/dl_mk_coalesce.h b/src/muz_qe/dl_mk_coalesce.h
index 4259d31fe..ab0b74479 100644
--- a/src/muz_qe/dl_mk_coalesce.h
+++ b/src/muz_qe/dl_mk_coalesce.h
@@ -37,7 +37,6 @@ namespace datalog {
         rule_manager&   rm;
         expr_ref_vector m_sub1, m_sub2;
         unsigned        m_idx;
-        replace_proof_converter* m_pc;
 
         void mk_pred(app_ref& pred, app* p1, app* p2);
 
@@ -53,7 +52,7 @@ namespace datalog {
          */
         mk_coalesce(context & ctx);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp
index 04d654120..915dd4306 100644
--- a/src/muz_qe/dl_mk_coi_filter.cpp
+++ b/src/muz_qe/dl_mk_coi_filter.cpp
@@ -35,8 +35,7 @@ namespace datalog {
 
     rule_set * mk_coi_filter::operator()(
         rule_set const & source,
-        model_converter_ref& mc,
-        proof_converter_ref& pc) 
+        model_converter_ref& mc) 
     {
         if (source.get_num_rules()==0) {
             return 0;
diff --git a/src/muz_qe/dl_mk_coi_filter.h b/src/muz_qe/dl_mk_coi_filter.h
index b8fb37964..2191048d3 100644
--- a/src/muz_qe/dl_mk_coi_filter.h
+++ b/src/muz_qe/dl_mk_coi_filter.h
@@ -40,8 +40,7 @@ namespace datalog {
 
 
         rule_set * operator()(rule_set const & source,
-                              model_converter_ref& mc,
-                              proof_converter_ref& pc);
+                              model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp
index b4683bdbe..af5b1d97a 100644
--- a/src/muz_qe/dl_mk_explanations.cpp
+++ b/src/muz_qe/dl_mk_explanations.cpp
@@ -708,8 +708,8 @@ namespace datalog {
     }
 
     rule * mk_explanations::get_e_rule(rule * r) {
-        var_counter ctr;
-        ctr.count_vars(m_manager, r);
+        rule_counter ctr;
+        ctr.count_rule_vars(m_manager, r);
         unsigned max_var;
         unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
         unsigned head_var = next_var++;
@@ -875,8 +875,8 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        SASSERT(!mc && !pc);
+    rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc) {
+        SASSERT(!mc);
         if(source.get_num_rules()==0) {
             return 0;
         }
diff --git a/src/muz_qe/dl_mk_explanations.h b/src/muz_qe/dl_mk_explanations.h
index 36fb1a3a1..40606f8df 100644
--- a/src/muz_qe/dl_mk_explanations.h
+++ b/src/muz_qe/dl_mk_explanations.h
@@ -82,7 +82,7 @@ namespace datalog {
             return get_union_decl(m_context);
         }
 
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
         static expr* get_explanation(relation_base const& r);
     };
diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp
index 35f7485d5..a3d5cc2ab 100644
--- a/src/muz_qe/dl_mk_extract_quantifiers.cpp
+++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp
@@ -168,7 +168,15 @@ namespace datalog {
             fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head());
             TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";);
             rule_ref_vector rules(rm);
-            rm.mk_rule(fml, rules, r.name());
+            proof_ref pr(m);
+            if (m_ctx.generate_proof_trace()) {
+                scoped_proof _scp(m);
+                expr_ref fml1(m);
+                r.to_formula(fml1);
+                pr = m.mk_rewrite(fml1, fml);
+                pr = m.mk_modus_ponens(r.get_proof(), pr);
+            }
+            rm.mk_rule(fml, pr, rules, r.name());
             for (unsigned i = 0; i < rules.size(); ++i) {
                 new_rules.add_rule(rules[i].get());
                 m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs));
@@ -347,7 +355,7 @@ namespace datalog {
         m_quantifiers.reset();
     }
     
-    rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+    rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc) {
         reset();
         rule_set::iterator it = source.begin(), end = source.end();
         for (; !m_has_quantifiers && it != end; ++it) {
diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h
index b32dbc32d..7d2f7b149 100644
--- a/src/muz_qe/dl_mk_extract_quantifiers.h
+++ b/src/muz_qe/dl_mk_extract_quantifiers.h
@@ -77,7 +77,7 @@ namespace datalog {
 
         void set_query(func_decl* q);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
         bool has_quantifiers() { return m_has_quantifiers; }
 
diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp
index 4f01a3651..46fde4bc2 100644
--- a/src/muz_qe/dl_mk_filter_rules.cpp
+++ b/src/muz_qe/dl_mk_filter_rules.cpp
@@ -90,6 +90,7 @@ namespace datalog {
             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);
             m_result->add_rule(filter_rule);
+            m_context.get_rule_manager().mk_rule_asserted_proof(*filter_rule);
         }
         else {
             dealloc(key);
@@ -135,12 +136,13 @@ namespace datalog {
             }
             new_is_negated.push_back(r->is_neg_tail(i));
         }
-        if(rule_modified) {
+        if (rule_modified) {
             remove_duplicate_tails(new_tail, new_is_negated);
             SASSERT(new_tail.size() == new_is_negated.size());
             rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr());
             new_rule->set_accounting_parent_object(m_context, m_current);
             m_result->add_rule(new_rule);
+            m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule);
             m_modified = true;
         }
         else {
@@ -148,7 +150,7 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+    rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc) {
         // TODO mc, pc
         m_tail2filter.reset();
         m_result           = alloc(rule_set, m_context);
diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h
index cd1d10997..daa72e36f 100644
--- a/src/muz_qe/dl_mk_filter_rules.h
+++ b/src/muz_qe/dl_mk_filter_rules.h
@@ -72,7 +72,7 @@ namespace datalog {
         /**
            \brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values.
         */
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
index d028c8751..a48b7b32f 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
@@ -35,7 +35,7 @@ namespace datalog {
     // -----------------------------------
 
     void mk_interp_tail_simplifier::rule_substitution::reset(rule * r) {
-        unsigned var_cnt = m_context.get_rule_manager().get_var_counter().get_max_var(*r)+1;
+        unsigned var_cnt = m_context.get_rule_manager().get_counter().get_max_rule_var(*r)+1;
         m_subst.reset();
         m_subst.reserve(1, var_cnt);
         m_rule = r;
@@ -541,8 +541,8 @@ namespace datalog {
 
         rule_ref pro_var_eq_result(m_context.get_rule_manager());
         if (propagate_variable_equivalences(res, pro_var_eq_result)) {
-            SASSERT(var_counter().get_max_var(*r.get())==0 || 
-                var_counter().get_max_var(*r.get()) > var_counter().get_max_var(*pro_var_eq_result.get()));
+            SASSERT(rule_counter().get_max_rule_var(*r.get())==0 || 
+                    rule_counter().get_max_rule_var(*r.get()) > rule_counter().get_max_rule_var(*pro_var_eq_result.get()));
             r = pro_var_eq_result;
             goto start;
         }
@@ -554,11 +554,13 @@ namespace datalog {
 
     bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) {
         bool modified = false;
+        rule_manager& rm = m_context.get_rule_manager();
         rule_set::iterator rit = orig.begin();
         rule_set::iterator rend = orig.end();
         for (; rit!=rend; ++rit) {
-            rule_ref new_rule(m_context.get_rule_manager());
+            rule_ref new_rule(rm);
             if (transform_rule(*rit, new_rule)) {
+                rm.mk_rule_rewrite_proof(**rit, *new_rule.get());
                 bool is_modified = *rit != new_rule;
                 modified |= is_modified;
                 tgt.add_rule(new_rule);
@@ -570,8 +572,7 @@ namespace datalog {
         return modified;
     }
 
-    rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc
+    rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc) {
         if (source.get_num_rules() == 0) {
             return 0;
         }
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h
index 5e4fd8fbc..4cb14914a 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.h
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h
@@ -93,7 +93,7 @@ namespace datalog {
         */
         bool transform_rule(rule * r, rule_ref& res);
 
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp
index f690346bc..18b152589 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz_qe/dl_mk_karr_invariants.cpp
@@ -145,7 +145,7 @@ namespace datalog {
     }
     
     bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) {
-        unsigned num_vars = rm.get_var_counter().get_max_var(r)+1;
+        unsigned num_vars = rm.get_counter().get_max_rule_var(r)+1;
         unsigned arity = r.get_decl()->get_arity();
         unsigned num_columns = arity + num_vars;        
         unsigned utsz = r.get_uninterpreted_tail_size();
@@ -310,7 +310,7 @@ namespace datalog {
         m_hb.reset();
         for (unsigned i = 0; i < src.size(); ++i) {
             vector<rational> v(src.A[i]);
-            v.append(src.b[i]);
+            v.push_back(src.b[i]);
             if (src.eq[i]) {
                 m_hb.add_eq(v, rational(0));
             }
@@ -420,6 +420,7 @@ namespace datalog {
             new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name());
         }
         rules.add_rule(new_rule);
+        rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening rule.
     }
 
     class mk_karr_invariants::add_invariant_model_converter : public model_converter {
@@ -519,7 +520,7 @@ namespace datalog {
         m_hb.set_cancel(true);
     }
     
-    rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+    rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc) {
         if (!m_ctx.get_params().karr()) {
             return 0;
         }
diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h
index 3b82578a4..7cd26d495 100644
--- a/src/muz_qe/dl_mk_karr_invariants.h
+++ b/src/muz_qe/dl_mk_karr_invariants.h
@@ -69,7 +69,7 @@ namespace datalog {
 
         virtual void cancel(); 
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
     };
 
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp
index 373a90969..990040ab8 100644
--- a/src/muz_qe/dl_mk_magic_sets.cpp
+++ b/src/muz_qe/dl_mk_magic_sets.cpp
@@ -317,8 +317,8 @@ namespace datalog {
         m_rules.push_back(r);
     }
 
-    rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        SASSERT(!mc && !pc);
+    rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc) {
+        SASSERT(!mc);
         unsigned init_rule_cnt = source.get_num_rules();
         {
             func_decl_set intentional;
diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h
index f98ad55a3..3f50e6713 100644
--- a/src/muz_qe/dl_mk_magic_sets.h
+++ b/src/muz_qe/dl_mk_magic_sets.h
@@ -121,7 +121,7 @@ namespace datalog {
          */
         mk_magic_sets(context & ctx, rule * goal_rule);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp
index 367a15743..b55f5294e 100644
--- a/src/muz_qe/dl_mk_partial_equiv.cpp
+++ b/src/muz_qe/dl_mk_partial_equiv.cpp
@@ -86,8 +86,8 @@ namespace datalog {
     }
 
 
-    rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc  
+    rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc) {
+        // TODO mc  
 
         if (source.get_num_rules() == 0) {
             return 0;
diff --git a/src/muz_qe/dl_mk_partial_equiv.h b/src/muz_qe/dl_mk_partial_equiv.h
index 8fef4aea9..c44d59e8c 100644
--- a/src/muz_qe/dl_mk_partial_equiv.h
+++ b/src/muz_qe/dl_mk_partial_equiv.h
@@ -35,7 +35,7 @@ namespace datalog {
             m(ctx.get_manager()),
             m_context(ctx) {}
 
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
     private:
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index 0919e2ff0..047ed768f 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -65,8 +65,8 @@ namespace datalog {
     // -----------------------------------
 
     bool rule_unifier::unify_rules(const rule& tgt, unsigned tgt_idx, const rule& src) {
-        var_counter& vc = m_rm.get_var_counter();
-        unsigned var_cnt = std::max(vc.get_max_var(tgt), vc.get_max_var(src))+1;
+        rule_counter& vc = m_rm.get_counter();
+        unsigned var_cnt = std::max(vc.get_max_rule_var(tgt), vc.get_max_rule_var(src))+1;
         m_subst.reset();
         m_subst.reserve(2, var_cnt);
         
@@ -181,10 +181,10 @@ namespace datalog {
         }
 
         if (m_unifier.apply(tgt, tail_index, src, res)) {
-            if (m_pc) {
+            if (m_context.generate_proof_trace()) {
                 expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true);
                 expr_ref_vector s2 = m_unifier.get_rule_subst(src, false);
-                datalog::resolve_rule(m_pc, tgt, src, tail_index, s1, s2, *res.get());
+                datalog::resolve_rule(tgt, src, tail_index, s1, s2, *res.get());
             }
             return true;        
         }
@@ -733,7 +733,7 @@ namespace datalog {
         }
 
         // initialize substitution.
-        var_counter& vc = m_rm.get_var_counter();
+        rule_counter& vc = m_rm.get_counter();
         unsigned max_var = 0;
         for (unsigned i = 0; i < sz; ++i) {
             rule* r = acc[i].get();
@@ -820,7 +820,7 @@ namespace datalog {
                     del_rule(r2, j);
                 }
 
-                max_var = std::max(max_var, vc.get_max_var(*r.get()));
+                max_var = std::max(max_var, vc.get_max_rule_var(*r.get()));
                 m_subst.reserve_vars(max_var+1);
 
             }
@@ -837,11 +837,10 @@ namespace datalog {
         return done_something;
     }
 
-    rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
+    rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc) {
 
         bool something_done = false;
         ref<horn_subsume_model_converter> hsmc;        
-        ref<replace_proof_converter> hpc;
 
         if (source.get_num_rules() == 0) {
             return 0;
@@ -858,11 +857,7 @@ namespace datalog {
         if (mc) {
             hsmc = alloc(horn_subsume_model_converter, m);
         }
-        if (pc) {
-            hpc = alloc(replace_proof_converter, m);
-        }
         m_mc = hsmc.get();
-        m_pc = hpc.get();
 
         scoped_ptr<rule_set> res = alloc(rule_set, m_context);
 
@@ -889,9 +884,6 @@ namespace datalog {
             if (mc) {
                 mc = concat(mc.get(), hsmc.get());
             }
-            if (pc) {
-                pc = concat(pc.get(), hpc.get());
-            }
         }
 
         return res.detach();
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index 6d5448cd6..a58b3b473 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -114,7 +114,6 @@ namespace datalog {
         ast_counter     m_tail_pred_ctr;
         rule_set        m_inlined_rules;
         horn_subsume_model_converter* m_mc;
-        replace_proof_converter* m_pc;
 
 
         //used in try_to_inline_rule and do_eager_inlining
@@ -188,7 +187,6 @@ namespace datalog {
             m_pinned(m_rm),
             m_inlined_rules(m_context),
             m_mc(0),
-            m_pc(0),
             m_unifier(ctx),
             m_head_index(m),
             m_tail_index(m),
@@ -198,7 +196,7 @@ namespace datalog {
         {}
         virtual ~mk_rule_inliner() { }
 
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp
index 42a5ba367..dfd0a4d81 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.cpp
+++ b/src/muz_qe/dl_mk_similarity_compressor.cpp
@@ -372,10 +372,10 @@ namespace datalog {
             new_negs.push_back(r->is_neg_tail(i));
         }
 
-        var_counter var_ctr;
-        var_ctr.count_vars(m_manager, r);
+        rule_counter ctr;
+        ctr.count_rule_vars(m_manager, r);
         unsigned max_var_idx, new_var_idx_base;
-        if(var_ctr.get_max_positive(max_var_idx)) {
+        if(ctr.get_max_positive(max_var_idx)) {
             new_var_idx_base = max_var_idx+1;
         }
         else {
@@ -500,8 +500,8 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc
+    rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
+        // TODO mc
         m_modified = false;
         unsigned init_rule_cnt = source.get_num_rules();
         SASSERT(m_rules.empty());
diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz_qe/dl_mk_similarity_compressor.h
index ad4a5e246..d1ded01e7 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.h
+++ b/src/muz_qe/dl_mk_similarity_compressor.h
@@ -69,7 +69,7 @@ namespace datalog {
     public:
         mk_similarity_compressor(context & ctx, unsigned threshold_count);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp
index 363a4f0f7..f19e34fec 100644
--- a/src/muz_qe/dl_mk_simple_joins.cpp
+++ b/src/muz_qe/dl_mk_simple_joins.cpp
@@ -310,8 +310,8 @@ namespace datalog {
         }
 
         void register_rule(rule * r) {
-            var_counter counter;
-            counter.count_vars(m, r, 1);
+            rule_counter counter;
+            counter.count_rule_vars(m, r, 1);
 
             ptr_vector<app> & rule_content = 
                 m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;
@@ -706,19 +706,20 @@ namespace datalog {
                     negs.c_ptr());
 
                 new_rule->set_accounting_parent_object(m_context, orig_r);
-
+                m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule);
                 result->add_rule(new_rule);
             }
-            while(!m_introduced_rules.empty()) {
+            while (!m_introduced_rules.empty()) {
                 result->add_rule(m_introduced_rules.back());
+                m_context.get_rule_manager().mk_rule_asserted_proof(*m_introduced_rules.back());
                 m_introduced_rules.pop_back();
             }
             return result;
         }
     };
 
-    rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc
+    rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc) {
+        // TODO mc
         rule_set rs_aux_copy(m_context);
         rs_aux_copy.add_rules(source);
         if(!rs_aux_copy.is_closed()) {
diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz_qe/dl_mk_simple_joins.h
index 5431c4117..df8d3f55c 100644
--- a/src/muz_qe/dl_mk_simple_joins.h
+++ b/src/muz_qe/dl_mk_simple_joins.h
@@ -53,7 +53,7 @@ namespace datalog {
     public:
         mk_simple_joins(context & ctx);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 84b732280..0adab78ce 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -164,10 +164,8 @@ namespace datalog {
                 TRACE("dl", tout << "does not have fact\n" << mk_pp(fact, m) << "\n";);
                 return false;
             }
-            expr_ref fml(m);
             proof_ref new_p(m);
-            r->to_formula(fml);
-            new_p = m.mk_asserted(fml);
+            new_p = r->get_proof();
             m_pinned_exprs.push_back(new_p);
             m_todo.pop_back();
             m_new_proof.insert(p, new_p);
@@ -784,6 +782,9 @@ namespace datalog {
             rm.fix_unbound_vars(new_rule, false);
 
             TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
+            if (m_ctx.generate_proof_trace()) {
+                rm.mk_rule_asserted_proof(*new_rule.get());
+            }
         }
         else {
             new_rule = &r;
@@ -801,7 +802,7 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {        
+    rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc) {        
         for (unsigned i = 0; i < src.get_num_rules(); ++i) {
             if (src.get_rule(i)->has_quantifiers()) {
                 return 0;
@@ -809,8 +810,8 @@ namespace datalog {
         }
         ref<slice_proof_converter> spc;
         ref<slice_model_converter> smc;
-        if (pc) {
-            spc = alloc(slice_proof_converter, m_ctx);
+        if (m_ctx.generate_proof_trace()) {
+            spc = alloc(slice_proof_converter, m_ctx);        
         }
         if (mc) {
             smc = alloc(slice_model_converter, *this, m);
@@ -834,7 +835,7 @@ namespace datalog {
                 m_mc->add_sliceable(it->m_key, it->m_value);
             }
         }
-        pc = concat(pc.get(), spc.get());
+        m_ctx.add_proof_converter(spc.get());
         mc = concat(mc.get(), smc.get());
         return result;
     }    
diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h
index 26a8175f2..4290ee4b9 100644
--- a/src/muz_qe/dl_mk_slice.h
+++ b/src/muz_qe/dl_mk_slice.h
@@ -102,7 +102,7 @@ namespace datalog {
 
         virtual ~mk_slice() { }
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
 
         func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }
 
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp
index 19c28c036..2f0d56475 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.cpp
+++ b/src/muz_qe/dl_mk_subsumption_checker.cpp
@@ -166,7 +166,8 @@ namespace datalog {
         res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
         res->set_accounting_parent_object(m_context, r);
         m_context.get_rule_manager().fix_unbound_vars(res, true);
-        
+        m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());
+
         return true;
     }
 
@@ -208,10 +209,10 @@ namespace datalog {
                     continue;
                 }
                 rule * defining_rule;
-                TRUSTME(m_total_relation_defining_rules.find(head_pred, defining_rule));
-                if(defining_rule) {
+                VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
+                if (defining_rule) {
                     rule_ref totality_rule(m_context.get_rule_manager());
-                    TRUSTME(transform_rule(defining_rule, subs_index, totality_rule));
+                    VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
                     if(defining_rule!=totality_rule) {
                         modified = true;
                     }
@@ -331,8 +332,8 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc
+    rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc) {
+        // TODO mc
 
         m_have_new_total_rule = false;
         collect_ground_unconditional_rule_heads(source);
diff --git a/src/muz_qe/dl_mk_subsumption_checker.h b/src/muz_qe/dl_mk_subsumption_checker.h
index ce33e7574..a95f08c5d 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.h
+++ b/src/muz_qe/dl_mk_subsumption_checker.h
@@ -84,7 +84,7 @@ namespace datalog {
             reset_dealloc_values(m_ground_unconditional_rule_heads);
         }
 
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp
index e3db82759..54b6f4ebe 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.cpp
+++ b/src/muz_qe/dl_mk_unbound_compressor.cpp
@@ -238,6 +238,7 @@ namespace datalog {
 
         unsigned new_rule_index = m_rules.size();
         m_rules.push_back(new_rule);
+        m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get());
         m_head_occurrence_ctr.inc(new_rule->get_head()->get_decl());
 
 
@@ -333,8 +334,8 @@ namespace datalog {
         }
     }
 
-    rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        // TODO mc, pc
+    rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
+        // TODO mc
         m_modified = false;
 
         m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h
index 0e13bad75..256be180d 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.h
+++ b/src/muz_qe/dl_mk_unbound_compressor.h
@@ -82,7 +82,7 @@ namespace datalog {
     public:
         mk_unbound_compressor(context & ctx);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_mk_unfold.cpp b/src/muz_qe/dl_mk_unfold.cpp
index d26a0a290..7af82110a 100644
--- a/src/muz_qe/dl_mk_unfold.cpp
+++ b/src/muz_qe/dl_mk_unfold.cpp
@@ -42,29 +42,20 @@ namespace datalog {
                 if (m_unify.unify_rules(r, tail_idx, r2) &&
                     m_unify.apply(r, tail_idx, r2, new_rule)) {
                     expr_ref_vector s1 = m_unify.get_rule_subst(r, true);
-                    expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);
-                    resolve_rule(m_pc, r, r2, tail_idx, s1, s2, *new_rule.get());
+                    expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);                    
+                    resolve_rule(r, r2, tail_idx, s1, s2, *new_rule.get());
                     expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst);
                 }
             }
         }
     }
         
-    rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
-        m_pc = 0;
-        ref<replace_proof_converter> rpc;
-        if (pc) {
-            rpc = alloc(replace_proof_converter, m);
-            m_pc = rpc.get();
-        }
+    rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc) {
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::iterator it = source.begin(), end = source.end();
         for (; it != end; ++it) {
             expand_tail(**it, 0, source, *rules);
         }
-        if (pc) {
-            pc = concat(pc.get(), rpc.get());
-        }
         return rules;
     }
 
diff --git a/src/muz_qe/dl_mk_unfold.h b/src/muz_qe/dl_mk_unfold.h
index 3d20686a7..90aefa86e 100644
--- a/src/muz_qe/dl_mk_unfold.h
+++ b/src/muz_qe/dl_mk_unfold.h
@@ -35,7 +35,6 @@ namespace datalog {
         ast_manager&    m;
         rule_manager&   rm;
         rule_unifier    m_unify;
-        replace_proof_converter* m_pc;
 
         void expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst);
 
@@ -45,7 +44,7 @@ namespace datalog {
          */
         mk_unfold(context & ctx);
         
-        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc);
     };
 
 };
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 0b626d72e..a13229e7a 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -42,13 +42,13 @@ Revision History:
 #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_refs(ctx.get_manager()) {}
+          m_ctx(ctx) {}
 
     bool rule_manager::is_predicate(func_decl * f) const {
         return m_ctx.is_predicate(f);
@@ -89,111 +89,32 @@ namespace datalog {
         }
     };
 
-    void rule_manager::remove_labels(expr_ref& fml) {
+    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);
+        if (pr && fml != tmp) {
+            
+            pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
+        }
         fml = tmp;
     }
 
 
-    void rule_manager::mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name) {              
+    void rule_manager::mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) {              
+        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
+        proof_ref pr(p, m);
         expr_ref fml1(m);
-        m_memoize_disj.reset();
-        m_refs.reset();
         bind_variables(fml, true, fml1);
-        unsigned num_rules = rules.size();
-        mk_rule_core(fml1, rules, name);
-        if (m_pc) {
-            // big-step proof
-            // m.mk_cnf_star(fml1, conj, 0, 0);
-            // 
+        if (fml1 != fml && pr) {
+            pr = m.mk_asserted(fml1);
         }
+        remove_labels(fml1, pr);        
+        mk_rule_core_new(fml1, pr, rules, name);
     }
 
-    // 
-    // Hoist quantifier from rule (universal) or query (existential)
-    // 
-    unsigned rule_manager::hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {   
-
-        unsigned index = var_counter().get_next_var(fml);
-        while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
-            quantifier* q = to_quantifier(fml);
-            index += q->get_num_decls();
-            if (names) {
-                names->append(q->get_num_decls(), q->get_decl_names());
-            }
-            fml = q->get_expr();
-        }
-        if (!has_quantifiers(fml)) {
-            return index;
-        }
-        app_ref_vector vars(m);
-        quantifier_hoister qh(m);
-        qh.pull_quantifier(is_forall, fml, vars);
-        if (vars.empty()) {
-            return index;
-        }
-        // replace vars by de-bruijn indices
-        expr_safe_replace rep(m);
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            app* v = vars[i].get();
-            if (names) {
-                names->push_back(v->get_decl()->get_name());
-            }                
-            rep.insert(v, m.mk_var(index++,m.get_sort(v)));
-        }
-        rep(fml);
-        return index;
-    }
-
-    void rule_manager::mk_rule_core(expr* _fml, rule_ref_vector& rules, symbol const& name) {
-        app_ref_vector body(m);
-        app_ref head(m);
-        expr_ref e(m), fml(_fml, m);
-        svector<bool> is_negated;
-        TRACE("dl_rule", tout << mk_pp(fml, m) << "\n";);
-        unsigned index = hoist_quantifier(true, fml, 0); 
-        check_app(fml);
-        head = to_app(fml);
-        
-        while (m.is_implies(head)) {
-            e = head->get_arg(0);
-            th_rewriter th_rwr(m);
-            th_rwr(e);
-            body.push_back(ensure_app(e));
-            e = to_app(head)->get_arg(1);
-            check_app(e);
-            head = to_app(e.get());
-        }
-        symbol head_name = (name == symbol::null)?head->get_decl()->get_name():name;
-        flatten_body(body);
-        if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
-            app* _or = to_app(body[0].get());
-            for (unsigned i = 0; i < _or->get_num_args(); ++i) {
-                e = m.mk_implies(_or->get_arg(i), head);
-                mk_rule_core(e, rules, head_name);
-            } 
-            return;
-        }
-
-        eliminate_disjunctions(body, rules, head_name);
-        eliminate_quantifier_body(body, rules, head_name);
-        hoist_compound(index, head, body);
-        unsigned sz = body.size();
-        for (unsigned i = 0; i < sz; ++i) {
-            app_ref b(body[i].get(), m);
-            hoist_compound(index, b, body);
-            body[i] = b;
-        }
-        TRACE("dl_rule",
-              tout << mk_pp(head, m) << " :- ";
-              for (unsigned i = 0; i < body.size(); ++i) {
-                  tout << mk_pp(body[i].get(), m) << " ";
-              }
-              tout << "\n";);
-
+    void rule_manager::mk_negations(app_ref_vector& body, svector<bool>& is_negated) {
         for (unsigned i = 0; i < body.size(); ++i) {
             expr* e = body[i].get(), *e1;
             if (m.is_not(e, e1) && is_predicate(e1)) {
@@ -204,23 +125,105 @@ namespace datalog {
             else {
                 is_negated.push_back(false);
             }
-        }
-        check_valid_rule(head, body.size(), body.c_ptr());
+        }        
+    }
 
-        rules.push_back(mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name));
-        
-        if (m_ctx.fix_unbound_vars()) {
-            unsigned rule_cnt = rules.size();
-            for (unsigned i=0; i<rule_cnt; ++i) {
-                rule_ref r(rules[i].get(), *this);
-                fix_unbound_vars(r, true);
-                if (r.get()!=rules[i].get()) {
-                    rules[i] = r;
-                }
-            }
+    void rule_manager::mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& 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]);
+        }
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name);
         }
     }
 
+    void rule_manager::mk_rule_core2(expr* fml, proof* p, rule_ref_vector& 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);
+        TRACE("dl_rule",
+              tout << mk_pp(head, m) << " :- ";
+              for (unsigned i = 0; i < body.size(); ++i) {
+                  tout << mk_pp(body[i].get(), m) << " ";
+              }
+              tout << "\n";);
+
+
+        mk_negations(body, is_negated);
+        check_valid_rule(head, body.size(), body.c_ptr());
+
+        rule_ref r(*this);
+        r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
+
+        expr_ref fml1(m);
+        if (p) {
+            r->to_formula(fml1);
+            if (fml1 == fml) {
+                // no-op.
+            }
+            else if (is_quantifier(fml1)) {
+                p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml)));
+            }            
+            else {
+                p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1));
+            }
+        }
+
+        if (m_ctx.fix_unbound_vars()) {            
+            fix_unbound_vars(r, true);
+        }
+
+        if (p) {
+            expr_ref fml2(m);
+            r->to_formula(fml2);
+            if (fml1 != fml2) {
+                p = m.mk_modus_ponens(p, m.mk_rewrite(fml1, fml2));
+            }
+            r->set_proof(m, p);
+        }
+        rules.push_back(r);        
+    }
+
+    unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) {
+        expr* e1, *e2;
+        unsigned index = m_counter.get_next_var(fml);
+        if (::is_forall(fml)) {
+            index += to_quantifier(fml)->get_num_decls();
+            fml = to_quantifier(fml)->get_expr();
+        }
+        if (m.is_implies(fml, e1, e2)) {
+            expr_ref_vector es(m);
+            head = ensure_app(e2);
+            datalog::flatten_and(e1, es);
+            for (unsigned i = 0; i < es.size(); ++i) {
+                body.push_back(ensure_app(es[i].get()));
+            }
+        } 
+        else {
+            head = ensure_app(fml);
+        }
+        return index;
+    }
+
+    void rule_manager::hoist_compound_predicates(unsigned index, app_ref& head, app_ref_vector& body) {
+        unsigned sz = body.size();
+        hoist_compound(index, head, body);
+        for (unsigned i = 0; i < sz; ++i) {
+            app_ref b(body[i].get(), m);
+            hoist_compound(index, b, body);
+            body[i] = b;
+        }
+    }
+
+
     void rule_manager::mk_query(expr* query, func_decl_ref& qpred, rule_ref_vector& query_rules, rule_ref& query_rule) {
         ptr_vector<sort> vars;
         svector<symbol> names;
@@ -230,7 +233,8 @@ namespace datalog {
         // Add implicit variables.
         // Remove existential prefix.
         bind_variables(query, false, q);
-        hoist_quantifier(false, q, &names);
+        quantifier_hoister qh(m);
+        qh.pull_quantifier(false, q, 0, &names);
         // retrieve free variables.
         get_free_vars(q, vars);
         if (vars.contains(static_cast<sort*>(0))) {
@@ -288,7 +292,12 @@ namespace datalog {
             rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl);
         }
 
-        mk_rule(rule_expr, query_rules);
+        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
+        proof_ref pr(m);
+        if (m_ctx.generate_proof_trace()) {
+            pr = m.mk_asserted(rule_expr);
+        }
+        mk_rule(rule_expr, pr, query_rules);
         SASSERT(query_rules.size() >= 1);
         query_rule = query_rules.back();
     }
@@ -368,73 +377,6 @@ namespace datalog {
         return false;
     }
 
-    void rule_manager::eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
-
-        app* b = body.get(); 
-        expr* e1;
-        bool negate_args = false;
-        bool is_disj = false;
-        unsigned num_disj = 0;
-        expr* const* disjs = 0;
-        if (!contains_predicate(b)) {
-            return;
-        }
-        TRACE("dl_rule", tout << mk_ismt2_pp(b, m) << "\n";);
-        if (m.is_or(b)) {
-            is_disj = true;
-            negate_args = false;
-            num_disj = b->get_num_args();
-            disjs = b->get_args();
-        }
-        if (m.is_not(b, e1) && m.is_and(e1)) {
-            is_disj = true;
-            negate_args = true;
-            num_disj = to_app(e1)->get_num_args();
-            disjs = to_app(e1)->get_args();
-        }
-        if (is_disj) {
-            ptr_vector<sort> sorts0, sorts1;
-            get_free_vars(b, sorts0);
-            expr_ref_vector args(m);
-            for (unsigned i = 0; i < sorts0.size(); ++i) {
-                if (sorts0[i]) {
-                    args.push_back(m.mk_var(i,sorts0[i]));
-                    sorts1.push_back(sorts0[i]);
-                }
-            }
-            app* old_head = 0;
-            if (m_memoize_disj.find(b, old_head)) {
-                body = old_head;
-            }
-            else {
-                app_ref head(m);
-                func_decl_ref f(m);
-                f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
-                m_ctx.register_predicate(f);
-                head = m.mk_app(f, args.size(), args.c_ptr());
-                
-                for (unsigned i = 0; i < num_disj; ++i) {
-                    expr_ref fml(m);
-                    expr* e = disjs[i];
-                    if (negate_args) e = m.mk_not(e);
-                    fml = m.mk_implies(e,head);
-                    mk_rule_core(fml, rules, name);
-                }
-                m_memoize_disj.insert(b, head);
-                m_refs.push_back(b);
-                m_refs.push_back(head);
-                // update the body to be the newly introduced head relation
-                body = head;
-            }
-        }
-    }
-
-    void rule_manager::eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
-        for (unsigned i = 0; i < body.size(); ++i) {
-            app_ref_vector::element_ref t = body[i];
-            eliminate_disjunctions(t, rules, name);
-        }
-    }
 
     bool rule_manager::is_forall(ast_manager& m, expr* e, quantifier*& q) {
         expr* e1, *e2;
@@ -453,40 +395,6 @@ namespace datalog {
         return false;
     }
 
-    void rule_manager::eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
-        quantifier* q;
-        if (is_forall(m, body.get(), q) && contains_predicate(q)) {
-            expr* e = q->get_expr();
-            if (!is_predicate(e)) {
-                ptr_vector<sort> sorts0, sorts1;
-                get_free_vars(e, sorts0);
-                expr_ref_vector args(m);
-                for (unsigned i = 0; i < sorts0.size(); ++i) {
-                    if (sorts0[i]) {
-                        args.push_back(m.mk_var(i,sorts0[i]));
-                        sorts1.push_back(sorts0[i]);
-                    }
-                }
-                app_ref head(m), fml(m);
-                func_decl_ref f(m);
-                f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
-                m_ctx.register_predicate(f);
-                head = m.mk_app(f, args.size(), args.c_ptr());
-                fml = m.mk_implies(e, head);
-                mk_rule_core(fml, rules, name);
-                // update the body to be the newly introduced head relation
-                body = m.mk_eq(m.mk_true(), m.update_quantifier(q, head));                
-            }
-        }
-    }
-
-    void rule_manager::eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
-        for (unsigned i = 0; i < body.size(); ++i) {
-            app_ref_vector::element_ref t = body[i];
-            eliminate_quantifier_body(t, rules, name);
-        }
-    }
-
 
     app_ref rule_manager::ensure_app(expr* e) {
         SASSERT(m.is_bool(e));
@@ -514,6 +422,7 @@ namespace datalog {
         r->m_head       = head;
         r->m_name       = name;
         r->m_tail_size  = n;
+        r->m_proof      = 0;
         m.inc_ref(r->m_head);
 
         app * * uninterp_tail = r->m_tail; //grows upwards
@@ -571,6 +480,11 @@ namespace datalog {
         if (normalize) {
             r->norm_vars(*this);
         }
+        DEBUG_CODE(ptr_vector<sort> sorts; 
+                   ::get_free_vars(head, sorts);
+                   for (unsigned i = 0; i < n; ++i) {
+                       ::get_free_vars(tail[i], sorts);
+                   });
         return r;
     }
 
@@ -710,7 +624,7 @@ namespace datalog {
         bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
 
         unsigned q_var_cnt = unbound_vars.num_elems();
-        unsigned max_var = m_var_counter.get_max_var(*r);
+        unsigned max_var = m_counter.get_max_rule_var(*r);
 
         expr_ref_vector subst(m);
 
@@ -792,6 +706,27 @@ namespace datalog {
         r->set_accounting_parent_object(m_ctx, old_r);
     }
 
+    void rule_manager::mk_rule_rewrite_proof(rule& old_rule, rule& new_rule) {
+        if (&old_rule != &new_rule &&
+            !new_rule.get_proof() &&
+            old_rule.get_proof()) {
+            expr_ref fml(m);
+            new_rule.to_formula(fml);
+            scoped_proof _sc(m);
+            proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml);
+            new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p)); 
+        }
+    }
+
+    void rule_manager::mk_rule_asserted_proof(rule& r) {
+        if (m_ctx.generate_proof_trace()) {
+            scoped_proof _scp(m);
+            expr_ref fml(m);
+            r.to_formula(fml);
+            r.set_proof(m, m.mk_asserted(fml));
+        }
+    }
+
     void rule_manager::substitute(rule_ref& r, unsigned sz, expr*const* es) {
         expr_ref tmp(m);
         app_ref  new_head(m);
@@ -850,10 +785,23 @@ namespace datalog {
         for (unsigned i = 0; i < n; i++) {
             m.dec_ref(get_tail(i));
         }
+        if (m_proof) {
+            m.dec_ref(m_proof);
+        }
         this->~rule();
         m.get_allocator().deallocate(get_obj_size(n), this);
     }
 
+    void rule::set_proof(ast_manager& m, proof* p) { 
+        if (p) {
+            m.inc_ref(p); 
+        }
+        if (m_proof) {
+            m.dec_ref(m_proof); 
+        }
+        m_proof = p; 
+    }
+
     bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
         unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size();
         for (unsigned i = 0; i < len; i++) {
@@ -1031,6 +979,9 @@ namespace datalog {
             out << '}';
         }
         out << '\n';
+        if (m_proof) {
+            out << mk_pp(m_proof, m) << '\n';
+        }
     }
 
     void rule::to_formula(expr_ref& fml) const {
@@ -1120,3 +1071,4 @@ namespace datalog {
 
 
 };
+
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index ebd93d090..3f535125f 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -46,38 +46,25 @@ namespace datalog {
     */
     class rule_manager
     {
-        ast_manager&        m;
-        context&            m_ctx;
-        var_counter         m_var_counter;
-        obj_map<expr, app*> m_memoize_disj;
-        expr_ref_vector     m_refs;
-        model_converter_ref m_mc;
-        proof_converter_ref m_pc;
+        ast_manager&         m;
+        context&             m_ctx;
+        rule_counter         m_counter;
 
         // only the context can create a rule_manager
         friend class context;
 
         explicit rule_manager(context& ctx);
 
-        void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
-        void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
-
         /**
            \brief Move functions from predicate tails into the interpreted tail by introducing new variables.
         */
+        void hoist_compound_predicates(unsigned num_bound, app_ref& head, app_ref_vector& body);
+
         void hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body);
 
         void flatten_body(app_ref_vector& body);
 
-        void remove_labels(expr_ref& fml);
-
-        void eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
-
-        void eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);        
-
-        void eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
-
-        void eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);
+        void remove_labels(expr_ref& fml, proof_ref& pr);
 
         app_ref ensure_app(expr* e);
 
@@ -89,7 +76,15 @@ namespace datalog {
 
         void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name);
 
-        unsigned hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
+        void mk_negations(app_ref_vector& body, svector<bool>& is_negated);
+
+        void mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
+
+        void mk_rule_core2(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
+
+        static expr_ref mk_implies(app_ref_vector const& body, expr* head);
+
+        unsigned extract_horn(expr* fml, app_ref_vector& body, app_ref& head);
 
         /**
            \brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
@@ -109,7 +104,7 @@ namespace datalog {
            The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))
            
         */
-        void mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name = symbol::null);
+        void mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name = symbol::null);
 
         /**
            \brief Create a Datalog query from an expression.
@@ -139,7 +134,15 @@ namespace datalog {
         /** make sure there are not non-quantified variables that occur only in interpreted predicates */
         void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
 
+        /**
+           \brief add proof that new rule is obtained by rewriting old rule.
+         */
+        void mk_rule_rewrite_proof(rule& old_rule, rule& new_rule);
 
+        /**
+           \brief tag rule as asserted.
+         */
+        void mk_rule_asserted_proof(rule& r);
 
         /**
            \brief apply substitution to variables of rule.
@@ -170,7 +173,7 @@ namespace datalog {
 
         static bool is_forall(ast_manager& m, expr* e, quantifier*& q);
 
-        var_counter& get_var_counter() { return m_var_counter; }
+        rule_counter& get_counter() { return m_counter; }
 
     };
 
@@ -178,6 +181,7 @@ namespace datalog {
         friend class rule_manager;
 
         app *    m_head;
+        proof*   m_proof;
         unsigned m_tail_size:20;
         // unsigned m_reserve:12;
         unsigned m_ref_cnt;
@@ -209,6 +213,10 @@ namespace datalog {
         void get_used_vars(used_vars& uv) const;
         
     public:
+
+        proof * get_proof() const { return m_proof; }
+
+        void set_proof(ast_manager& m, proof* p);
         
         app * get_head() const { return m_head; }
 
diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp
index a246d9d61..5ecbf2b45 100644
--- a/src/muz_qe/dl_rule_transformer.cpp
+++ b/src/muz_qe/dl_rule_transformer.cpp
@@ -73,7 +73,7 @@ namespace datalog {
         m_dirty=true;
     }
 
-    bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc) {
+    bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc) {
         ensure_ordered();
 
         bool modified = false;
@@ -87,7 +87,7 @@ namespace datalog {
         for(; it!=end && !m_cancel; ++it) {
             plugin & p = **it;
 
-            rule_set * new_rules = p(rules, mc, pc);
+            rule_set * new_rules = p(rules, mc);
             if (!new_rules) {
                 continue;
             }
diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h
index cf1a9be75..3b2140caf 100644
--- a/src/muz_qe/dl_rule_transformer.h
+++ b/src/muz_qe/dl_rule_transformer.h
@@ -24,7 +24,6 @@ Revision History:
 #include"dl_rule.h"
 #include"dl_rule_set.h"
 #include"model_converter.h"
-#include"proof_converter.h"
 
 namespace datalog {
 
@@ -69,7 +68,7 @@ namespace datalog {
            \brief Transform the rule set using the registered transformation plugins. If the rule 
            set has changed, return true; otherwise return false.
         */
-        bool operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc);
+        bool operator()(rule_set & rules, model_converter_ref& mc);
     };
     
     class rule_transformer::plugin {
@@ -106,8 +105,7 @@ namespace datalog {
            The caller takes ownership of the returned \c rule_set object.
         */
         virtual rule_set * operator()(rule_set const & source,
-                                      model_converter_ref& mc,
-                                      proof_converter_ref& pc) = 0;
+                                      model_converter_ref& mc) = 0;
 
         virtual void cancel() { m_cancel = true; }
 
diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp
index 3b5ca7658..74c16a6ea 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz_qe/dl_util.cpp
@@ -431,6 +431,29 @@ namespace datalog {
         }
     }
 
+<<<<<<< HEAD
+=======
+    
+    void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
+        count_vars(m, r->get_head(), 1);
+        unsigned n = r->get_tail_size();
+        for (unsigned i = 0; i < n; i++) {
+            count_vars(m, r->get_tail(i), coef);
+        }
+    }
+
+    unsigned rule_counter::get_max_rule_var(const rule & r) {
+        m_todo.push_back(r.get_head());
+        m_scopes.push_back(0);
+        unsigned n = r.get_tail_size();
+        bool has_var = false;
+        for (unsigned i = 0; i < n; i++) {
+            m_todo.push_back(r.get_tail(i));
+            m_scopes.push_back(0);
+        }
+        return get_max_var(has_var);
+    }
+>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
 
     void del_rule(horn_subsume_model_converter* mc, rule& r) {
         if (mc) {
@@ -492,6 +515,44 @@ namespace datalog {
         pc->insert(pr);
     }
 
+    void resolve_rule(rule const& r1, rule const& r2, unsigned idx, 
+                      expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
+        if (!r1.get_proof()) {
+            return;
+        }
+        SASSERT(r2.get_proof());
+        ast_manager& m = s1.get_manager();
+        expr_ref fml(m);
+        res.to_formula(fml);
+        vector<expr_ref_vector> substs;
+        svector<std::pair<unsigned, unsigned> > positions;
+        substs.push_back(s1);
+        substs.push_back(s2);
+
+        scoped_proof _sc(m);
+        proof_ref pr(m);
+        proof_ref_vector premises(m);
+        premises.push_back(r1.get_proof());
+        premises.push_back(r2.get_proof());
+        positions.push_back(std::make_pair(idx+1, 0));
+
+        TRACE("dl", 
+              tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
+              for (unsigned i = 0; i < s1.size(); ++i) {
+                  tout << mk_pp(s1[i], m) << " ";
+              }
+              tout << "\n";
+              tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
+              for (unsigned i = 0; i < s2.size(); ++i) {
+                  tout << mk_pp(s2[i], m) << " ";
+              }
+              tout << "\n";
+              ); 
+
+        pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
+        res.set_proof(m, pr);
+    }
+
     class skip_model_converter : public model_converter {
     public:
         skip_model_converter() {}
@@ -519,10 +580,6 @@ namespace datalog {
     proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); }
 
 
-    unsigned get_max_var(const rule & r, ast_manager & m) {
-        var_counter ctr;
-        return ctr.get_max_var(r);
-    }
 
     void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt) {
         SASSERT(tgt.empty());
diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h
index 4314b87f3..3d3c3ea54 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -27,6 +27,7 @@ Revision History:
 #include"replace_proof_converter.h"
 #include"substitution.h"
 #include"fixedpoint_params.hpp"
+#include"ast_counter.h"
 
 namespace datalog {
 
@@ -411,21 +412,26 @@ namespace datalog {
     }
 
 
+    class rule_counter : public var_counter {        
+    public:
+        rule_counter(bool stay_non_negative = true): var_counter(stay_non_negative) {}
+        void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
+        unsigned get_max_rule_var(const rule& r);
+    };
+
     void del_rule(horn_subsume_model_converter* mc, rule& r);
 
     void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res);
 
+    void resolve_rule(rule const& r1, rule const& r2, unsigned idx, 
+                      expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res);
+
     model_converter* mk_skip_model_converter();
 
     proof_converter* mk_skip_proof_converter();
 
 
-    /**
-       Return maximal variable number, or zero is there isn't any
-    */
-    // unsigned get_max_var(const rule & r, ast_manager & m);
-
     void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt);
 
     /**
diff --git a/src/muz_qe/equiv_proof_converter.cpp b/src/muz_qe/equiv_proof_converter.cpp
index 53db01900..98ea88044 100644
--- a/src/muz_qe/equiv_proof_converter.cpp
+++ b/src/muz_qe/equiv_proof_converter.cpp
@@ -22,12 +22,14 @@ Revision History:
 #include "dl_util.h"
 
 void equiv_proof_converter::insert(expr* fml1, expr* fml2) {
-    datalog::scoped_proof _sp(m);
-    proof_ref p1(m), p2(m), p3(m);
-    p1 = m.mk_asserted(fml1);
-    p2 = m.mk_rewrite(fml1, fml2);
-    p3 = m.mk_modus_ponens(p1, p2);
-    TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
-    SASSERT(m.has_fact(p3));
-    m_replace.insert(p3);
+    if (fml1 != fml2) {
+        datalog::scoped_proof _sp(m);
+        proof_ref p1(m), p2(m), p3(m);
+        p1 = m.mk_asserted(fml1);
+        p2 = m.mk_rewrite(fml1, fml2);
+        p3 = m.mk_modus_ponens(p1, p2);
+        TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
+        SASSERT(m.has_fact(p3));
+        m_replace.insert(p3);
+    }
 }
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 1b1f85988..98c21288e 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -113,8 +113,8 @@ class horn_tactic : public tactic {
                     todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
                 }
                 else if (m.is_ite(a)) {
-                    todo.append(to_app(a)->get_arg(1));
-                    todo.append(to_app(a)->get_arg(2));
+                    todo.push_back(to_app(a)->get_arg(1));
+                    todo.push_back(to_app(a)->get_arg(2));
                 }
                 else if (is_predicate(a)) {
                     register_predicate(a);
@@ -270,21 +270,16 @@ class horn_tactic : public tactic {
                     proof_converter_ref & pc) {
 
             expr_ref fml(m);            
-            bool produce_models = g->models_enabled();
-            bool produce_proofs = g->proofs_enabled();
 
-            if (produce_models) {
-                mc = datalog::mk_skip_model_converter();
-            }
-            if (produce_proofs) {
-                pc = datalog::mk_skip_proof_converter();
-            }
 
             func_decl* query_pred = to_app(q)->get_decl();
             m_ctx.set_output_predicate(query_pred);
             m_ctx.get_rules(); // flush adding rules.
+<<<<<<< HEAD
             m_ctx.set_model_converter(mc);
             m_ctx.set_proof_converter(pc);
+=======
+>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
             m_ctx.apply_default_transformation();
             
             if (m_ctx.get_params().slice()) {
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 8bdff1800..d4027d73d 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -950,16 +950,45 @@ namespace pdr {
         return out;
     }
 
+    /**
+       \brief Ensure that all nodes in the tree have associated models.
+       get_trace and get_proof_trace rely on models to extract rules.
+     */
+    void model_search::update_models() {
+        obj_map<expr, model*> models;
+        ptr_vector<model_node> todo;
+        todo.push_back(m_root);
+        while (!todo.empty()) {
+            model_node* n = todo.back();
+            if (n->get_model_ptr()) {
+                models.insert(n->state(), n->get_model_ptr());
+            }
+            todo.pop_back();
+            todo.append(n->children().size(), n->children().c_ptr());
+        }
+
+        todo.push_back(m_root);
+        while (!todo.empty()) {
+            model_node* n = todo.back();
+            model* md = 0;
+            if (!n->get_model_ptr() && models.find(n->state(), md)) {
+                model_ref mr(md);
+                n->set_model(mr);
+            }
+            todo.pop_back();
+            todo.append(n->children().size(), n->children().c_ptr());
+        }        
+    }
+
     /**
        Extract trace comprising of constraints 
        and predicates that are satisfied from facts to the query.
        The resulting trace 
      */
-    expr_ref model_search::get_trace(context const& ctx) const {       
+    expr_ref model_search::get_trace(context const& ctx) {       
         pred_transformer& pt = get_root().pt();
         ast_manager& m = pt.get_manager();
         manager& pm = pt.get_pdr_manager();
-
         datalog::context& dctx = ctx.get_context();
         datalog::rule_manager& rm = dctx.get_rule_manager();
         expr_ref_vector constraints(m), predicates(m);
@@ -968,22 +997,24 @@ namespace pdr {
         unsigned deltas[2];
         datalog::rule_ref rule(rm), r0(rm);
         model_node* n = m_root;
-        datalog::var_counter& vc = rm.get_var_counter();
+        datalog::rule_counter& vc = rm.get_counter();
         substitution subst(m);
         unifier unif(m);
         rule = n->get_rule();
-        unsigned max_var = vc.get_max_var(*rule);
+        unsigned max_var = vc.get_max_rule_var(*rule);
         predicates.push_back(rule->get_head());
-        children.append(n);
+        children.push_back(n);
         bool first = true;
+        update_models();
         while (!children.empty()) {
             SASSERT(children.size() == predicates.size());
             expr_ref_vector binding(m);
             n = children.back();
             children.pop_back();
+            TRACE("pdr", n->display(tout, 0););
             n->mk_instantiate(r0, rule, binding);
             
-            max_var = std::max(max_var, vc.get_max_var(*rule));
+            max_var = std::max(max_var, vc.get_max_rule_var(*rule));
             subst.reset();
             subst.reserve(2, max_var+1);
             deltas[0] = 0;
@@ -1026,7 +1057,7 @@ namespace pdr {
         return pm.mk_and(constraints);
     }
 
-    proof_ref model_search::get_proof_trace(context const& ctx) const {
+    proof_ref model_search::get_proof_trace(context const& ctx) {
         pred_transformer& pt = get_root().pt();
         ast_manager& m = pt.get_manager();
         datalog::context& dctx = ctx.get_context();
@@ -1042,8 +1073,10 @@ namespace pdr {
         proof* pr = 0;
         unifier.set_normalize(false);
         todo.push_back(m_root);
+        update_models();
         while (!todo.empty()) {
             model_node* n = todo.back();
+            TRACE("pdr", n->display(tout, 0););
             if (cache.find(n->state(), pr)) {
                 todo.pop_back();
                 continue;
@@ -1066,12 +1099,14 @@ namespace pdr {
                 continue;
             }
             proof_ref rl(m);
-            expr_ref  fml0(m);
             expr_ref_vector binding(m);
             n->mk_instantiate(r0, r1, binding);
-            r0->to_formula(fml0);
             proof_ref p1(m), p2(m);
-            p1 = m.mk_asserted(fml0);
+            p1 = r0->get_proof();
+            if (!p1) {
+                r0->display(dctx, std::cout);
+            }
+            SASSERT(p1);
             pfs[0] = p1;
             rls[0] = r1;
             TRACE("pdr",
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 32f13cdd4..6aa02ef10 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -240,6 +240,7 @@ namespace pdr {
         void erase_leaf(model_node& n);
         void remove_node(model_node& n);
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
+        void update_models();
     public:
         model_search(bool bfs): m_bfs(bfs), m_root(0) {}
         ~model_search();
@@ -253,8 +254,8 @@ namespace pdr {
         void set_root(model_node* n);
         model_node& get_root() const { return *m_root; }
         std::ostream& display(std::ostream& out) const; 
-        expr_ref get_trace(context const& ctx) const;
-        proof_ref get_proof_trace(context const& ctx) const;
+        expr_ref get_trace(context const& ctx);
+        proof_ref get_proof_trace(context const& ctx);
         void backtrack_level(bool uses_level, model_node& n);
     };
 
@@ -299,7 +300,7 @@ namespace pdr {
         decl2rel             m_rels;         // Map from relation predicate to fp-operator.       
         func_decl_ref        m_query_pred;
         pred_transformer*    m_query;
-        model_search         m_search;
+        mutable model_search m_search;
         lbool                m_last_result;
         unsigned             m_inductive_lvl;
         ptr_vector<core_generalizer>  m_core_generalizers;
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 3498b7969..033057683 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -85,6 +85,7 @@ lbool dl_interface::query(expr * query) {
     m_pred2slice.reset();
     ast_manager& m =                      m_ctx.get_manager();
     datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
+
     datalog::rule_set        old_rules(m_ctx.get_rules());
     func_decl_ref            query_pred(m);
     datalog::rule_ref_vector query_rules(rule_manager);
@@ -112,8 +113,13 @@ lbool dl_interface::query(expr * query) {
           m_ctx.display_rules(tout);
           );
 
+<<<<<<< HEAD
     m_ctx.set_output_predicate(query_pred);
 
+=======
+
+    m_ctx.set_output_predicate(query_pred);
+>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
     m_ctx.apply_default_transformation();
 
     if (m_ctx.get_params().slice()) {
@@ -141,10 +147,19 @@ lbool dl_interface::query(expr * query) {
         transf1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
         transf2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
         if (m_ctx.get_params().coalesce_rules()) {
+<<<<<<< HEAD
             m_ctx.transform_rules(transf1);
+=======
+            transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+            m_ctx.transform_rules(transformer1);
+>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
         }
         while (num_unfolds > 0) {
+<<<<<<< HEAD
             m_ctx.transform_rules(transf2);
+=======
+            m_ctx.transform_rules(transformer2);
+>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
             --num_unfolds;
         }
     }
@@ -168,8 +183,8 @@ lbool dl_interface::query(expr * query) {
     
     datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode.
 
-    m_context->set_proof_converter(pc);
-    m_context->set_model_converter(mc);
+    m_context->set_proof_converter(m_ctx.get_proof_converter());
+    m_context->set_model_converter(m_ctx.get_model_converter());
     m_context->set_query(query_pred);
     m_context->set_axioms(bg_assertion);
     m_context->update_rules(m_pdr_rules);
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index 4cdfb186e..1b8ea22f9 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -228,11 +228,13 @@ namespace pdr {
             is_lower = !is_lower;
         }
 
+        vector<term_loc_t> bound;
+        bound.push_back(std::make_pair(x, i));
         if (is_lower) {
-            m_lb.insert(abs(r), std::make_pair(x, i));
+            m_lb.insert(abs(r), bound);
         }
         else {
-            m_ub.insert(abs(r), std::make_pair(x, i));
+            m_ub.insert(abs(r), bound);
         }
     }
 
diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp
index 5cc97893a..4a7b4b995 100644
--- a/src/muz_qe/pdr_quantifiers.cpp
+++ b/src/muz_qe/pdr_quantifiers.cpp
@@ -612,8 +612,8 @@ namespace pdr {
         datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
         for (; it != end; ++it) {
             datalog::rule* r = *it;
-            datalog::var_counter vc(true);
-            unsigned max_var = vc.get_max_var(*r);
+            datalog::rule_counter vc(true);
+            unsigned max_var = vc.get_max_rule_var(*r);
             app_ref_vector body(m);
             for (unsigned i = 0; i < m_instantiations.size(); ++i) {
                 if (r == m_instantiated_rules[i]) {
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index 5f018895c..be3f80f92 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -2492,7 +2492,13 @@ class qe_lite_tactic : public tactic {
                 new_f = f;
                 m_qe(new_f, new_pr);
                 if (produce_proofs) {
-                    new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
+                    expr* fact = m.get_fact(new_pr);
+                    if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
+                        new_pr = m.mk_modus_ponens(g->pr(i), new_pr);                        
+                    }
+                    else {
+                        new_pr = g->pr(i);
+                    }
                 }
                 g->update(i, new_f, new_pr, g->dep(i));                
             }
diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp
index 72727bea8..9ee059f44 100644
--- a/src/muz_qe/tab_context.cpp
+++ b/src/muz_qe/tab_context.cpp
@@ -317,7 +317,7 @@ namespace tb {
             for (unsigned i = utsz; i < tsz; ++i) {
                 fmls.push_back(r->get_tail(i));
             }
-            m_num_vars = 1 + r.get_manager().get_var_counter().get_max_var(*r);
+            m_num_vars = 1 + r.get_manager().get_counter().get_max_rule_var(*r);
             m_head = r->get_head();
             m_predicates.reset();
             for (unsigned i = 0; i < utsz; ++i) {
@@ -1644,9 +1644,7 @@ namespace datalog {
         void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, 
                           expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const {
             unsigned idx = r1.get_predicate_index();
-            expr_ref fml1 = r1.to_formula();
-            expr_ref fml2 = r2.to_formula();
-            expr_ref fml3 = res.to_formula();
+            expr_ref fml = res.to_formula();
             vector<expr_ref_vector> substs;
             svector<std::pair<unsigned, unsigned> > positions;
             substs.push_back(s1);
@@ -1654,13 +1652,12 @@ namespace datalog {
             scoped_proof _sc(m);
             proof_ref pr(m);
             proof_ref_vector premises(m);
-            premises.push_back(m.mk_asserted(fml1));
-            premises.push_back(m.mk_asserted(fml2));
+            premises.push_back(m.mk_asserted(r1.to_formula()));
+            premises.push_back(m.mk_asserted(r2.to_formula()));
             positions.push_back(std::make_pair(idx+1, 0));            
-            pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
+            pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
             pc.insert(pr);
-        }
-            
+        }            
     };
 
     tab::tab(context& ctx):
diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp
index 2b67c3a71..7d3f96ae4 100644
--- a/src/test/bit_vector.cpp
+++ b/src/test/bit_vector.cpp
@@ -276,12 +276,35 @@ static void tst_bv_reset() {
     }
 }
 
+static void tst_eq() {
+    bit_vector b1, b2, b3;
+    b1.resize(32);
+    b2.resize(32);
+    b3.resize(32);
+
+    b1.set(3, true);
+    SASSERT(b1 != b2);
+    SASSERT(!(b1 == b2));
+    SASSERT(b2 == b3);
+
+    b3.set(3, true);
+    SASSERT(b1 == b3);
+    SASSERT(!(b1 != b3));
+    
+    b2.set(31, true);
+    b3.set(31);
+    b3.unset(3);
+    SASSERT(b2 == b3);
+    SASSERT(!(b2 != b3));
+}
+
 void tst_bit_vector() {
     tst_crash();
     tst_shift(); 
     tst_or();
     tst_and();
     tst_bv_reset();
+    tst_eq();
     return;
     tst2();
     for (unsigned i = 0; i < 20; i++) {
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index 210d230bc..2328a5849 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -116,7 +116,7 @@ void bit_vector::shift_right(unsigned k) {
     }
 }
 
-bool bit_vector::operator==(bit_vector const & source) {
+bool bit_vector::operator==(bit_vector const & source) const {
     if (m_num_bits != source.m_num_bits)
         return false;
     unsigned n = num_words();
@@ -129,6 +129,7 @@ bool bit_vector::operator==(bit_vector const & source) {
     }
     unsigned bit_rest = source.m_num_bits % 32;
     unsigned mask = (1 << bit_rest) - 1;
+    if (mask == 0) mask = UINT_MAX;
     return (m_data[i] & mask) == (source.m_data[i] & mask);
 }
 
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 9560af7e2..2e7becee7 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -171,9 +171,9 @@ public:
             resize(sz, val);
     }
 
-    bool operator==(bit_vector const & other);
+    bool operator==(bit_vector const & other) const;
 
-    bool operator!=(bit_vector const & other) { return !operator==(other); }
+    bool operator!=(bit_vector const & other) const { return !operator==(other); }
 
     bit_vector & operator=(bit_vector const & source) {
         m_num_bits = source.m_num_bits;
diff --git a/src/util/vector.h b/src/util/vector.h
index a9d36b202..704452d0f 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -151,23 +151,6 @@ public:
         }
     }
 
-    vector(T const & e) : 
-        m_data(0) { 
-        push_back(e); 
-    }
-
-    vector(T const & t1, T const & t2) : 
-        m_data(0) { 
-        push_back(t1); 
-        push_back(t2); 
-    }
-
-    vector(T const & t1, T const & t2, T const & t3) : 
-        m_data(0) { 
-        push_back(t1); 
-        push_back(t2); 
-        push_back(t3); 
-    }
  
     ~vector() { 
         destroy();