diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 38027efbc..c141e8112 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -325,6 +325,7 @@ namespace qe {
                 }
             }
             fmls.shrink(j);
+            TRACE("qe", tout << "formulas\n" << fmls << "\n";);
 
             // fmls holds residue,
             // mbo holds linear inequalities that are in scope
@@ -380,7 +381,11 @@ namespace qe {
                   }
                   mbo.display(tout););
             vector<opt::model_based_opt::def> defs = mbo.project(real_vars.size(), real_vars.c_ptr(), compute_def);
-            TRACE("qe", mbo.display(tout););
+            TRACE("qe", mbo.display(tout << "mbo result\n");
+                  for (auto const& d : defs) {
+                      tout << "def: " << d << "\n";
+                  }
+                  );
             vector<row> rows;
             mbo.get_live_rows(rows);
             
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index e58f86ba5..cee6e3e8e 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -1442,13 +1442,13 @@ namespace qe {
             for_each_store_proc(imp& i, term_graph& tg) : m_imp(i), tg(tg) {}
 
             void operator()(app* n) {
-                if (m_imp.a.is_array(n) && tg.get_model_based_rep(n)) {
+                if (m_imp.a.is_array(n) && tg.rep_of(n)) {
                     m_imp.add_array(n);
                 }
 
                 if (m_imp.a.is_store(n) &&
-                    (tg.get_model_based_rep(n->get_arg(0)) ||
-                     tg.get_model_based_rep(n->get_arg(n->get_num_args() - 1)))) {
+                    (tg.rep_of(n->get_arg(0)) ||
+                     tg.rep_of(n->get_arg(n->get_num_args() - 1)))) {
                     m_imp.m_stores.push_back(n);
                     for (unsigned i = 1; i + 1 < n->get_num_args(); ++i) {
                         m_imp.add_index_sort(n->get_arg(i));
@@ -1466,7 +1466,7 @@ namespace qe {
 
             void operator()(app* n) {
                 auto* v = m_imp.is_index(n);
-                if (v && tg.get_model_based_rep(n)) {
+                if (v && tg.rep_of(n)) {
                     v->push_back(n);
                 }
             }
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index f6ccf7b7d..a9db391e9 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -117,7 +117,8 @@ namespace qe {
     }
 
     void prop_mbi_plugin::block(expr_ref_vector const& lits) {
-        m_solver->assert_expr(mk_not(mk_and(lits)));
+        expr_ref clause(mk_not(mk_and(lits)), m);
+        m_solver->assert_expr(clause);
     }
 
     // -------------------------------
@@ -171,6 +172,7 @@ namespace qe {
 
     bool uflia_mbi::get_literals(model_ref& mdl, expr_ref_vector& lits) {
         lits.reset();
+        IF_VERBOSE(10, verbose_stream() << "atoms: " << m_atoms << "\n");
         for (expr* e : m_atoms) {
             if (mdl->is_true(e)) {
                 lits.push_back(e);
@@ -204,7 +206,7 @@ namespace qe {
      * 
      *  The result is ordered using deepest term first.
      */
-    app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector& lits) {
+    app_ref_vector uflia_mbi::get_arith_vars(expr_ref_vector const& lits) {
         app_ref_vector avars(m); 
         svector<bool> seen;
         arith_util a(m);
@@ -221,7 +223,7 @@ namespace qe {
             }
         }
         order_avars(avars);
-        TRACE("qe", tout << "vars: " << avars << "\n";);
+        TRACE("qe", tout << "vars: " << avars << " from " << lits << "\n";);
         return avars;
     }
 
@@ -263,14 +265,57 @@ namespace qe {
     */
     void uflia_mbi::project(model_ref& mdl, expr_ref_vector& lits) {
         TRACE("qe", 
-              tout << lits << "\n" << *mdl << "\n";
+              tout << "project literals: " << lits << "\n" << *mdl << "\n";
               tout << m_solver->get_assertions() << "\n";);
 
         add_dcert(mdl, lits);
+        expr_ref_vector alits(m), uflits(m);
+        split_arith(lits, alits, uflits);
         auto avars = get_arith_vars(lits);
-        auto defs = arith_project(mdl, avars, lits);
-        substitute(defs, lits);
-        project_euf(mdl, lits);
+        vector<def> defs = arith_project(mdl, avars, alits);
+        prune_defs(defs);
+        substitute(defs, uflits);
+        project_euf(mdl, uflits);
+        lits.reset();
+        lits.append(alits);
+        lits.append(uflits);
+        IF_VERBOSE(10, verbose_stream() << "projection : " << lits << "\n");
+    }
+
+    void uflia_mbi::split_arith(expr_ref_vector const& lits, 
+                                expr_ref_vector& alits,
+                                expr_ref_vector& uflits) {
+        arith_util a(m);
+        for (expr* lit : lits) {
+            expr* atom = lit, *x = nullptr, *y = nullptr;
+            m.is_not(lit, atom);
+            if (m.is_eq(atom, x, y)) {
+                if (a.is_int_real(x)) {
+                    alits.push_back(lit);
+                }
+                uflits.push_back(lit);
+            }
+            else if (a.is_arith_expr(atom)) {
+                alits.push_back(lit);
+            }
+            else {
+                uflits.push_back(lit);
+            }
+        }
+    }
+
+
+    /**
+     * prune defs to only contain substitutions of terms with leading uninterpreted function.
+     */
+    void uflia_mbi::prune_defs(vector<def>& defs) {
+        unsigned i = 0; 
+        for (auto& d : defs) {
+            if (!is_shared(to_app(d.var)->get_decl())) {
+                defs[i++] = d;
+            }
+        }
+        defs.shrink(i);
     }
 
     /**
@@ -284,8 +329,7 @@ namespace qe {
         term_graph tg(m);
         func_decl_ref_vector shared(m_shared_trail);
         tg.set_vars(shared, false);
-        tg.add_lits(lits);
-        lits.append(tg.get_ackerman_disequalities());
+        lits.append(tg.dcert(*mdl.get(), lits));
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
@@ -293,13 +337,14 @@ namespace qe {
      * \brief substitute solution to arithmetical variables into lits
      */
     void uflia_mbi::substitute(vector<def> const& defs, expr_ref_vector& lits) {
+        TRACE("qe", tout << "start substitute: " << lits << "\n";);
         for (auto const& def : defs) {
             expr_safe_replace rep(m);
             rep.insert(def.var, def.term);
             rep(lits);
+            TRACE("qe", tout << "substitute: " << def.var << " |-> " << def.term << ": " << lits << "\n";);
         }
-        TRACE("qe", tout << "substitute: " << lits << "\n";);
-        IF_VERBOSE(1, verbose_stream() << lits << "\n");
+        IF_VERBOSE(1, verbose_stream() << "substituted: " << lits << "\n");
     }
 
     /**
@@ -333,10 +378,11 @@ namespace qe {
     }
 
     void uflia_mbi::block(expr_ref_vector const& lits) {
-        // want to rely only on atoms from original literals: collect_atoms(lits);
-        expr_ref conj(mk_not(mk_and(lits)), m);
+        expr_ref clause(mk_not(mk_and(lits)), m);
+        collect_atoms(lits);
+        m_fmls.push_back(clause);
         TRACE("qe", tout << "block " << lits << "\n";);
-        m_solver->assert_expr(conj);
+        m_solver->assert_expr(clause);
     }
 
 
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index a693bf493..97875993c 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -120,10 +120,14 @@ namespace qe {
         void order_avars(app_ref_vector& avars);
 
         void add_dcert(model_ref& mdl, expr_ref_vector& lits);
-        app_ref_vector get_arith_vars(expr_ref_vector& lits);
+        app_ref_vector get_arith_vars(expr_ref_vector const& lits);
         vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
         void substitute(vector<def> const& defs, expr_ref_vector& lits);
         void project_euf(model_ref& mdl, expr_ref_vector& lits);
+        void split_arith(expr_ref_vector const& lits, 
+                         expr_ref_vector& alits,
+                         expr_ref_vector& uflits);
+        void prune_defs(vector<def>& defs);
     public:
         uflia_mbi(solver* s, solver* emptySolver);
         ~uflia_mbi() override {}
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index dd631f228..6bfad07d7 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -19,6 +19,7 @@ Notes:
 
 #include "util/util.h"
 #include "util/uint_set.h"
+#include "util/obj_pair_hashtable.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
@@ -217,7 +218,7 @@ namespace qe {
     bool term_graph::is_variable_proc::operator()(const expr * e) const {
         if (!is_app(e)) return false;
         const app *a = ::to_app(e);
-        TRACE("qe", tout << a->get_family_id() << " " << m_solved.contains(a->get_decl()) << " " << m_decls.contains(a->get_decl()) << "\n";);
+        TRACE("qe_verbose", tout << a->get_family_id() << " " << m_solved.contains(a->get_decl()) << " " << m_decls.contains(a->get_decl()) << "\n";);
         return
             a->get_family_id() == null_family_id &&
             !m_solved.contains(a->get_decl()) &&
@@ -1176,56 +1177,95 @@ namespace qe {
 
     }
 
-    expr* term_graph::get_model_based_rep(expr* e) {
+    expr* term_graph::rep_of(expr* e) {
         SASSERT(m_projector);
         term* t = get_term(e);
         SASSERT(t && "only get representatives");
         return m_projector->find_term2app(*t);
     }
-
+    
     expr_ref_vector term_graph::dcert(model& mdl, expr_ref_vector const& lits) {
-#if 0
-        obj_pair_hashtable<expr, expr> diseqs;
-        extract_disequalities(lits, diseqs);
-        svector<std::pair<expr*, expr*>> todo;
-        for (auto const& p : diseqs) todo.push_back(p);
-        expr_ref_vector result(m);
+        TRACE("qe", tout << "dcert " << lits << "\n";);
+        struct pair_t {
+            expr* a, *b;
+            pair_t(): a(nullptr), b(nullptr) {}
+            pair_t(expr* _a, expr* _b):a(_a), b(_b) {
+                if (a->get_id() > b->get_id()) std::swap(a, b);
+            }
+            struct hash {
+                unsigned operator()(pair_t const& p) const { return mk_mix(p.a ? p.a->hash() : 0, p.b ? p.b->hash() : 0, 1); }
+            };
+            struct eq {
+                bool operator()(pair_t const& a, pair_t const& b) const { return a.a == b.a && a.b == b.b; }
+            };
+        };
+        hashtable<pair_t, pair_t::hash, pair_t::eq> diseqs;
+        expr_ref_vector result(m);        
+        add_lits(lits);
+        auto const partitions = get_partition(mdl);
+        svector<pair_t> todo;
+        for (expr* e : lits) {
+            expr* ne, *a, *b;
+            if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) {
+                todo.push_back(pair_t(a, b));
+            }
+            else if (is_uninterp(e)) {
+                todo.push_back(pair_t(e, m.mk_false()));
+            }
+            else if (m.is_not(e, ne) && is_uninterp(ne)) {
+                todo.push_back(pair_t(ne, m.mk_true()));
+            }
+        }
+        for (auto& p : todo) diseqs.insert(p);
+
+        obj_map<expr, unsigned> term2pid;
+        unsigned id = 0;
+        for (auto const& vec : partitions) {
+            for (expr* e : vec) term2pid.insert(e, id);
+            ++id;
+        }
+        auto partition_of = [&](expr* e) { return partitions[term2pid[e]]; }; 
+        auto in_table = [&](expr* a, expr* b) { 
+            return diseqs.contains(pair_t(a, b));
+        };
+        auto same_function = [](expr* a, expr* b) {
+            return is_app(a) && is_app(b) && 
+            to_app(a)->get_decl() == to_app(b)->get_decl() && to_app(a)->get_family_id() == null_family_id;
+        };
 
         // make sure that diseqs is closed under function applications
         // of uninterpreted functions.
         for (unsigned idx = 0; idx < todo.size(); ++idx) {
             auto p = todo[idx];
-            for (app* t1 : partition_of(p.first)) {
-                for (app* t2 : partition_of(p.second)) {
+            for (expr* t1 : partition_of(p.a)) {
+                for (expr* t2 : partition_of(p.b)) {
                     if (same_function(t1, t2)) {
-                        unsigned sz = t1->get_num_args();
+                        unsigned sz = to_app(t1)->get_num_args();
                         bool found = false;
-                        std::pair<expr*, expr*> q(nullptr, nullptr);
+                        pair_t q(t1, t2);
                         for (unsigned i = 0; i < sz; ++i) {
-                            expr* arg1 = t1->get_arg(i);
-                            expr* arg2 = t2->get_arg(i);
+                            expr* arg1 = to_app(t1)->get_arg(i);
+                            expr* arg2 = to_app(t2)->get_arg(i);
                             if (mdl(arg1) == mdl(t2)) {
                                 continue;
                             }
-                            if (in_table(diseqs, arg1, arg2)) {
+                            if (in_table(arg1, arg2)) {
                                 found = true;
                                 break;
                             }
-                            q = make_diseq(arg1, arg2);
+                            q = pair_t(arg1, arg2);
                         }
                         if (!found) {
                             diseqs.insert(q);
                             todo.push_back(q);
-                            result.push_back(m.mk_not(m.mk_eq(q.first, q.second)));
+                            result.push_back(m.mk_not(m.mk_eq(q.a, q.b)));
                         }
                     }
                 }
             }
         }
+        TRACE("qe", tout << result << "\n";);
         return result;
-#endif
-        NOT_IMPLEMENTED_YET();
-        return expr_ref_vector(m);
     }
 
 }
diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h
index 6b0e1c437..c94f18441 100644
--- a/src/qe/qe_term_graph.h
+++ b/src/qe/qe_term_graph.h
@@ -87,7 +87,7 @@ namespace qe {
         void display(std::ostream &out);
 
         bool is_pure_def(expr* atom, expr *& v);
-
+        
     public:
         term_graph(ast_manager &m);
         ~term_graph();
@@ -150,7 +150,7 @@ namespace qe {
          * Map expression that occurs in added literals into representative if it exists.
          */
         void  add_model_based_terms(model& mdl, expr_ref_vector const& terms);
-        expr* get_model_based_rep(expr* e);
+        expr* rep_of(expr* e);
 
     };
 
diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index 8d93a1604..bd2f0fb64 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -336,8 +336,7 @@ namespace sat {
 
     void aig_cuts::init_cut_set(unsigned id) {
         SASSERT(m_aig[id].size() == 1);
-        node const& n = m_aig[id][0];
-        SASSERT(n.is_valid());
+        SASSERT(m_aig[id][0].is_valid());
         auto& cut_set = m_cuts[id];
         reset(cut_set);
         cut_set.init(m_region, m_config.m_max_cutset_size + 1, id);
diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index 3f2017701..703b73941 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -16,7 +16,6 @@
 
   --*/
 
-#include "util/union_find.h"
 #include "sat/sat_aig_simplifier.h"
 #include "sat/sat_xor_finder.h"
 #include "sat/sat_elim_eqs.h"
@@ -231,79 +230,77 @@ namespace sat {
     void aig_simplifier::aig2clauses() {
         vector<cut_set> const& cuts = m_aig_cuts();
         m_stats.m_num_cuts = m_aig_cuts.num_cuts();
-
         add_dont_cares(cuts);
+        cuts2equiv(cuts);
+    }
 
-        map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;
-                
+    void aig_simplifier::cuts2equiv(vector<cut_set> const& cuts) {
+        map<cut const*, unsigned, cut::hash_proc, cut::eq_proc> cut2id;                
+        bool new_eq = false;
         union_find_default_ctx ctx;
-        union_find<> uf(ctx), uf2(ctx);
+        union_find<> uf(ctx);
+
         for (unsigned i = 2*s.num_vars(); i--> 0; ) uf.mk_var();
         auto add_eq = [&](literal l1, literal l2) {
             uf.merge(l1.index(), l2.index());
             uf.merge((~l1).index(), (~l2).index());
+            new_eq = true;
         };
-        bool new_eq = false;
+
         for (unsigned i = cuts.size(); i-- > 0; ) {
+            literal u(i, false);
             for (auto& c : cuts[i]) {
                 unsigned j = 0;
-                if (m_config.m_enable_units && c.is_true()) {
-                    if (s.value(i) == l_undef) {
-                        literal lit(i, false);
-                        // validate_unit(lit);
-                        IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
-                        s.assign_unit(lit);
-                        ++m_stats.m_num_units;
-                    }
-                    break;
-                }
-                if (m_config.m_enable_units && c.is_false()) {
-                    if (s.value(i) == l_undef) {
-                        literal lit(i, true);
-                        // validate_unit(lit);
-                        IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
-                        s.assign_unit(lit);
-                        ++m_stats.m_num_units;
-                    }
-                    break;
-                }
-                if (cut2id.find(&c, j)) {
-                    VERIFY(i != j);
-                    literal u(i, false);
-                    literal v(j, false);
-                    IF_VERBOSE(10,
-                               verbose_stream() << u << " " << c << "\n";
-                               verbose_stream() << v << ": ";
-                               for (cut const& d : cuts[v.var()]) verbose_stream() << d << "\n";);
-
-                    certify_equivalence(u, v, c);                    
-                    //validate_eq(u, v);
-                    add_eq(u, v);
-                    TRACE("aig_simplifier", tout << u << " == " << v << "\n";);                    
-                    new_eq = true;
-                    break;
-                }
-
                 cut nc(c);
                 nc.negate();
-                if (cut2id.find(&nc, j)) {
-                    if (i == j) continue;
-                    literal u(i, false);
-                    literal v(j, true);
-                    certify_equivalence(u, v, c);
-                    // validate_eq(u, v);
-                    add_eq(u, v);
-                    TRACE("aig_simplifier", tout << u << " == " << v << "\n";);
-                    new_eq = true;
-                    break;
+                if (m_config.m_enable_units && c.is_true()) {
+                    assign_unit(u);
+                }
+                else if (m_config.m_enable_units && c.is_false()) {
+                    assign_unit(~u);
+                }
+                else if (cut2id.find(&c, j)) {
+                    literal v(j, false);
+                    assign_equiv(c, u, v);
+                    add_eq(u, v);
+                }
+                else if (cut2id.find(&nc, j)) {
+                    literal v(j, true);
+                    assign_equiv(c, u, v);
+                    add_eq(u, v);
+                }
+                else {
+                    cut2id.insert(&c, i);
                 }
-                cut2id.insert(&c, i);                
             }
         }        
-        if (!new_eq) {
-            return;
+        if (new_eq) {
+            uf2equiv(uf);
         }
-        new_eq = false;
+    }
+
+    void aig_simplifier::assign_unit(literal lit) {
+        if (s.value(lit) == l_undef) {
+            // validate_unit(lit);
+            IF_VERBOSE(2, verbose_stream() << "new unit " << lit << "\n");
+            s.assign_unit(lit);
+            ++m_stats.m_num_units;
+        }
+    }
+
+    void aig_simplifier::assign_equiv(cut const& c, literal u, literal v) {
+        if (u.var() == v.var()) return;
+        IF_VERBOSE(10, verbose_stream() << u << " " << v << " " << c << "\n";);
+        TRACE("aig_simplifier", tout << u << " == " << v << "\n";);                    
+        
+        certify_equivalence(u, v, c);                    
+        //validate_eq(u, v);
+    }
+
+    void aig_simplifier::uf2equiv(union_find<> const& uf) {
+        union_find_default_ctx ctx;
+        union_find<> uf2(ctx);
+        bool new_eq = false;
         for (unsigned i = 2*s.num_vars(); i--> 0; ) uf2.mk_var();
         // extract equivalences over non-eliminated literals.
         for (unsigned idx = 0; idx < uf.get_num_vars(); ++idx) {
@@ -326,11 +323,10 @@ namespace sat {
             }
             while (first != idx);
         }
-        if (!new_eq) {
-            return;
+        if (new_eq) {
+            elim_eqs elim(s);
+            elim(uf2);        
         }
-        elim_eqs elim(s);
-        elim(uf2);        
     }
 
     /**
@@ -396,45 +392,45 @@ namespace sat {
 
     void aig_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
         if (m_config.m_enable_dont_cares) {
-            cuts2pairs(cuts);
-            pairs2dont_cares();
+            cuts2bins(cuts);
+            bins2dont_cares();
             dont_cares2cuts(cuts);
         }
     }
 
     /**
-     * collect pairs of variables that occur in cut sets.
+     * collect binary relations between variables that occur in cut sets.
      */
-    void aig_simplifier::cuts2pairs(vector<cut_set> const& cuts) {
-        svector<var_pair> dcs;
-        for (auto const& p : m_pairs) {
+    void aig_simplifier::cuts2bins(vector<cut_set> const& cuts) {
+        svector<bin_rel> dcs;
+        for (auto const& p : m_bins) {
             if (p.op != none) 
                 dcs.push_back(p);
         }
-        m_pairs.reset();
+        m_bins.reset();
         for (auto const& cs : cuts) {
             for (auto const& c : cs) {
                 for (unsigned i = c.size(); i-- > 0; ) {
                     for (unsigned j = i; j-- > 0; ) {
-                        m_pairs.insert(var_pair(c[j],c[i]));
+                        m_bins.insert(bin_rel(c[j],c[i]));
                     }
                 }
             }
         }
         // don't lose previous don't cares
         for (auto const& p : dcs) {
-            if (m_pairs.contains(p)) 
-                m_pairs.insert(p);
+            if (m_bins.contains(p)) 
+                m_bins.insert(p);
         }
     }
     
     /**
-     * compute masks for pairs.
+     * compute masks for binary relations.
      */
-    void aig_simplifier::pairs2dont_cares() {
+    void aig_simplifier::bins2dont_cares() {
         big b(s.rand());
         b.init(s, true);
-        for (auto& p : m_pairs) {
+        for (auto& p : m_bins) {
             if (p.op != none) continue;
             literal u(p.u, false), v(p.v, false);
             // u -> v, then u & ~v is impossible
@@ -452,8 +448,8 @@ namespace sat {
             }
         }
         IF_VERBOSE(2, {
-                unsigned n = 0; for (auto const& p : m_pairs) if (p.op != none) ++n;
-                verbose_stream() << n << " / " << m_pairs.size() << " don't cares\n";
+                unsigned n = 0; for (auto const& p : m_bins) if (p.op != none) ++n;
+                verbose_stream() << n << " / " << m_bins.size() << " don't cares\n";
             });
     }
 
@@ -476,7 +472,7 @@ namespace sat {
     /*
      * compute masks for position i, j and op-code p.op
      */ 
-    uint64_t aig_simplifier::op2dont_care(unsigned i, unsigned j, var_pair const& p) {
+    uint64_t aig_simplifier::op2dont_care(unsigned i, unsigned j, bin_rel const& p) {
         SASSERT(i < j && j < 6);
         if (p.op == none) return 0ull;
         // first position of mask is offset into output bits contributed by i and j
@@ -496,13 +492,12 @@ namespace sat {
         uint64_t dc = 0;
         for (unsigned i = 0; i < c.size(); ++i) {
             for (unsigned j = i + 1; j < c.size(); ++j) {
-                var_pair p(c[i], c[j]);
-                if (m_pairs.find(p, p) && p.op != none) {
+                bin_rel p(c[i], c[j]);
+                if (m_bins.find(p, p) && p.op != none) {
                     dc |= op2dont_care(i, j, p);
                 }
             }
-        }
-        
+        }        
         return (dc != c.dont_care()) && (c.add_dont_care(dc), true);
     }
 
@@ -525,7 +520,7 @@ namespace sat {
         literal lits1[2] = { a, ~b };
         literal lits2[2] = { ~a, b };
         m_validator->validate(2, lits1);
-        m_validator->validate(2, lits1);
+        m_validator->validate(2, lits2);
     }
 
     
diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h
index 73b27aa67..b6dc58263 100644
--- a/src/sat/sat_aig_simplifier.h
+++ b/src/sat/sat_aig_simplifier.h
@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include "util/union_find.h"
 #include "sat/sat_aig_finder.h"
 #include "sat/sat_aig_cuts.h"
 
@@ -56,6 +57,10 @@ namespace sat {
 
         void clauses2aig();
         void aig2clauses();
+        void cuts2equiv(vector<cut_set> const& cuts);
+        void uf2equiv(union_find<> const& uf);
+        void assign_unit(literal lit);
+        void assign_equiv(cut const& c, literal u, literal v);
         void ensure_validator();
         void validate_unit(literal lit);
         void validate_eq(literal a, literal b);
@@ -63,40 +68,40 @@ namespace sat {
         
         /**
          * collect pairs of literal combinations that are impossible
-         * base on binary implication graph queries.
-         * Apply the masks on cut sets so to allow detecting 
-         * equivalences modulo implications.
+         * base on binary implication graph queries.  Apply the masks
+         * on cut sets so to allow detecting equivalences modulo
+         * implications.
          */
 
         enum op_code { pp, pn, np, nn, none };
 
-        struct var_pair {
+        struct bin_rel {
             unsigned u, v;
             op_code op;
-            var_pair(unsigned _u, unsigned _v): u(_u), v(_v), op(none) {
+            bin_rel(unsigned _u, unsigned _v): u(_u), v(_v), op(none) {
                 if (u > v) std::swap(u, v);
             }
-            var_pair(): u(UINT_MAX), v(UINT_MAX), op(none) {}
+            bin_rel(): u(UINT_MAX), v(UINT_MAX), op(none) {}
 
             struct hash {
-                unsigned operator()(var_pair const& p) const { 
+                unsigned operator()(bin_rel const& p) const { 
                     return mk_mix(p.u, p.v, 1); 
                 }
             };
             struct eq {
-                bool operator()(var_pair const& a, var_pair const& b) const {
+                bool operator()(bin_rel const& a, bin_rel const& b) const {
                     return a.u == b.u && a.v == b.v;
                 }
             };
         };
-        hashtable<var_pair, var_pair::hash, var_pair::eq> m_pairs;
+        hashtable<bin_rel, bin_rel::hash, bin_rel::eq> m_bins;
         
         void add_dont_cares(vector<cut_set> const& cuts);
-        void cuts2pairs(vector<cut_set> const& cuts);
-        void pairs2dont_cares();
+        void cuts2bins(vector<cut_set> const& cuts);
+        void bins2dont_cares();
         void dont_cares2cuts(vector<cut_set> const& cuts);
         bool add_dont_care(cut const & c);
-        uint64_t op2dont_care(unsigned i, unsigned j, var_pair const& p);
+        uint64_t op2dont_care(unsigned i, unsigned j, bin_rel const& p);
 
     public:
         aig_simplifier(solver& s);
diff --git a/src/sat/sat_cutset.cpp b/src/sat/sat_cutset.cpp
index e43c74852..4909198d2 100644
--- a/src/sat/sat_cutset.cpp
+++ b/src/sat/sat_cutset.cpp
@@ -32,7 +32,7 @@ namespace sat {
     */
     
     bool cut_set::insert(on_update_t& on_add, on_update_t& on_del, cut const& c) {
-        unsigned i = 0, j = 0, k = m_size;
+        unsigned i = 0, k = m_size;
         for (; i < k; ++i) {
             cut const& a = (*this)[i];
             if (a.subset_of(c)) {