diff --git a/lib/dl_mk_coalesce.cpp b/lib/dl_mk_coalesce.cpp
new file mode 100644
index 000000000..c2ec0adc5
--- /dev/null
+++ b/lib/dl_mk_coalesce.cpp
@@ -0,0 +1,209 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_coalesce.cpp
+
+Abstract:
+
+    Coalesce rules with shared bodies.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-10-15
+
+Revision History:
+
+
+Notes:
+
+ Implements proof rule of the form:
+
+    a(x) & q(x) -> p(x)       b(y) & q(y) -> p(y)
+    ---------------------------------------------
+           (a(z) \/ b(z)) & q(z) -> p(z)
+
+ 
+--*/
+#include "dl_mk_coalesce.h"
+#include "bool_rewriter.h"
+
+namespace datalog {
+
+    mk_coalesce::mk_coalesce(context& ctx):
+        rule_transformer::plugin(50, false),
+        m_ctx(ctx),
+        m(ctx.get_manager()),
+        rm(ctx.get_rule_manager()),
+        m_sub1(m),
+        m_sub2(m),
+        m_idx(0)
+    {}
+
+    void mk_coalesce::mk_pred(app_ref& pred, app* p1, app* p2) {
+        SASSERT(p1->get_decl() == p2->get_decl());
+        unsigned sz = p1->get_num_args();
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* a = p1->get_arg(i);
+            expr* b = p2->get_arg(i);
+            SASSERT(m.get_sort(a) == m.get_sort(b));
+            m_sub1.push_back(a);
+            m_sub2.push_back(b);
+            args.push_back(m.mk_var(m_idx++, m.get_sort(a)));
+        }
+        pred = m.mk_app(p1->get_decl(), args.size(), args.c_ptr());
+    }
+
+    void mk_coalesce::extract_conjs(expr_ref_vector const& sub, rule const& rl, expr_ref& result) {
+        obj_map<expr, unsigned> indices;
+        bool_rewriter bwr(m);
+        rule_ref r(const_cast<rule*>(&rl), rm);
+        sort_ref_vector sorts(m);
+        expr_ref_vector revsub(m), conjs(m);
+        rl.get_vars(sorts);
+        revsub.resize(sorts.size());  
+        svector<bool> valid(sorts.size(), true);
+        for (unsigned i = 0; i < sub.size(); ++i) {
+            expr* e = sub[i];
+            sort* s = m.get_sort(e);
+            expr_ref w(m.mk_var(i, s), m);
+            if (is_var(e)) {
+                unsigned v = to_var(e)->get_idx();
+                SASSERT(v < valid.size());
+                if (sorts[v].get()) {
+                    SASSERT(s == sorts[v].get());
+                    if (valid[v]) {
+                        revsub[v] = w;
+                        valid[v] = false;
+                    }
+                    else {
+                        SASSERT(revsub[v].get());
+                        SASSERT(m.get_sort(revsub[v].get()) == s);
+                        conjs.push_back(m.mk_eq(revsub[v].get(), w));    
+                    }
+                }
+            }
+            else {
+                SASSERT(m.is_value(e));
+                SASSERT(m.get_sort(e) == m.get_sort(w));
+                conjs.push_back(m.mk_eq(e, w));
+            }
+        }
+        for (unsigned i = 0; i < sorts.size(); ++i) {
+            if (valid[i] && sorts[i].get() && !revsub[i].get()) {
+                revsub[i] = m.mk_var(m_idx++, sorts[i].get());
+            }
+        }
+        var_subst vs(m, false);
+        for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) {
+            vs(r->get_tail(i), revsub.size(), revsub.c_ptr(), result);
+            conjs.push_back(result);
+        }
+        bwr.mk_and(conjs.size(), conjs.c_ptr(), result);
+    }
+
+    void mk_coalesce::merge_rules(rule_ref& tgt, rule const& src) {
+        SASSERT(same_body(*tgt.get(), src));
+        m_sub1.reset();
+        m_sub2.reset();
+        m_idx = 0;
+        app_ref pred(m), head(m);
+        expr_ref fml1(m), fml2(m), fml(m);
+        app_ref_vector tail(m);
+        sort_ref_vector sorts1(m), sorts2(m);
+        expr_ref_vector conjs1(m), conjs(m);
+        rule_ref res(rm);
+        bool_rewriter bwr(m);
+        svector<bool> is_neg;
+        tgt->get_vars(sorts1);
+        src.get_vars(sorts2);
+
+        mk_pred(head, src.get_head(), tgt->get_head()); 
+        for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {
+            mk_pred(pred, src.get_tail(i), tgt->get_tail(i));
+            tail.push_back(pred);
+            is_neg.push_back(src.is_neg_tail(i));
+        }           
+        extract_conjs(m_sub1, src, fml1);
+        extract_conjs(m_sub2, *tgt.get(),  fml2);
+        bwr.mk_or(fml1, fml2, fml);
+        SASSERT(is_app(fml));
+        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) {
+            src.to_formula(fml1);
+            tgt->to_formula(fml2);
+            res->to_formula(fml);
+#if 0
+            sort* ps = m.mk_proof_sort();
+            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));
+#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));
+#endif
+        }
+        tgt = res;
+    }
+
+    bool mk_coalesce::same_body(rule const& r1, rule const& r2) const {
+        SASSERT(r1.get_decl() == r2.get_decl());
+        unsigned sz = r1.get_uninterpreted_tail_size();
+        if (sz != r2.get_uninterpreted_tail_size()) {
+            return false;
+        }
+        for (unsigned i = 0; i < sz; ++i) {
+            if (r1.get_decl(i) != r2.get_decl(i)) {
+                return false;
+            }
+            if (r1.is_neg_tail(i) != r2.is_neg_tail(i)) {
+                return false;
+            }
+        }
+        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* rules = alloc(rule_set, m_ctx);
+        rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
+        bool change = false;
+        for (; it != end; ++it) {
+            func_decl* p = it->m_key;
+            rule_ref_vector d_rules(rm);
+            d_rules.append(it->m_value->size(), it->m_value->c_ptr());
+            for (unsigned i = 0; i < d_rules.size(); ++i) {
+                rule_ref r1(d_rules[i].get(), rm);
+                for (unsigned j = i + 1; j < d_rules.size(); ++j) {
+                    if (same_body(*r1.get(), *d_rules[j].get())) {
+                        merge_rules(r1, *d_rules[j].get());
+                        d_rules[j] = d_rules.back();
+                        d_rules.pop_back();
+                        change = true;
+                        --j;
+                    }
+                }
+                rules->add_rule(r1.get());
+            }
+        }
+        if (pc) {
+            pc = concat(pc.get(), rpc.get());
+        }
+        return rules;
+    }
+
+};
+
+
diff --git a/lib/dl_mk_coalesce.h b/lib/dl_mk_coalesce.h
new file mode 100644
index 000000000..4259d31fe
--- /dev/null
+++ b/lib/dl_mk_coalesce.h
@@ -0,0 +1,62 @@
+
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_coalesce.h
+
+Abstract:
+
+    Coalesce rules with shared bodies.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-10-15
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_COALESCE_H_
+#define _DL_MK_COALESCE_H_
+
+#include"dl_context.h"
+#include"dl_rule_set.h"
+#include"uint_set.h"
+#include"dl_rule_transformer.h"
+#include"dl_mk_rule_inliner.h"
+
+namespace datalog {
+
+    /**
+       \brief Implements an unfolding transformation.
+    */
+    class mk_coalesce : public rule_transformer::plugin {
+        context&        m_ctx;
+        ast_manager&    m;
+        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);
+
+        void extract_conjs(expr_ref_vector const& sub, rule const& rl, expr_ref& result);
+
+        bool same_body(rule const& r1, rule const& r2) const;
+
+        void merge_rules(rule_ref& tgt, rule const& src);
+
+    public:
+        /**
+           \brief Create coalesced rules.
+         */
+        mk_coalesce(context & ctx);
+        
+        rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
+    };
+
+};
+
+#endif /* _DL_MK_COALESCE_H_ */
+
diff --git a/lib/dl_mk_unfold.cpp b/lib/dl_mk_unfold.cpp
index 5be9aebe7..d26a0a290 100644
--- a/lib/dl_mk_unfold.cpp
+++ b/lib/dl_mk_unfold.cpp
@@ -21,7 +21,7 @@ Revision History:
 namespace datalog {
 
     mk_unfold::mk_unfold(context& ctx):
-        rule_transformer::plugin(0, false),
+        rule_transformer::plugin(100, false),
         m_ctx(ctx),
         m(ctx.get_manager()),
         rm(ctx.get_rule_manager()),
diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj
index 0206c2741..01a33e4f7 100644
--- a/lib/lib.vcxproj
+++ b/lib/lib.vcxproj
@@ -542,6 +542,7 @@
     <ClCompile Include="dl_costs.cpp" />
     <ClCompile Include="dl_cmds.cpp" />
     <ClCompile Include="dl_decl_plugin.cpp" />
+    <ClCompile Include="dl_mk_coalesce.cpp" />
     <ClCompile Include="dl_mk_coi_filter.cpp" />
     <ClCompile Include="dl_mk_explanations.cpp" />
     <ClCompile Include="dl_mk_partial_equiv.cpp" />
@@ -998,6 +999,7 @@
     <ClInclude Include="diff_logic.h" />
     <ClInclude Include="dl_decl_plugin.h" />
     <ClInclude Include="dl_mk_bit_blast.h" />
+    <ClInclude Include="dl_mk_coalesce.h" />
     <ClInclude Include="dl_mk_slice.h" />
     <ClInclude Include="dl_mk_coi_filter.h" />
     <ClInclude Include="dl_mk_explanations.h" />
diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp
index aba2fe63d..52481bd13 100644
--- a/lib/pdr_dl_interface.cpp
+++ b/lib/pdr_dl_interface.cpp
@@ -31,6 +31,7 @@ Revision History:
 #include "dl_rule_set.h"
 #include "dl_mk_slice.h"
 #include "dl_mk_unfold.h"
+#include "dl_mk_coalesce.h"
 
 using namespace pdr;
 
@@ -120,11 +121,12 @@ lbool dl_interface::query(expr * query) {
 
     if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) {
         unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0);
-        datalog::rule_transformer transformer(m_ctx);
-        datalog::mk_unfold* unfold = alloc(datalog::mk_unfold, m_ctx);
-        transformer.register_plugin(unfold);
+        datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
+        transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+        m_ctx.transform_rules(transformer1, mc, pc);
+        transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
         while (num_unfolds > 0) {
-            m_ctx.transform_rules(transformer, mc, pc);        
+            m_ctx.transform_rules(transformer2, mc, pc);        
             --num_unfolds;
         }
     }