diff --git a/src/ast/proofs/proof_utils.cpp b/src/ast/proofs/proof_utils.cpp
index bd82696ea..b6c8b58d7 100644
--- a/src/ast/proofs/proof_utils.cpp
+++ b/src/ast/proofs/proof_utils.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/proofs/proof_utils.h"
 #include "ast/proofs/proof_checker.h"
+#include "util/container_util.h"
 
 
 
@@ -331,3 +332,678 @@ void reduce_hypotheses(proof_ref &pr) {
                SASSERT(pc.check(pr, side));
               );
 }
+
+
+
+#include "ast/ast_smt2_pp.h"
+#include "ast/rewriter/var_subst.h"
+
+class reduce_hypotheses0 {
+    typedef obj_hashtable<expr> expr_set;
+    ast_manager&          m;
+    // reference for any expression created by the tranformation
+    expr_ref_vector       m_refs;
+    // currently computed result
+    obj_map<proof,proof*> m_cache;
+    // map conclusions to closed proofs that derive them
+    obj_map<expr, proof*> m_units;
+    // currently active units
+    ptr_vector<expr>      m_units_trail;
+    // size of m_units_trail at the last push
+    unsigned_vector       m_limits;
+    // map from proofs to active hypotheses
+    obj_map<proof, expr_set*> m_hypmap;
+    // refernce train for hypotheses sets
+    ptr_vector<expr_set>  m_hyprefs;
+    ptr_vector<expr>      m_literals;
+    
+    void reset() {
+        m_refs.reset();
+        m_cache.reset();
+        m_units.reset();
+        m_units_trail.reset();
+        m_limits.reset();
+        std::for_each(m_hyprefs.begin(), m_hyprefs.end(), delete_proc<expr_set>());
+        m_hypmap.reset();
+        m_hyprefs.reset();
+        m_literals.reset();
+    }
+    
+    void push() {
+        m_limits.push_back(m_units_trail.size());
+    }
+    
+    void pop() {
+        unsigned sz = m_limits.back();
+        while (m_units_trail.size() > sz) {
+            m_units.remove(m_units_trail.back());
+            m_units_trail.pop_back();
+        }
+        m_limits.pop_back();
+    }
+    
+    void get_literals(expr* clause) {
+        m_literals.reset();
+        if (m.is_or(clause)) {
+            m_literals.append(to_app(clause)->get_num_args(), to_app(clause)->get_args());                
+        }
+        else {
+            m_literals.push_back(clause);
+        }
+    }
+    
+    void add_hypotheses(proof* p) {
+        expr_set* hyps = 0;
+        bool inherited = false;
+        if (p->get_decl_kind() == PR_HYPOTHESIS) {
+            hyps = alloc(expr_set);
+            hyps->insert(m.get_fact(p));
+            m_hyprefs.push_back(hyps);
+        }
+        else {
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                expr_set* hyps1 = m_hypmap.find(m.get_parent(p, i));
+                if (hyps1) {
+                    if (!hyps) {
+                        hyps = hyps1;
+                        inherited = true;
+                        continue;
+                    }
+                    if (inherited) {
+                        hyps = alloc(expr_set,*hyps);
+                        m_hyprefs.push_back(hyps);
+                        inherited = false;
+                    }
+                    set_union(*hyps, *hyps1);
+                }
+            }
+        }
+        m_hypmap.insert(p, hyps);
+    }
+
+    expr_ref complement_lit(expr* e) {
+        expr* e1;
+        if (m.is_not(e, e1)) {
+            return expr_ref(e1, m);
+        }
+        else {
+            return expr_ref(m.mk_not(e), m);
+        }
+    }
+    
+    bool in_hypotheses(expr* e, expr_set* hyps) {
+        if (!hyps) {
+            return false;
+        }
+        expr_ref not_e = complement_lit(e);
+        return hyps->contains(not_e);
+    }
+
+    bool contains_hypothesis(proof* p) {
+        ptr_vector<proof> todo;
+        ast_mark visit;
+        todo.push_back(p);
+        while (!todo.empty()) {
+            p = todo.back();
+            todo.pop_back();
+            if (visit.is_marked(p)) {
+                continue;
+            }
+            visit.mark(p, true);
+            if (PR_HYPOTHESIS == p->get_decl_kind()) {
+                return true;
+            }
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                todo.push_back(m.get_parent(p, i));
+            }
+        }
+        return false;
+    }
+
+    bool is_closed(proof* p) {
+        expr_set* hyps = m_hypmap.find(p);
+        return !hyps || hyps->empty();
+    }    
+    
+public:
+    reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
+    
+    void operator()(proof_ref& pr) {
+        proof_ref tmp(m);
+        tmp = pr;
+        elim(pr);
+        reset();
+        CTRACE("proof_utils", contains_hypothesis(pr),
+            tout << "Contains hypothesis:\n";
+            tout << mk_ismt2_pp(tmp, m) << "\n====>\n";
+            tout << mk_ismt2_pp(pr, m) << "\n";);
+        
+    }
+    
+    void elim(proof_ref& p) {
+        proof_ref tmp(m);
+        proof* result = p.get();
+        if (m_cache.find(p, result)) {
+            p = result;
+            return;
+        }
+        //SASSERT (p.get () == result);
+        switch(p->get_decl_kind()) {
+        case PR_HYPOTHESIS:
+            // replace result by m_units[m.get_fact (p)] if defined
+            // AG: This is the main step. Replace a hypothesis by a derivation of its consequence
+            if (!m_units.find(m.get_fact(p), result)) {
+                // restore ther result back to p
+                result = p.get();
+            }
+            // compute hypothesis of the result
+            // not clear what 'result' is at this point.
+            // probably the proof at the top of the call
+            // XXX not clear why this is re-computed each time
+            // XXX moreover, m_units are guaranteed to be closed!
+            // XXX so no hypotheses are needed for them
+            add_hypotheses(result);
+            break;
+        case PR_LEMMA: {
+            SASSERT(m.get_num_parents(p) == 1);
+            tmp = m.get_parent(p, 0);
+            // eliminate hypothesis recursively in the proof of the lemma
+            elim(tmp);
+            expr_set* hyps = m_hypmap.find(tmp);
+            expr_set* new_hyps = 0;
+            // XXX if the proof is correct, the hypotheses of the tmp
+            // XXX should be exactly those of the consequence of the lemma
+            // XXX but if this code actually eliminates hypotheses, the set might be a subset
+            if (hyps) {
+                new_hyps = alloc(expr_set, *hyps);
+            }
+            expr* fact = m.get_fact(p);
+            // when hypothesis is a single literal of the form 
+            // (or A B), and the fact of p is (or A B).            
+            if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
+                m_literals.reset();
+                m_literals.push_back(fact);
+            }
+            else {
+                get_literals(fact);
+            }
+
+            // go over all the literals in the consequence of the lemma
+            for (unsigned i = 0; i < m_literals.size(); ++i) {
+                expr* e = m_literals[i];
+                // if the literal is not in hypothesis, skip it
+                if (!in_hypotheses(e, hyps)) {
+                    m_literals[i] = m_literals.back();
+                    m_literals.pop_back();
+                    --i;
+                }
+                // if the literal is in hypothesis remove it because
+                // it is not in hypothesis set of the lemma
+                // XXX but we assume that lemmas have empty hypothesis set.
+                // XXX eventually every element of new_hyps must be removed!
+                else {
+                    SASSERT(new_hyps);
+                    expr_ref not_e = complement_lit(e);
+                    SASSERT(new_hyps->contains(not_e));
+                    new_hyps->remove(not_e);
+                }
+            }
+            // killed all hypotheses, so can stop at the lemma since
+            // we have a closed pf of false
+            if (m_literals.empty()) {
+                result = tmp;
+            }
+            else {
+                // create a new lemma, but might be re-creating existing one
+                expr_ref clause(m);
+                if (m_literals.size() == 1) {
+                    clause = m_literals[0];
+                }
+                else {
+                    clause = m.mk_or(m_literals.size(), m_literals.c_ptr());
+                }
+                tmp = m.mk_lemma(tmp, clause);
+                m_refs.push_back(tmp);
+                result = tmp;
+            }
+            if (new_hyps && new_hyps->empty()) {
+                dealloc(new_hyps);
+                new_hyps = 0;
+            }
+            m_hypmap.insert(result, new_hyps);
+            // might push 0 into m_hyprefs. No reason for that
+            m_hyprefs.push_back(new_hyps);
+            TRACE("proof_utils",            
+                    tout << "New lemma: " << mk_pp(m.get_fact(p), m) 
+                      << "\n==>\n" 
+                      << mk_pp(m.get_fact(result), m) << "\n";
+                if (hyps) {
+                    expr_set::iterator it = hyps->begin();
+                    expr_set::iterator end = hyps->end();
+                    for (; it != end; ++it) {
+                        tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
+                    }
+                });                               
+            
+            break;
+        }
+        case PR_UNIT_RESOLUTION: {
+            proof_ref_vector parents(m);
+            // get the clause being resolved with
+            parents.push_back(m.get_parent(p, 0));
+            // save state
+            push();
+            bool found_false = false;
+            // for every derivation of a unit literal
+            for (unsigned i = 1; i < m.get_num_parents(p); ++i) {
+                // see if it derives false
+                tmp = m.get_parent(p, i);
+                elim(tmp);
+                if (m.is_false(m.get_fact(tmp))) {
+                    // if derived false, the whole pf is false and we can bail out
+                    result = tmp;
+                    found_false = true;
+                    break;
+                }
+                // -- otherwise, the fact has not changed. nothing to simplify
+                SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+                parents.push_back(tmp);          
+                // remember that we have this derivation while we have not poped the trail
+                // but only if the proof is closed (i.e., a real unit)
+                if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
+                    m_units.insert(m.get_fact(tmp), tmp);
+                    m_units_trail.push_back(m.get_fact(tmp));
+                }
+            }
+            if (found_false) {
+                pop();
+                break;
+            }
+            // look at the clause being resolved with
+            tmp = m.get_parent(p, 0);
+            // remember its fact
+            expr* old_clause = m.get_fact(tmp);
+            // attempt to reduce its fact
+            elim(tmp);
+            // update parents
+            parents[0] = tmp;
+            // if the new fact is false, bail out
+            expr* clause = m.get_fact(tmp);
+            if (m.is_false(clause)) {
+                m_refs.push_back(tmp);
+                result = tmp;
+                pop();
+                break;
+            }
+            //
+            // case where clause is a literal in the old clause.
+            // i.e., reduce multi-literal clause to a unit
+            //
+            if (is_literal_in_clause(clause, old_clause)) {
+                // if the resulting literal was resolved, get a pf of false and bail out
+                bool found = false;
+                for (unsigned i = 1; !found && i < parents.size(); ++i) {
+                    if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
+                        parents[1] = parents[i].get();
+                        parents.resize(2);
+                        result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
+                        m_refs.push_back(result);               
+                        add_hypotheses(result);
+                        found = true;
+                    }                    
+                }
+                // else if the resulting literal is not resolved, it is the new consequence  
+                if (!found) {
+                    result = parents[0].get();
+                }
+                pop(); 
+                break;
+            }
+            //
+            // case where new clause is a subset of old clause.
+            // the literals in clause should be a subset of literals in old_clause.
+            // 
+            get_literals(clause);
+            for (unsigned i = 1; i < parents.size(); ++i) {
+                bool found = false;
+                for (unsigned j = 0; j < m_literals.size(); ++j) {
+                    if (m.is_complement(m_literals[j], m.get_fact(parents[i].get()))) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    // literal was removed as hypothesis.
+                    parents[i] = parents.back();
+                    parents.pop_back();
+                    --i;
+                }
+            }
+            if (parents.size() == 1) {
+                result = parents[0].get();
+            }
+            else {
+                result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
+                m_refs.push_back(result);               
+                add_hypotheses(result);
+            }
+            pop();
+            break;
+        }                
+        default: {
+            ptr_buffer<expr> args;
+            bool change = false;
+            bool found_false = false;
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                tmp = m.get_parent(p, i);
+                elim(tmp);
+                if (m.is_false(m.get_fact(tmp))) {
+                    result = tmp;
+                    found_false = true;
+                    break;
+                }
+                // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+                change = change || (tmp != m.get_parent(p, i));
+                args.push_back(tmp);
+            }
+            if (found_false) {
+                break;
+            }
+            if (m.has_fact(p)) {
+                args.push_back(m.get_fact(p));
+            }
+            if (change) {
+                tmp = m.mk_app(p->get_decl(), args.size(), args.c_ptr());
+                m_refs.push_back(tmp);
+            }
+            else {
+                tmp = p;
+            }
+            result = tmp;                
+            add_hypotheses(result);
+            break;
+        }
+        }          
+        SASSERT(m_hypmap.contains(result));
+        m_cache.insert(p, result);
+        p = result;
+    }        
+
+    bool is_literal_in_clause(expr* fml, expr* clause) {
+        if (!m.is_or(clause)) {
+            return false;
+        }
+        app* cl = to_app(clause);
+        for (unsigned i = 0; i < cl->get_num_args(); ++i) {
+            if (cl->get_arg(i) == fml) {
+                return true;
+            }
+        }
+        return false;
+    }
+};
+
+void proof_utils::reduce_hypotheses(proof_ref& pr) {
+    ast_manager& m = pr.get_manager();
+    class reduce_hypotheses0 reduce(m);
+    reduce(pr);
+    CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
+}
+
+class proof_is_closed {
+    ast_manager&     m;
+    ptr_vector<expr> m_literals;
+    ast_mark         m_visit;
+
+    void reset() {
+        m_literals.reset();
+        m_visit.reset();
+    }
+
+    bool check(proof* p) {
+        // really just a partial check because nodes may be visited 
+        // already under a different lemma scope.
+        if (m_visit.is_marked(p)) {
+            return true;
+        }
+        bool result = false;
+        m_visit.mark(p, true);
+        switch(p->get_decl_kind()) {
+        case PR_LEMMA: {
+            unsigned sz = m_literals.size();
+            expr* cls = m.get_fact(p);
+            m_literals.push_back(cls);
+            if (m.is_or(cls)) {
+                m_literals.append(to_app(cls)->get_num_args(), to_app(cls)->get_args());
+            }
+            SASSERT(m.get_num_parents(p) == 1);
+            result = check(m.get_parent(p, 0));
+            m_literals.resize(sz);
+            break;            
+        }
+        case PR_HYPOTHESIS: {
+            expr* fact = m.get_fact(p);
+            for (unsigned i = 0; i < m_literals.size(); ++i) {
+                if (m.is_complement(m_literals[i], fact)) {
+                    result = true;
+                    break;
+                }
+            }
+            break;
+        }
+        default: 
+            result = true;
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                if (!check(m.get_parent(p, i))) {
+                    result = false;
+                    break;
+                }
+            }
+            break;
+        }
+        
+        return result;
+    }
+    
+public:
+    proof_is_closed(ast_manager& m): m(m) {}
+
+    bool operator()(proof *p) {
+        bool ok = check(p);
+        reset();
+        return ok;
+    }
+};
+
+bool proof_utils::is_closed(ast_manager& m, proof* p) {
+    proof_is_closed checker(m);
+    return checker(p);
+}
+
+
+static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
+    ast_manager& m = pr.get_manager();
+    proof* pr2 = 0;
+    proof_ref_vector parents(m);
+    proof_ref prNew(pr); 
+    if (cache.find(pr, pr2)) {
+        pr = pr2;
+        return;
+    }
+    
+    for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
+        prNew = m.get_parent(pr, i);
+        permute_unit_resolution(refs, cache, prNew);
+        parents.push_back(prNew);
+    }
+    
+    prNew = pr;
+    if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
+        parents[0]->get_decl_kind() == PR_TH_LEMMA) { 
+        /*
+          Unit resolution:
+          T1:      (or l_1 ... l_n l_1' ... l_m')
+          T2:      (not l_1)
+          ...
+          T(n+1):  (not l_n)
+                   [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
+          Th lemma:
+          T1:      (not l_1)
+          ...
+          Tn:      (not l_n)
+          [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
+                    
+          Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
+                    
+          Implement conversion:
+                    
+                 T1 |- not l_1 ... Tn |- not l_n  
+                 -------------------------------  TH_LEMMA
+                          (or k_1 .. k_m j_1 ... j_m)    S1 |- not k_1 ... Sm |- not k_m
+                          -------------------------------------------------------------- UNIT_RESOLUTION
+                                        (or j_1 .. j_m)
+
+
+            |-> 
+
+                    T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
+                    ---------------------------------------------------------------- TH_LEMMA
+                                        (or j_1 .. j_m)
+
+        */
+        proof_ref_vector premises(m);
+        proof* thLemma = parents[0].get();
+        for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
+            premises.push_back(m.get_parent(thLemma, i));
+        }
+        for (unsigned i = 1; i < parents.size(); ++i) {
+            premises.push_back(parents[i].get());
+        }
+        parameter const* params = thLemma->get_decl()->get_parameters();
+        unsigned num_params = thLemma->get_decl()->get_num_parameters();
+        SASSERT(params[0].is_symbol());
+        family_id tid = m.mk_family_id(params[0].get_symbol());
+        SASSERT(tid != null_family_id);
+        // AG: This can break a theory lemma. In particular, for Farkas lemmas the coefficients
+        // AG: for the literals propagated from the unit resolution are missing.
+        // AG: Why is this a good thing to do?
+        // AG: This can lead to merging of the units with other terms in interpolation,
+        // AG: but without farkas coefficients this does not make sense
+        prNew = m.mk_th_lemma(tid, m.get_fact(pr), 
+                              premises.size(), premises.c_ptr(), num_params-1, params+1);
+    }
+    else {
+        ptr_vector<expr> args;
+        for (unsigned i = 0; i < parents.size(); ++i) {
+            args.push_back(parents[i].get());
+        }
+        if (m.has_fact(pr)) {
+            args.push_back(m.get_fact(pr));
+        }
+        prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
+    }    
+    
+    cache.insert(pr, prNew);
+    refs.push_back(prNew);
+    pr = prNew;
+}
+
+
+// permute unit resolution over Theory lemmas to track premises.
+void proof_utils::permute_unit_resolution(proof_ref& pr) {
+    expr_ref_vector refs(pr.get_manager());
+    obj_map<proof,proof*> cache;
+    ::permute_unit_resolution(refs, cache, pr);
+}
+
+class push_instantiations_up_cl {
+    ast_manager& m;
+public:
+    push_instantiations_up_cl(ast_manager& m): m(m) {}
+
+    void operator()(proof_ref& p) {
+        expr_ref_vector s0(m);
+        p = push(p, s0);
+    }
+
+private:
+
+    proof* push(proof* p, expr_ref_vector const& sub) {
+        proof_ref_vector premises(m);
+        expr_ref conclusion(m);
+        svector<std::pair<unsigned, unsigned> >  positions;
+        vector<expr_ref_vector> substs;
+
+        if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
+            for (unsigned i = 0; i < premises.size(); ++i) {
+                compose(substs[i], sub);
+                premises[i] = push(premises[i].get(), substs[i]);
+                substs[i].reset();
+            }
+            instantiate(sub, conclusion);
+            return 
+                m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, 
+                                   positions, 
+                                   substs);
+        }        
+        if (sub.empty()) {
+            return p;
+        }
+        if (m.is_modus_ponens(p)) {
+            SASSERT(m.get_num_parents(p) == 2);
+            proof* p0 = m.get_parent(p, 0);
+            proof* p1 = m.get_parent(p, 1);
+            if (m.get_fact(p0) == m.get_fact(p)) {
+                return push(p0, sub);
+            }
+            expr* e1, *e2;
+            if (m.is_rewrite(p1, e1, e2) && 
+                is_quantifier(e1) && is_quantifier(e2) &&
+                to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
+                expr_ref r1(e1,m), r2(e2,m);
+                instantiate(sub, r1);
+                instantiate(sub, r2);
+                p1 = m.mk_rewrite(r1, r2);
+                return m.mk_modus_ponens(push(p0, sub), p1);
+            }
+        }
+        premises.push_back(p);
+        substs.push_back(sub);
+        conclusion = m.get_fact(p);
+        instantiate(sub, conclusion);
+        return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
+    }
+
+    void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
+        for (unsigned i = 0; i < sub.size(); ++i) {
+            expr_ref e(m);
+            var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
+            sub[i] = e;            
+        }
+    }
+
+    void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
+        if (sub.empty()) {
+            return;
+        }
+        if (!is_forall(fml)) {
+            return;
+        }
+        quantifier* q = to_quantifier(fml);
+        if (q->get_num_decls() != sub.size()) {
+            TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
+                  tout << mk_pp(q, m) << "\n";
+                  tout << sub.size() << "\n";);
+            return;
+        }
+        var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
+    }
+
+};
+
+void proof_utils::push_instantiations_up(proof_ref& pr) {
+    push_instantiations_up_cl push(pr.get_manager());
+    push(pr);
+}
+
+
diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index 7963d52de..f813b96ad 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -16,8 +16,8 @@ Revision History:
 
 --*/
 
-#ifndef _PROOF_UTILS_H_
-#define _PROOF_UTILS_H_
+#ifndef PROOF_UTILS_H_
+#define PROOF_UTILS_H_
 #include "ast/ast.h"
 
 /*
@@ -39,4 +39,31 @@ private:
 void reduce_hypotheses(proof_ref &pr);
 
 
+class proof_utils {
+public:
+    /**
+       \brief reduce the set of hypotheses used in the proof.
+     */
+    static void reduce_hypotheses(proof_ref& pr);
+
+    /**
+       \brief Check that a proof does not contain open hypotheses.
+    */
+    static bool is_closed(ast_manager& m, proof* p);
+
+    /**
+       \brief Permute unit resolution rule with th-lemma
+    */
+    static void permute_unit_resolution(proof_ref& pr);
+
+    /**
+       \brief Push instantiations created in hyper-resolutions up to leaves.
+       This produces a "ground" proof where leaves are annotated by instantiations.
+    */
+    static void push_instantiations_up(proof_ref& pr);
+
+
+};
+
+
 #endif
diff --git a/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt
index ec1ce47c3..6b0334664 100644
--- a/src/muz/base/CMakeLists.txt
+++ b/src/muz/base/CMakeLists.txt
@@ -10,7 +10,6 @@ z3_add_component(muz
     dl_rule_transformer.cpp
     dl_util.cpp
     hnf.cpp
-    proof_utils.cpp
     rule_properties.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
diff --git a/src/muz/base/dl_boogie_proof.cpp b/src/muz/base/dl_boogie_proof.cpp
index ec999c05e..8f4f9c02d 100644
--- a/src/muz/base/dl_boogie_proof.cpp
+++ b/src/muz/base/dl_boogie_proof.cpp
@@ -53,7 +53,7 @@ Example from Boogie:
 
 #include "muz/base/dl_boogie_proof.h"
 #include "model/model_pp.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index d04e4037c..c560ee28e 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -11,7 +11,7 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2010-05-20.
+    Krystof Hoder 2010
 
 Revision History:
 
@@ -31,6 +31,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/stopwatch.h"
 #include "util/lbool.h"
+#include "util/container_util.h"
 
 namespace datalog {
 
@@ -381,129 +382,6 @@ namespace datalog {
     */
     void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub);
 
-    // -----------------------------------
-    //
-    // container functions
-    //
-    // -----------------------------------
-
-    template<class Set1, class Set2>
-    void set_intersection(Set1 & tgt, const Set2 & src) {
-        svector<typename Set1::data> to_remove;
-        typename Set1::iterator vit = tgt.begin();
-        typename Set1::iterator vend = tgt.end();
-        for(;vit!=vend;++vit) {
-            typename Set1::data itm=*vit;
-            if(!src.contains(itm)) {
-                to_remove.push_back(itm);
-            }
-        }
-        while(!to_remove.empty()) {
-            tgt.remove(to_remove.back());
-            to_remove.pop_back();
-        }
-    }
-
-    template<class Set>
-    void set_difference(Set & tgt, const Set & to_remove) {
-        typename Set::iterator vit = to_remove.begin();
-        typename Set::iterator vend = to_remove.end();
-        for(;vit!=vend;++vit) {
-            typename Set::data itm=*vit;
-            tgt.remove(itm);
-        }
-    }
-
-    template<class Set1, class Set2>
-    void set_union(Set1 & tgt, const Set2 & to_add) {
-        typename Set2::iterator vit = to_add.begin();
-        typename Set2::iterator vend = to_add.end();
-        for(;vit!=vend;++vit) {
-            typename Set1::data itm=*vit;
-            tgt.insert(itm);
-        }
-    }
-
-    void idx_set_union(idx_set & tgt, const idx_set & src);
-
-    template<class T>
-    void unite_disjoint_maps(T & tgt, const T & src) {
-        typename T::iterator it = src.begin();
-        typename T::iterator end = src.end();
-        for(; it!=end; ++it) {
-            SASSERT(!tgt.contains(it->m_key));
-            tgt.insert(it->m_key, it->m_value);
-        }
-    }
-
-    template<class T, class U>
-    void collect_map_range(T & acc, const U & map) {
-        typename U::iterator it = map.begin();
-        typename U::iterator end = map.end();
-        for(; it!=end; ++it) {
-            acc.push_back(it->m_value);
-        }
-    }
-
-
-    template<class T>
-    void print_container(const T & begin, const T & end, std::ostream & out) {
-        T it = begin;
-        out << "(";
-        bool first = true;
-        for(; it!=end; ++it) {
-            if(first) { first = false; } else { out << ","; }
-            out << (*it);
-        }
-        out << ")";
-    }
-
-    template<class T>
-    void print_container(const T & cont, std::ostream & out) {
-        print_container(cont.begin(), cont.end(), out);
-    }
-
-    template<class T, class M>
-    void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
-        print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
-    }
-
-    template<class T>
-    void print_map(const T & cont, std::ostream & out) {
-        typename T::iterator it = cont.begin();
-        typename T::iterator end = cont.end();
-        out << "(";
-        bool first = true;
-        for(; it!=end; ++it) {
-            if(first) { first = false; } else { out << ","; }
-            out << it->m_key << "->" << it->m_value;
-        }
-        out << ")";
-    }
-
-    template<class It, class V> 
-    unsigned find_index(const It & begin, const It & end, const V & val) {
-        unsigned idx = 0;
-        It it = begin;
-        for(; it!=end; it++, idx++) {
-            if(*it==val) {
-                return idx;
-            }
-        }
-        return UINT_MAX;
-    }
-
-    template<class T, class U>
-    bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
-        T it1 = begin1;
-        U it2 = begin2;
-        for(; it1!=end1 && it2!=end2; ++it1, ++it2) {
-            if(*it1!=*it2) { 
-                return false;
-            }
-        }
-        return it1==end1 && it2==end2;
-    }
 
     template<class T, class U>
     bool vectors_equal(const T & c1, const U & c2) {
@@ -521,6 +399,8 @@ namespace datalog {
         return true;
     }
 
+    void idx_set_union(idx_set & tgt, const idx_set & src);
+
     template<class T>
     struct default_obj_chash {
         unsigned operator()(T const& cont, unsigned i) const {
diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp
deleted file mode 100644
index 87355a07b..000000000
--- a/src/muz/base/proof_utils.cpp
+++ /dev/null
@@ -1,680 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-#include "muz/base/dl_util.h"
-#include "muz/base/proof_utils.h"
-#include "ast/ast_smt2_pp.h"
-#include "ast/rewriter/var_subst.h"
-
-class reduce_hypotheses0 {
-    typedef obj_hashtable<expr> expr_set;
-    ast_manager&          m;
-    // reference for any expression created by the tranformation
-    expr_ref_vector       m_refs;
-    // currently computed result
-    obj_map<proof,proof*> m_cache;
-    // map conclusions to closed proofs that derive them
-    obj_map<expr, proof*> m_units;
-    // currently active units
-    ptr_vector<expr>      m_units_trail;
-    // size of m_units_trail at the last push
-    unsigned_vector       m_limits;
-    // map from proofs to active hypotheses
-    obj_map<proof, expr_set*> m_hypmap;
-    // refernce train for hypotheses sets
-    ptr_vector<expr_set>  m_hyprefs;
-    ptr_vector<expr>      m_literals;
-    
-    void reset() {
-        m_refs.reset();
-        m_cache.reset();
-        m_units.reset();
-        m_units_trail.reset();
-        m_limits.reset();
-        std::for_each(m_hyprefs.begin(), m_hyprefs.end(), delete_proc<expr_set>());
-        m_hypmap.reset();
-        m_hyprefs.reset();
-        m_literals.reset();
-    }
-    
-    void push() {
-        m_limits.push_back(m_units_trail.size());
-    }
-    
-    void pop() {
-        unsigned sz = m_limits.back();
-        while (m_units_trail.size() > sz) {
-            m_units.remove(m_units_trail.back());
-            m_units_trail.pop_back();
-        }
-        m_limits.pop_back();
-    }
-    
-    void get_literals(expr* clause) {
-        m_literals.reset();
-        if (m.is_or(clause)) {
-            m_literals.append(to_app(clause)->get_num_args(), to_app(clause)->get_args());                
-        }
-        else {
-            m_literals.push_back(clause);
-        }
-    }
-    
-    void add_hypotheses(proof* p) {
-        expr_set* hyps = 0;
-        bool inherited = false;
-        if (p->get_decl_kind() == PR_HYPOTHESIS) {
-            hyps = alloc(expr_set);
-            hyps->insert(m.get_fact(p));
-            m_hyprefs.push_back(hyps);
-        }
-        else {
-            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
-                expr_set* hyps1 = m_hypmap.find(m.get_parent(p, i));
-                if (hyps1) {
-                    if (!hyps) {
-                        hyps = hyps1;
-                        inherited = true;
-                        continue;
-                    }
-                    if (inherited) {
-                        hyps = alloc(expr_set,*hyps);
-                        m_hyprefs.push_back(hyps);
-                        inherited = false;
-                    }
-                    datalog::set_union(*hyps, *hyps1);
-                }
-            }
-        }
-        m_hypmap.insert(p, hyps);
-    }
-
-    expr_ref complement_lit(expr* e) {
-        expr* e1;
-        if (m.is_not(e, e1)) {
-            return expr_ref(e1, m);
-        }
-        else {
-            return expr_ref(m.mk_not(e), m);
-        }
-    }
-    
-    bool in_hypotheses(expr* e, expr_set* hyps) {
-        if (!hyps) {
-            return false;
-        }
-        expr_ref not_e = complement_lit(e);
-        return hyps->contains(not_e);
-    }
-
-    bool contains_hypothesis(proof* p) {
-        ptr_vector<proof> todo;
-        ast_mark visit;
-        todo.push_back(p);
-        while (!todo.empty()) {
-            p = todo.back();
-            todo.pop_back();
-            if (visit.is_marked(p)) {
-                continue;
-            }
-            visit.mark(p, true);
-            if (PR_HYPOTHESIS == p->get_decl_kind()) {
-                return true;
-            }
-            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
-                todo.push_back(m.get_parent(p, i));
-            }
-        }
-        return false;
-    }
-
-    bool is_closed(proof* p) {
-        expr_set* hyps = m_hypmap.find(p);
-        return !hyps || hyps->empty();
-    }    
-    
-public:
-    reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
-    
-    void operator()(proof_ref& pr) {
-        proof_ref tmp(m);
-        tmp = pr;
-        elim(pr);
-        reset();
-        CTRACE("proof_utils", contains_hypothesis(pr),
-            tout << "Contains hypothesis:\n";
-            tout << mk_ismt2_pp(tmp, m) << "\n====>\n";
-            tout << mk_ismt2_pp(pr, m) << "\n";);
-        
-    }
-    
-    void elim(proof_ref& p) {
-        proof_ref tmp(m);
-        proof* result = p.get();
-        if (m_cache.find(p, result)) {
-            p = result;
-            return;
-        }
-        //SASSERT (p.get () == result);
-        switch(p->get_decl_kind()) {
-        case PR_HYPOTHESIS:
-            // replace result by m_units[m.get_fact (p)] if defined
-            // AG: This is the main step. Replace a hypothesis by a derivation of its consequence
-            if (!m_units.find(m.get_fact(p), result)) {
-                // restore ther result back to p
-                result = p.get();
-            }
-            // compute hypothesis of the result
-            // not clear what 'result' is at this point.
-            // probably the proof at the top of the call
-            // XXX not clear why this is re-computed each time
-            // XXX moreover, m_units are guaranteed to be closed!
-            // XXX so no hypotheses are needed for them
-            add_hypotheses(result);
-            break;
-        case PR_LEMMA: {
-            SASSERT(m.get_num_parents(p) == 1);
-            tmp = m.get_parent(p, 0);
-            // eliminate hypothesis recursively in the proof of the lemma
-            elim(tmp);
-            expr_set* hyps = m_hypmap.find(tmp);
-            expr_set* new_hyps = 0;
-            // XXX if the proof is correct, the hypotheses of the tmp
-            // XXX should be exactly those of the consequence of the lemma
-            // XXX but if this code actually eliminates hypotheses, the set might be a subset
-            if (hyps) {
-                new_hyps = alloc(expr_set, *hyps);
-            }
-            expr* fact = m.get_fact(p);
-            // when hypothesis is a single literal of the form 
-            // (or A B), and the fact of p is (or A B).            
-            if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
-                m_literals.reset();
-                m_literals.push_back(fact);
-            }
-            else {
-                get_literals(fact);
-            }
-
-            // go over all the literals in the consequence of the lemma
-            for (unsigned i = 0; i < m_literals.size(); ++i) {
-                expr* e = m_literals[i];
-                // if the literal is not in hypothesis, skip it
-                if (!in_hypotheses(e, hyps)) {
-                    m_literals[i] = m_literals.back();
-                    m_literals.pop_back();
-                    --i;
-                }
-                // if the literal is in hypothesis remove it because
-                // it is not in hypothesis set of the lemma
-                // XXX but we assume that lemmas have empty hypothesis set.
-                // XXX eventually every element of new_hyps must be removed!
-                else {
-                    SASSERT(new_hyps);
-                    expr_ref not_e = complement_lit(e);
-                    SASSERT(new_hyps->contains(not_e));
-                    new_hyps->remove(not_e);
-                }
-            }
-            // killed all hypotheses, so can stop at the lemma since
-            // we have a closed pf of false
-            if (m_literals.empty()) {
-                result = tmp;
-            }
-            else {
-                // create a new lemma, but might be re-creating existing one
-                expr_ref clause(m);
-                if (m_literals.size() == 1) {
-                    clause = m_literals[0];
-                }
-                else {
-                    clause = m.mk_or(m_literals.size(), m_literals.c_ptr());
-                }
-                tmp = m.mk_lemma(tmp, clause);
-                m_refs.push_back(tmp);
-                result = tmp;
-            }
-            if (new_hyps && new_hyps->empty()) {
-                dealloc(new_hyps);
-                new_hyps = 0;
-            }
-            m_hypmap.insert(result, new_hyps);
-            // might push 0 into m_hyprefs. No reason for that
-            m_hyprefs.push_back(new_hyps);
-            TRACE("proof_utils",            
-                    tout << "New lemma: " << mk_pp(m.get_fact(p), m) 
-                      << "\n==>\n" 
-                      << mk_pp(m.get_fact(result), m) << "\n";
-                if (hyps) {
-                    expr_set::iterator it = hyps->begin();
-                    expr_set::iterator end = hyps->end();
-                    for (; it != end; ++it) {
-                        tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
-                    }
-                });                               
-            
-            break;
-        }
-        case PR_UNIT_RESOLUTION: {
-            proof_ref_vector parents(m);
-            // get the clause being resolved with
-            parents.push_back(m.get_parent(p, 0));
-            // save state
-            push();
-            bool found_false = false;
-            // for every derivation of a unit literal
-            for (unsigned i = 1; i < m.get_num_parents(p); ++i) {
-                // see if it derives false
-                tmp = m.get_parent(p, i);
-                elim(tmp);
-                if (m.is_false(m.get_fact(tmp))) {
-                    // if derived false, the whole pf is false and we can bail out
-                    result = tmp;
-                    found_false = true;
-                    break;
-                }
-                // -- otherwise, the fact has not changed. nothing to simplify
-                SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
-                parents.push_back(tmp);          
-                // remember that we have this derivation while we have not poped the trail
-                // but only if the proof is closed (i.e., a real unit)
-                if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
-                    m_units.insert(m.get_fact(tmp), tmp);
-                    m_units_trail.push_back(m.get_fact(tmp));
-                }
-            }
-            if (found_false) {
-                pop();
-                break;
-            }
-            // look at the clause being resolved with
-            tmp = m.get_parent(p, 0);
-            // remember its fact
-            expr* old_clause = m.get_fact(tmp);
-            // attempt to reduce its fact
-            elim(tmp);
-            // update parents
-            parents[0] = tmp;
-            // if the new fact is false, bail out
-            expr* clause = m.get_fact(tmp);
-            if (m.is_false(clause)) {
-                m_refs.push_back(tmp);
-                result = tmp;
-                pop();
-                break;
-            }
-            //
-            // case where clause is a literal in the old clause.
-            // i.e., reduce multi-literal clause to a unit
-            //
-            if (is_literal_in_clause(clause, old_clause)) {
-                // if the resulting literal was resolved, get a pf of false and bail out
-                bool found = false;
-                for (unsigned i = 1; !found && i < parents.size(); ++i) {
-                    if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
-                        parents[1] = parents[i].get();
-                        parents.resize(2);
-                        result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
-                        m_refs.push_back(result);               
-                        add_hypotheses(result);
-                        found = true;
-                    }                    
-                }
-                // else if the resulting literal is not resolved, it is the new consequence  
-                if (!found) {
-                    result = parents[0].get();
-                }
-                pop(); 
-                break;
-            }
-            //
-            // case where new clause is a subset of old clause.
-            // the literals in clause should be a subset of literals in old_clause.
-            // 
-            get_literals(clause);
-            for (unsigned i = 1; i < parents.size(); ++i) {
-                bool found = false;
-                for (unsigned j = 0; j < m_literals.size(); ++j) {
-                    if (m.is_complement(m_literals[j], m.get_fact(parents[i].get()))) {
-                        found = true;
-                        break;
-                    }
-                }
-                if (!found) {
-                    // literal was removed as hypothesis.
-                    parents[i] = parents.back();
-                    parents.pop_back();
-                    --i;
-                }
-            }
-            if (parents.size() == 1) {
-                result = parents[0].get();
-            }
-            else {
-                result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
-                m_refs.push_back(result);               
-                add_hypotheses(result);
-            }
-            pop();
-            break;
-        }                
-        default: {
-            ptr_buffer<expr> args;
-            bool change = false;
-            bool found_false = false;
-            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
-                tmp = m.get_parent(p, i);
-                elim(tmp);
-                if (m.is_false(m.get_fact(tmp))) {
-                    result = tmp;
-                    found_false = true;
-                    break;
-                }
-                // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
-                change = change || (tmp != m.get_parent(p, i));
-                args.push_back(tmp);
-            }
-            if (found_false) {
-                break;
-            }
-            if (m.has_fact(p)) {
-                args.push_back(m.get_fact(p));
-            }
-            if (change) {
-                tmp = m.mk_app(p->get_decl(), args.size(), args.c_ptr());
-                m_refs.push_back(tmp);
-            }
-            else {
-                tmp = p;
-            }
-            result = tmp;                
-            add_hypotheses(result);
-            break;
-        }
-        }          
-        SASSERT(m_hypmap.contains(result));
-        m_cache.insert(p, result);
-        p = result;
-    }        
-
-    bool is_literal_in_clause(expr* fml, expr* clause) {
-        if (!m.is_or(clause)) {
-            return false;
-        }
-        app* cl = to_app(clause);
-        for (unsigned i = 0; i < cl->get_num_args(); ++i) {
-            if (cl->get_arg(i) == fml) {
-                return true;
-            }
-        }
-        return false;
-    }
-};
-
-void proof_utils::reduce_hypotheses(proof_ref& pr) {
-    ast_manager& m = pr.get_manager();
-    class reduce_hypotheses0 reduce(m);
-    reduce(pr);
-    CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
-}
-
-class proof_is_closed {
-    ast_manager&     m;
-    ptr_vector<expr> m_literals;
-    ast_mark         m_visit;
-
-    void reset() {
-        m_literals.reset();
-        m_visit.reset();
-    }
-
-    bool check(proof* p) {
-        // really just a partial check because nodes may be visited 
-        // already under a different lemma scope.
-        if (m_visit.is_marked(p)) {
-            return true;
-        }
-        bool result = false;
-        m_visit.mark(p, true);
-        switch(p->get_decl_kind()) {
-        case PR_LEMMA: {
-            unsigned sz = m_literals.size();
-            expr* cls = m.get_fact(p);
-            m_literals.push_back(cls);
-            if (m.is_or(cls)) {
-                m_literals.append(to_app(cls)->get_num_args(), to_app(cls)->get_args());
-            }
-            SASSERT(m.get_num_parents(p) == 1);
-            result = check(m.get_parent(p, 0));
-            m_literals.resize(sz);
-            break;            
-        }
-        case PR_HYPOTHESIS: {
-            expr* fact = m.get_fact(p);
-            for (unsigned i = 0; i < m_literals.size(); ++i) {
-                if (m.is_complement(m_literals[i], fact)) {
-                    result = true;
-                    break;
-                }
-            }
-            break;
-        }
-        default: 
-            result = true;
-            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
-                if (!check(m.get_parent(p, i))) {
-                    result = false;
-                    break;
-                }
-            }
-            break;
-        }
-        
-        return result;
-    }
-    
-public:
-    proof_is_closed(ast_manager& m): m(m) {}
-
-    bool operator()(proof *p) {
-        bool ok = check(p);
-        reset();
-        return ok;
-    }
-};
-
-bool proof_utils::is_closed(ast_manager& m, proof* p) {
-    proof_is_closed checker(m);
-    return checker(p);
-}
-
-
-static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
-    ast_manager& m = pr.get_manager();
-    proof* pr2 = 0;
-    proof_ref_vector parents(m);
-    proof_ref prNew(pr); 
-    if (cache.find(pr, pr2)) {
-        pr = pr2;
-        return;
-    }
-    
-    for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
-        prNew = m.get_parent(pr, i);
-        permute_unit_resolution(refs, cache, prNew);
-        parents.push_back(prNew);
-    }
-    
-    prNew = pr;
-    if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
-        parents[0]->get_decl_kind() == PR_TH_LEMMA) { 
-        /*
-          Unit resolution:
-          T1:      (or l_1 ... l_n l_1' ... l_m')
-          T2:      (not l_1)
-          ...
-          T(n+1):  (not l_n)
-                   [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
-          Th lemma:
-          T1:      (not l_1)
-          ...
-          Tn:      (not l_n)
-          [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
-                    
-          Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
-                    
-          Implement conversion:
-                    
-                 T1 |- not l_1 ... Tn |- not l_n  
-                 -------------------------------  TH_LEMMA
-                          (or k_1 .. k_m j_1 ... j_m)    S1 |- not k_1 ... Sm |- not k_m
-                          -------------------------------------------------------------- UNIT_RESOLUTION
-                                        (or j_1 .. j_m)
-
-
-            |-> 
-
-                    T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
-                    ---------------------------------------------------------------- TH_LEMMA
-                                        (or j_1 .. j_m)
-
-        */
-        proof_ref_vector premises(m);
-        proof* thLemma = parents[0].get();
-        for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
-            premises.push_back(m.get_parent(thLemma, i));
-        }
-        for (unsigned i = 1; i < parents.size(); ++i) {
-            premises.push_back(parents[i].get());
-        }
-        parameter const* params = thLemma->get_decl()->get_parameters();
-        unsigned num_params = thLemma->get_decl()->get_num_parameters();
-        SASSERT(params[0].is_symbol());
-        family_id tid = m.mk_family_id(params[0].get_symbol());
-        SASSERT(tid != null_family_id);
-        // AG: This can break a theory lemma. In particular, for Farkas lemmas the coefficients
-        // AG: for the literals propagated from the unit resolution are missing.
-        // AG: Why is this a good thing to do?
-        // AG: This can lead to merging of the units with other terms in interpolation,
-        // AG: but without farkas coefficients this does not make sense
-        prNew = m.mk_th_lemma(tid, m.get_fact(pr), 
-                              premises.size(), premises.c_ptr(), num_params-1, params+1);
-    }
-    else {
-        ptr_vector<expr> args;
-        for (unsigned i = 0; i < parents.size(); ++i) {
-            args.push_back(parents[i].get());
-        }
-        if (m.has_fact(pr)) {
-            args.push_back(m.get_fact(pr));
-        }
-        prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
-    }    
-    
-    cache.insert(pr, prNew);
-    refs.push_back(prNew);
-    pr = prNew;
-}
-
-
-// permute unit resolution over Theory lemmas to track premises.
-void proof_utils::permute_unit_resolution(proof_ref& pr) {
-    expr_ref_vector refs(pr.get_manager());
-    obj_map<proof,proof*> cache;
-    ::permute_unit_resolution(refs, cache, pr);
-}
-
-class push_instantiations_up_cl {
-    ast_manager& m;
-public:
-    push_instantiations_up_cl(ast_manager& m): m(m) {}
-
-    void operator()(proof_ref& p) {
-        expr_ref_vector s0(m);
-        p = push(p, s0);
-    }
-
-private:
-
-    proof* push(proof* p, expr_ref_vector const& sub) {
-        proof_ref_vector premises(m);
-        expr_ref conclusion(m);
-        svector<std::pair<unsigned, unsigned> >  positions;
-        vector<expr_ref_vector> substs;
-
-        if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
-            for (unsigned i = 0; i < premises.size(); ++i) {
-                compose(substs[i], sub);
-                premises[i] = push(premises[i].get(), substs[i]);
-                substs[i].reset();
-            }
-            instantiate(sub, conclusion);
-            return 
-                m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, 
-                                   positions, 
-                                   substs);
-        }        
-        if (sub.empty()) {
-            return p;
-        }
-        if (m.is_modus_ponens(p)) {
-            SASSERT(m.get_num_parents(p) == 2);
-            proof* p0 = m.get_parent(p, 0);
-            proof* p1 = m.get_parent(p, 1);
-            if (m.get_fact(p0) == m.get_fact(p)) {
-                return push(p0, sub);
-            }
-            expr* e1, *e2;
-            if (m.is_rewrite(p1, e1, e2) && 
-                is_quantifier(e1) && is_quantifier(e2) &&
-                to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
-                expr_ref r1(e1,m), r2(e2,m);
-                instantiate(sub, r1);
-                instantiate(sub, r2);
-                p1 = m.mk_rewrite(r1, r2);
-                return m.mk_modus_ponens(push(p0, sub), p1);
-            }
-        }
-        premises.push_back(p);
-        substs.push_back(sub);
-        conclusion = m.get_fact(p);
-        instantiate(sub, conclusion);
-        return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
-    }
-
-    void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
-        for (unsigned i = 0; i < sub.size(); ++i) {
-            expr_ref e(m);
-            var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
-            sub[i] = e;            
-        }
-    }
-
-    void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
-        if (sub.empty()) {
-            return;
-        }
-        if (!is_forall(fml)) {
-            return;
-        }
-        quantifier* q = to_quantifier(fml);
-        if (q->get_num_decls() != sub.size()) {
-            TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
-                  tout << mk_pp(q, m) << "\n";
-                  tout << sub.size() << "\n";);
-            return;
-        }
-        var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
-    }
-
-};
-
-void proof_utils::push_instantiations_up(proof_ref& pr) {
-    push_instantiations_up_cl push(pr.get_manager());
-    push(pr);
-}
-
-
diff --git a/src/muz/base/proof_utils.h b/src/muz/base/proof_utils.h
deleted file mode 100644
index 0db831c4f..000000000
--- a/src/muz/base/proof_utils.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    proof_utils.h
-
-Abstract:
-
-    Utilities for transforming proofs.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2012-10-12.
-
-Revision History:
-
---*/
-#ifndef PROOF_UTILS_H_
-#define PROOF_UTILS_H_
-
-class proof_utils {
-public:
-    /**
-       \brief reduce the set of hypotheses used in the proof.
-     */
-    static void reduce_hypotheses(proof_ref& pr);
-
-    /**
-       \brief Check that a proof does not contain open hypotheses.
-    */
-    static bool is_closed(ast_manager& m, proof* p);
-
-    /**
-       \brief Permute unit resolution rule with th-lemma
-    */
-    static void permute_unit_resolution(proof_ref& pr);
-
-    /**
-       \brief Push instantiations created in hyper-resolutions up to leaves.
-       This produces a "ground" proof where leaves are annotated by instantiations.
-    */
-    static void push_instantiations_up(proof_ref& pr);
-
-
-};
-
-#endif
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index a1878dc7a..37d80e2d6 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -43,7 +43,6 @@ Notes:
 #include "ast/ast_ll_pp.h"
 #include "ast/proofs/proof_checker.h"
 #include "smt/smt_value_sort.h"
-#include "muz/base/proof_utils.h"
 #include "muz/base/dl_boogie_proof.h"
 #include "ast/scoped_proof.h"
 #include "tactic/core/blast_term_ite_tactic.h"
diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index 4f47cb554..4a77d2f5f 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -31,7 +31,7 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/ast_ll_pp.h"
 #include "tactic/arith/arith_bounds_tactic.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/reg_decl_plugins.h"
 
 
@@ -733,8 +733,8 @@ namespace pdr {
                     }
                     else {
                         expr_set* hyps3 = alloc(expr_set);
-                        datalog::set_union(*hyps3, *hyps);
-                        datalog::set_union(*hyps3, *hyps2);
+                        set_union(*hyps3, *hyps);
+                        set_union(*hyps3, *hyps2);
                         hyps = hyps3;
                         hyprefs.push_back(hyps);
                     }
@@ -795,7 +795,7 @@ namespace pdr {
             case PR_LEMMA: {
                 expr_set* hyps2 = alloc(expr_set);
                 hyprefs.push_back(hyps2);
-                datalog::set_union(*hyps2, *hyps); 
+                set_union(*hyps2, *hyps); 
                 hyps = hyps2;
                 expr* fml = m.get_fact(p);
                 hyps->remove(fml);
diff --git a/src/muz/pdr/pdr_generalizers.cpp b/src/muz/pdr/pdr_generalizers.cpp
index b17d3f8b6..094379a0b 100644
--- a/src/muz/pdr/pdr_generalizers.cpp
+++ b/src/muz/pdr/pdr_generalizers.cpp
@@ -81,7 +81,7 @@ namespace pdr {
         m_gen(n, core0, uses_level1);
         new_cores.push_back(std::make_pair(core0, uses_level1));
         obj_hashtable<expr> core_exprs, core1_exprs;
-        datalog::set_union(core_exprs, core0);
+        set_union(core_exprs, core0);
         for (unsigned i = 0; i < old_core.size(); ++i) {
             expr* lit = old_core[i].get();             
             if (core_exprs.contains(lit)) {
@@ -94,8 +94,8 @@ namespace pdr {
                 if (core1.size() < old_core.size()) {
                     new_cores.push_back(std::make_pair(core1, uses_level1));
                     core1_exprs.reset();
-                    datalog::set_union(core1_exprs, core1);
-                    datalog::set_intersection(core_exprs, core1_exprs);
+                    set_union(core1_exprs, core1);
+                    set_intersection(core_exprs, core1_exprs);
                 }
             }
         }
diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp
index 47bc474ef..d97bee49f 100644
--- a/src/muz/spacer/spacer_farkas_learner.cpp
+++ b/src/muz/spacer/spacer_farkas_learner.cpp
@@ -31,7 +31,7 @@ Revision History:
 #include "muz/spacer/spacer_farkas_learner.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/ast_ll_pp.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/reg_decl_plugins.h"
 #include "smt/smt_farkas_util.h"
 
@@ -231,8 +231,8 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
                     hyps = hyps2;
                 } else {
                     expr_set* hyps3 = alloc(expr_set);
-                    datalog::set_union(*hyps3, *hyps);
-                    datalog::set_union(*hyps3, *hyps2);
+                    set_union(*hyps3, *hyps);
+                    set_union(*hyps3, *hyps2);
                     hyps = hyps3;
                     hyprefs.push_back(hyps);
                 }
@@ -291,7 +291,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
         case PR_LEMMA: {
             expr_set* hyps2 = alloc(expr_set);
             hyprefs.push_back(hyps2);
-            datalog::set_union(*hyps2, *hyps);
+            set_union(*hyps2, *hyps);
             hyps = hyps2;
             expr* fml = m.get_fact(p);
             hyps->remove(fml);
diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index dd2a16abd..679736add 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -25,7 +25,7 @@
 #include "ast/ast_util.h"
 #include "ast/proofs/proof_checker.h"
 #include "smt/smt_value_sort.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/scoped_proof.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "tactic/core/blast_term_ite_tactic.h"