diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index c506c04e0..88f4f3dd6 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -3,6 +3,7 @@ z3_add_component(sat
     ba_solver.cpp
     dimacs.cpp
     sat_asymm_branch.cpp
+    sat_bdd.cpp
     sat_clause.cpp
     sat_clause_set.cpp
     sat_clause_use_list.cpp
@@ -10,6 +11,7 @@ z3_add_component(sat
     sat_config.cpp
     sat_drat.cpp
     sat_elim_eqs.cpp
+    sat_elim_vars.cpp
     sat_iff3_finder.cpp
     sat_integrity_checker.cpp
     sat_local_search.cpp
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index e0c1b1696..ab2352253 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1288,7 +1288,6 @@ namespace sat {
         if (!create_asserting_lemma()) {
             goto bail_out;
         }
-        active2card();
 
         DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A)););
         
@@ -1347,6 +1346,7 @@ namespace sat {
     }
 
     bool ba_solver::create_asserting_lemma() {
+        bool adjusted = false;
 
     adjust_conflict_level:
         int64 bound64 = m_bound;
@@ -1354,7 +1354,6 @@ namespace sat {
         for (bool_var v : m_active_vars) {
             slack += get_abs_coeff(v);
         }
-
         m_lemma.reset();        
         m_lemma.push_back(null_literal);
         unsigned num_skipped = 0;
@@ -1389,26 +1388,32 @@ namespace sat {
                 }
             }
         }
-
         if (slack >= 0) {
             IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
             return false;
         }
-        
+        if (m_overflow) {
+            return false;
+        }        
         if (m_lemma[0] == null_literal) {
             if (m_lemma.size() == 1) {
                 s().set_conflict(justification());
                 return false;
             }
+            return false;
             unsigned old_level = m_conflict_lvl;
             m_conflict_lvl = 0;
             for (unsigned i = 1; i < m_lemma.size(); ++i) {
                 m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i]));
             }
-            IF_VERBOSE(10, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";);
+            adjusted = true;
             goto adjust_conflict_level;
         }
-        return !m_overflow;
+        if (!adjusted) {
+            active2card();
+        }
+        return true;
     }
 
     /*
@@ -1551,7 +1556,7 @@ namespace sat {
             m_learned.push_back(c);
         }
         else {
-            SASSERT(s().at_base_lvl());
+            SASSERT(!m_solver || s().at_base_lvl());
             m_constraints.push_back(c);
         }
         literal lit = c->lit();
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 3e02d49dc..09903f889 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -362,8 +362,8 @@ namespace sat {
         // access solver
         inline lbool value(bool_var v) const { return value(literal(v, false)); }
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
-        inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }
-        inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); }
+        inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); }
+        inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); }
         inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); }
         inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
         inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp
new file mode 100644
index 000000000..52714eae6
--- /dev/null
+++ b/src/sat/sat_bdd.cpp
@@ -0,0 +1,894 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_bdd.cpp
+
+Abstract:
+
+    Simple BDD package modeled after BuDDy, which is modeled after CUDD.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-13
+
+Revision History:
+
+--*/
+
+#include "sat/sat_bdd.h"
+#include "util/trace.h"
+#include "util/stopwatch.h"
+
+namespace sat {
+
+    bdd_manager::bdd_manager(unsigned num_vars) {
+        m_cost_metric = bdd_cost;
+        m_cost_bdd = 0;
+        for (BDD a = 0; a < 2; ++a) {
+            for (BDD b = 0; b < 2; ++b) {
+                for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) {                
+                    unsigned index = a + 2*b + 4*op;
+                    m_apply_const.reserve(index+1);
+                    m_apply_const[index] = apply_const(a, b, static_cast<bdd_op>(op));
+                }
+            }
+        }
+
+        // add dummy nodes for operations, and true, false bdds.
+        for (unsigned i = 0; i <= bdd_no_op + 2; ++i) {
+            m_nodes.push_back(bdd_node(0,0,0));
+            m_nodes.back().m_refcount = max_rc;
+            m_nodes.back().m_index = m_nodes.size()-1;
+        }
+
+        m_spare_entry = nullptr;
+        m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes
+        m_mark_level = 0;
+        alloc_free_nodes(1024 + num_vars);
+        m_disable_gc = false;
+        m_is_new_node = false;
+        
+        // add variables
+        for (unsigned i = 0; i < num_vars; ++i) {
+            reserve_var(i);
+        }            
+    }
+
+    bdd_manager::~bdd_manager() {
+        if (m_spare_entry) {
+            m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
+        }
+        for (auto* e : m_op_cache) {
+            SASSERT(e != m_spare_entry);
+            m_alloc.deallocate(sizeof(*e), e);
+        }
+    }
+    
+    bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) {
+        SASSERT(is_const(a) && is_const(b));
+        switch (op) {
+        case bdd_and_op:
+            return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd;
+        case bdd_or_op:
+            return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd;
+        case bdd_xor_op:
+            return (a == b) ? false_bdd : true_bdd;
+        default:
+            return false_bdd;
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) {
+        bool first = true;
+        SASSERT(well_formed());
+        while (true) {
+            try {
+                return apply_rec(arg1, arg2, op);
+            }
+            catch (mem_out) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
+        SASSERT(well_formed());
+    }
+
+
+    bdd bdd_manager::mk_true() { return bdd(true_bdd, this); }
+    bdd bdd_manager::mk_false() { return bdd(false_bdd, this); }
+    bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
+    bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
+    bdd bdd_manager::mk_xor(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_xor_op), this); }
+    bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); }
+    bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); }
+
+
+    bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) {
+        if (e1 != e2) {
+            SASSERT(e2->m_result != -1);
+            push_entry(e1);
+            e1 = nullptr;
+            return true;            
+        }
+        else {
+            e1->m_bdd1 = a;
+            e1->m_bdd2 = b;
+            e1->m_op = c;
+            SASSERT(e1->m_result == -1);
+            return false;        
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) {
+        switch (op) {
+        case bdd_and_op:
+            if (a == b) return a;
+            if (is_false(a) || is_false(b)) return false_bdd;
+            if (is_true(a)) return b;
+            if (is_true(b)) return a;
+            break;
+        case bdd_or_op:
+            if (a == b) return a;
+            if (is_false(a)) return b;
+            if (is_false(b)) return a;
+            if (is_true(a) || is_true(b)) return true_bdd;
+            break;
+        case bdd_xor_op:
+            if (a == b) return false_bdd;
+            if (is_false(a)) return b;
+            if (is_false(b)) return a;
+            break;
+        default:
+            UNREACHABLE();
+            break;
+        }
+        if (is_const(a) && is_const(b)) {
+            return m_apply_const[a + 2*b + 4*op];
+        }
+        op_entry * e1 = pop_entry(a, b, op);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+        if (check_result(e1, e2, a, b, op)) {
+            SASSERT(!m_free_nodes.contains(e2->m_result));
+            return e2->m_result;
+        }
+        // SASSERT(well_formed());
+        BDD r;
+        if (level(a) == level(b)) {
+            push(apply_rec(lo(a), lo(b), op));
+            push(apply_rec(hi(a), hi(b), op));
+            r = make_node(level(a), read(2), read(1));
+        }
+        else if (level(a) > level(b)) {
+            push(apply_rec(lo(a), b, op));
+            push(apply_rec(hi(a), b, op));
+            r = make_node(level(a), read(2), read(1));
+        }
+        else {
+            push(apply_rec(a, lo(b), op));
+            push(apply_rec(a, hi(b), op));
+            r = make_node(level(b), read(2), read(1));
+        }
+        pop(2);
+        e1->m_result = r;
+        // SASSERT(well_formed());
+        SASSERT(!m_free_nodes.contains(r));
+        return r;
+    }
+
+    void bdd_manager::push(BDD b) {
+        m_bdd_stack.push_back(b);
+    }
+
+    void bdd_manager::pop(unsigned num_scopes) {
+        m_bdd_stack.shrink(m_bdd_stack.size() - num_scopes);
+    }
+
+    bdd_manager::BDD bdd_manager::read(unsigned index) {
+        return m_bdd_stack[m_bdd_stack.size() - index];
+    }
+
+    bdd_manager::op_entry* bdd_manager::pop_entry(BDD l, BDD r, BDD op) {
+        op_entry* result = nullptr;
+        if (m_spare_entry) {
+            result = m_spare_entry;
+            m_spare_entry = nullptr;
+            result->m_bdd1 = l;
+            result->m_bdd2 = r;
+            result->m_op = op;
+        }
+        else {
+            void * mem = m_alloc.allocate(sizeof(op_entry));
+            result = new (mem) op_entry(l, r, op);
+        }
+        result->m_result = -1;
+        return result;
+    }
+
+    void bdd_manager::push_entry(op_entry* e) {
+        SASSERT(!m_spare_entry);
+        m_spare_entry = e;
+    }
+
+    bdd_manager::BDD bdd_manager::make_node(unsigned lvl, BDD l, BDD h) {
+        m_is_new_node = false;
+        if (l == h) {
+            return l;
+        }
+        SASSERT(is_const(l) || level(l) < lvl);
+        SASSERT(is_const(h) || level(h) < lvl);
+
+        bdd_node n(lvl, l, h);
+        node_table::entry* e = m_node_table.insert_if_not_there2(n);
+        if (e->get_data().m_index != 0) {
+            unsigned result = e->get_data().m_index;
+            return result;
+        }
+        e->get_data().m_refcount = 0;
+        bool do_gc = m_free_nodes.empty();
+        if (do_gc && !m_disable_gc) {
+            gc();
+            e = m_node_table.insert_if_not_there2(n);
+            e->get_data().m_refcount = 0;
+        }
+        if (do_gc && m_free_nodes.size()*3 < m_nodes.size()) {
+            if (m_nodes.size() > m_max_num_bdd_nodes) {
+                throw mem_out();
+            }
+            alloc_free_nodes(m_nodes.size()/2);
+        }
+
+        SASSERT(!m_free_nodes.empty());
+        unsigned result = m_free_nodes.back();
+        m_free_nodes.pop_back();
+        e->get_data().m_index = result;
+        m_nodes[result] = e->get_data();
+        m_is_new_node = true;        
+        SASSERT(!m_free_nodes.contains(result));
+        SASSERT(m_nodes[result].m_index == result); 
+        return result;
+    }
+
+    void bdd_manager::try_cnf_reorder(bdd const& b) {
+        m_cost_bdd = b.root;
+        m_cost_metric = cnf_cost;
+        try_reorder();
+        m_cost_metric = bdd_cost;
+        m_cost_bdd = 0;
+    }    
+
+    void bdd_manager::try_reorder() {
+        gc();        
+        for (auto* e : m_op_cache) {
+            m_alloc.deallocate(sizeof(*e), e);
+        }
+        m_op_cache.reset();
+        init_reorder();
+        for (unsigned i = 0; i < m_var2level.size(); ++i) {
+            sift_var(i);
+        }
+        SASSERT(m_op_cache.empty());
+        SASSERT(well_formed());
+    }
+
+    double bdd_manager::current_cost() {
+        switch (m_cost_metric) {
+        case bdd_cost: 
+            return m_nodes.size() - m_free_nodes.size();
+        case cnf_cost:
+            return cnf_size(m_cost_bdd);
+        case dnf_cost:
+            return dnf_size(m_cost_bdd);
+        default:
+            UNREACHABLE();
+            return 0;
+        }
+    }
+
+    bool bdd_manager::is_bad_cost(double current_cost, double best_cost) const {
+        return current_cost > 1.1 * best_cost;
+    }
+
+    void bdd_manager::sift_var(unsigned v) {
+        unsigned lvl = m_var2level[v];
+        unsigned start = lvl;
+        double best_cost = current_cost();
+        bool first = true;
+        unsigned max_lvl = m_level2nodes.size()-1;
+        if (lvl*2 < max_lvl) {
+            goto go_down;
+        }
+    go_up:
+        TRACE("bdd", tout << "sift up " << lvl << "\n";);
+        while (lvl < max_lvl) {
+            sift_up(lvl++);
+            double cost = current_cost();
+            if (is_bad_cost(cost, best_cost)) break;
+            best_cost = std::min(cost, best_cost);
+        }
+        if (first) {
+            first = false;
+            while (lvl != start) {
+                sift_up(--lvl);
+            }
+            goto go_down;
+        }
+        else {
+            while (current_cost() != best_cost) {
+                sift_up(--lvl);
+            }
+            return;
+        }
+    go_down:
+        TRACE("bdd", tout << "sift down " << lvl << "\n";);
+        while (lvl > 0) {
+            sift_up(--lvl);
+            double cost = current_cost();
+            if (is_bad_cost(cost, best_cost)) break;
+            best_cost = std::min(cost, best_cost);
+        }
+        if (first) {
+            first = false;
+            while (lvl != start) {
+                sift_up(lvl++);
+            }
+            goto go_up;
+        }
+        else {
+            while (current_cost() != best_cost) {
+                sift_up(lvl++);
+            }
+            return;
+        }
+    }
+
+    void bdd_manager::sift_up(unsigned lvl) {
+        if (m_level2nodes[lvl].empty()) return;
+        // SASSERT(well_formed());
+        // exchange level and level + 1.
+        m_S.reset();
+        m_T.reset();
+        m_to_free.reset();
+        m_disable_gc = true;
+
+        for (unsigned n : m_level2nodes[lvl + 1]) {
+            BDD l = lo(n);
+            BDD h = hi(n);
+            if (l == 0 && h == 0) continue;
+            if ((is_const(l) || level(l) != lvl) &&
+                (is_const(h) || level(h) != lvl)) {
+                m_S.push_back(n);
+            }
+            else {
+                reorder_decref(l);            
+                reorder_decref(h);            
+                m_T.push_back(n);
+            }
+            TRACE("bdd", tout << "remove " << n << "\n";);
+            m_node_table.remove(m_nodes[n]);
+        }
+        m_level2nodes[lvl + 1].reset();
+        m_level2nodes[lvl + 1].append(m_T);
+
+        for (unsigned n : m_level2nodes[lvl]) {
+            bdd_node& node = m_nodes[n];
+            m_node_table.remove(node);
+            node.m_level = lvl + 1;
+            if (m_reorder_rc[n] == 0) {
+                m_to_free.push_back(n);
+            }
+            else {
+                TRACE("bdd", tout << "set level " << n << " to " << lvl + 1 << "\n";);
+                m_node_table.insert(node);
+                m_level2nodes[lvl + 1].push_back(n);
+            }
+        }
+        m_level2nodes[lvl].reset();
+        m_level2nodes[lvl].append(m_S);
+    
+        for (unsigned n : m_S) {
+            m_nodes[n].m_level = lvl;
+            m_node_table.insert(m_nodes[n]);
+        }
+
+        for (unsigned n : m_T) {
+            BDD l = lo(n);
+            BDD h = hi(n);
+            if (l == 0 && h == 0) continue;
+            BDD a, b, c, d;
+            if (level(l) == lvl + 1) { 
+                a = lo(l);
+                b = hi(l);
+            }
+            else {
+                a = b = l;
+            }
+            if (level(h) == lvl + 1) { 
+                c = lo(h);
+                d = hi(h);
+            }
+            else {
+                c = d = h;
+            }
+
+            unsigned ac = make_node(lvl, a, c);
+            if (is_new_node()) {
+                m_level2nodes[lvl].push_back(ac);
+                m_reorder_rc.reserve(ac+1);
+                reorder_incref(a);
+                reorder_incref(c);
+            }
+            unsigned bd = make_node(lvl, b, d);
+            if (is_new_node()) {
+                m_level2nodes[lvl].push_back(bd);
+                m_reorder_rc.reserve(bd+1);
+                reorder_incref(b);
+                reorder_incref(d);
+            }
+            m_nodes[n].m_lo = ac;
+            m_nodes[n].m_hi = bd;
+            reorder_incref(ac);
+            reorder_incref(bd);
+            TRACE("bdd", tout << "transform " << n << " " << " " << a << " " << b << " " << c << " " << d << " " << ac << " " << bd << "\n";);
+            m_node_table.insert(m_nodes[n]);
+        }
+        unsigned v = m_level2var[lvl];
+        unsigned w = m_level2var[lvl+1];
+        std::swap(m_level2var[lvl], m_level2var[lvl+1]);
+        std::swap(m_var2level[v], m_var2level[w]);
+        m_disable_gc = false;
+
+        // add orphaned nodes to free-list
+        for (unsigned i = 0; i < m_to_free.size(); ++i) {
+            unsigned n = m_to_free[i];
+            bdd_node& node = m_nodes[n];
+            if (!node.is_internal()) {
+                SASSERT(!m_free_nodes.contains(n));
+                SASSERT(node.m_refcount == 0);
+                m_free_nodes.push_back(n);
+                m_node_table.remove(node);
+                BDD l = lo(n);
+                BDD h = hi(n);
+                node.set_internal();
+
+                reorder_decref(l);
+                if (!m_nodes[l].is_internal() && m_reorder_rc[l] == 0) {
+                    m_to_free.push_back(l);
+                }
+                reorder_decref(h);
+                if (!m_nodes[h].is_internal() && m_reorder_rc[h] == 0) {
+                    m_to_free.push_back(h);
+                }
+            }
+        }
+        TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); );
+        DEBUG_CODE(
+            for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
+                for (unsigned n : m_level2nodes[i]) {
+                    bdd_node const& node = m_nodes[n];
+                    SASSERT(node.m_level == i);
+                }
+            });
+        
+        TRACE("bdd", 
+              for (unsigned i = 0; i < m_nodes.size(); ++i) {
+                if (m_reorder_rc[i] != 0) {
+                    tout << i << " " << m_reorder_rc[i] << "\n";
+                }});
+        
+        // SASSERT(well_formed());
+    }
+
+    void bdd_manager::init_reorder() {
+        m_level2nodes.reset();
+        unsigned sz = m_nodes.size();
+        m_reorder_rc.fill(sz, 0);
+        for (unsigned i = 0; i < sz; ++i) {
+            if (m_nodes[i].m_refcount > 0) 
+                m_reorder_rc[i] = UINT_MAX;
+        }
+        for (unsigned i = 0; i < sz; ++i) {
+            bdd_node const& n = m_nodes[i];
+            if (n.is_internal()) continue;
+            unsigned lvl = n.m_level;
+            SASSERT(i == m_nodes[i].m_index);
+            m_level2nodes.reserve(lvl + 1);
+            m_level2nodes[lvl].push_back(i);
+            reorder_incref(n.m_lo);
+            reorder_incref(n.m_hi);
+        }
+        TRACE("bdd",
+              display(tout);
+              for (unsigned i = 0; i < sz; ++i) {
+                  bdd_node const& n = m_nodes[i];
+                  if (n.is_internal()) continue;
+                  unsigned lvl = n.m_level;
+                  tout << i << " lvl: " << lvl << " rc: " << m_reorder_rc[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n";
+              }
+              );
+    }
+
+    void bdd_manager::reorder_incref(unsigned n) {
+        if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]++;
+    }
+
+    void bdd_manager::reorder_decref(unsigned n) {
+        if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]--;
+    }
+
+    void bdd_manager::reserve_var(unsigned i) {
+        while (m_var2level.size() <= i) {
+            unsigned v = m_var2level.size();
+            m_var2bdd.push_back(make_node(v, false_bdd, true_bdd));
+            m_var2bdd.push_back(make_node(v, true_bdd, false_bdd));
+            m_nodes[m_var2bdd[2*v]].m_refcount = max_rc;
+            m_nodes[m_var2bdd[2*v+1]].m_refcount = max_rc;
+            m_var2level.push_back(v);
+            m_level2var.push_back(v);
+        }
+    }
+
+    bdd bdd_manager::mk_var(unsigned i) {
+        reserve_var(i);
+        return bdd(m_var2bdd[2*i], this);        
+    }
+
+    bdd bdd_manager::mk_nvar(unsigned i) {
+        reserve_var(i);
+        return bdd(m_var2bdd[2*i+1], this);
+    }
+
+    bdd bdd_manager::mk_not(bdd b) {
+        bool first = true;
+        while (true) {
+            try {
+                return bdd(mk_not_rec(b.root), this);
+            }
+            catch (mem_out) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::mk_not_rec(BDD b) {
+        if (is_true(b)) return false_bdd;
+        if (is_false(b)) return true_bdd;
+        op_entry* e1 = pop_entry(b, b, bdd_not_op);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+        if (check_result(e1, e2, b, b, bdd_not_op)) 
+            return e2->m_result;
+        push(mk_not_rec(lo(b)));
+        push(mk_not_rec(hi(b)));
+        BDD r = make_node(level(b), read(2), read(1));
+        pop(2);
+        e1->m_result = r;
+        return r;
+    }
+    
+    bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) {         
+        bool first = true;
+        while (true) {
+            try {
+                return bdd(mk_ite_rec(c.root, t.root, e.root), this); 
+            }
+            catch (mem_out) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) {
+        if (is_true(a)) return b;
+        if (is_false(a)) return c;
+        if (b == c) return b;
+        if (is_true(b)) return apply(a, c, bdd_or_op);
+        if (is_false(c)) return apply(a, b, bdd_and_op);
+        if (is_false(b)) return apply(mk_not_rec(a), c, bdd_and_op);
+        if (is_true(c)) return apply(mk_not_rec(a), b, bdd_or_op);
+        SASSERT(!is_const(a) && !is_const(b) && !is_const(c));
+        op_entry * e1 = pop_entry(a, b, c);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+        if (check_result(e1, e2, a, b, c)) 
+            return e2->m_result;
+        unsigned la = level(a), lb = level(b), lc = level(c);
+        BDD r;
+        BDD a1, b1, c1, a2, b2, c2;
+        unsigned lvl = la;
+        if (la >= lb && la >= lc) {
+            a1 = lo(a), a2 = hi(a);
+            lvl = la;
+        }
+        else {
+            a1 = a, a2 = a;
+        }
+        if (lb >= la && lb >= lc) {
+            b1 = lo(b), b2 = hi(b);
+            lvl = lb;
+        }
+        else {
+            b1 = b, b2 = b;
+        }
+        if (lc >= la && lc >= lb) {
+            c1 = lo(c), c2 = hi(c);
+            lvl = lc;
+        }
+        else {
+            c1 = c, c2 = c;
+        }
+        push(mk_ite_rec(a1, b1, c1));
+        push(mk_ite_rec(a2, b2, c2));
+        r = make_node(lvl, read(2), read(1));
+        pop(2);          
+        e1->m_result = r;
+        return r;
+    }
+
+    bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) {
+        // SASSERT(well_formed());
+        return bdd(mk_quant(n, vars, b.root, bdd_or_op), this);
+    }
+
+    bdd bdd_manager::mk_forall(unsigned n, unsigned const* vars, bdd const& b) {
+        return bdd(mk_quant(n, vars, b.root, bdd_and_op), this);
+    }
+
+    bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) {
+        BDD result = b;
+        for (unsigned i = 0; i < n; ++i) {
+            result = mk_quant_rec(m_var2level[vars[i]], result, op);
+        }
+        return result;
+    }
+
+    bdd_manager::BDD bdd_manager::mk_quant_rec(unsigned l, BDD b, bdd_op op) {
+        unsigned lvl = level(b);
+        BDD r;
+        if (is_const(b)) {
+            r = b;
+        }
+        else if (lvl == l) {
+            r = apply(lo(b), hi(b), op);
+        }
+        else if (lvl < l) {
+            r = b;
+        }
+        else {
+            BDD a = level2bdd(l);
+            bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op;
+            op_entry * e1 = pop_entry(a, b, q_op);
+            op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+            if (check_result(e1, e2, a, b, q_op)) {
+                r = e2->m_result;
+            }
+            else {
+                SASSERT(e1->m_result == -1);
+                push(mk_quant_rec(l, lo(b), op));
+                push(mk_quant_rec(l, hi(b), op));
+                r = make_node(lvl, read(2), read(1));
+                pop(2);
+                e1->m_result = r;
+            }
+        }
+        SASSERT(r != UINT_MAX);
+        return r;
+    }
+
+    double bdd_manager::count(BDD b, unsigned z) {
+        init_mark();
+        m_count.resize(m_nodes.size());
+        m_count[0] = z;
+        m_count[1] = 1-z;
+        set_mark(0);
+        set_mark(1);
+        m_todo.push_back(b);
+        while (!m_todo.empty()) {
+            BDD r = m_todo.back();
+            if (is_marked(r)) {
+                m_todo.pop_back();
+            }
+            else if (!is_marked(lo(r))) {
+                SASSERT (is_const(r) || r != lo(r));
+                m_todo.push_back(lo(r));
+            }
+            else if (!is_marked(hi(r))) {
+                SASSERT (is_const(r) || r != hi(r));
+                m_todo.push_back(hi(r));
+            }
+            else {
+                m_count[r] = m_count[lo(r)] + m_count[hi(r)];
+                set_mark(r);
+                m_todo.pop_back();
+            }
+        }
+        return m_count[b];
+    }
+
+    unsigned bdd_manager::bdd_size(bdd const& b) {
+        init_mark();
+        set_mark(0);
+        set_mark(1);
+        unsigned sz = 0;
+        m_todo.push_back(b.root);
+        while (!m_todo.empty()) {
+            BDD r = m_todo.back();
+            m_todo.pop_back();
+            if (!is_marked(r)) {
+                ++sz;
+                set_mark(r);
+                if (!is_marked(lo(r))) {
+                    m_todo.push_back(lo(r));
+                }
+                if (!is_marked(hi(r))) {
+                    m_todo.push_back(hi(r));
+                }
+            }
+        }
+        return sz;
+    }
+
+    void bdd_manager::alloc_free_nodes(unsigned n) {
+        for (unsigned i = 0; i < n; ++i) {
+            m_free_nodes.push_back(m_nodes.size());
+            m_nodes.push_back(bdd_node());
+            m_nodes.back().m_index = m_nodes.size() - 1;
+        }
+        m_free_nodes.reverse();
+    }
+
+    void bdd_manager::gc() {
+        m_free_nodes.reset();
+        IF_VERBOSE(3, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";);
+        svector<bool> reachable(m_nodes.size(), false);
+        for (unsigned i = m_bdd_stack.size(); i-- > 0; ) {
+            reachable[m_bdd_stack[i]] = true;
+            m_todo.push_back(m_bdd_stack[i]);
+        }
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (m_nodes[i].m_refcount > 0) {
+                reachable[i] = true;
+                m_todo.push_back(i);
+            }
+        }
+        while (!m_todo.empty()) {
+            BDD b = m_todo.back();
+            m_todo.pop_back();
+            SASSERT(reachable[b]);
+            if (is_const(b)) continue;
+            if (!reachable[lo(b)]) {
+                reachable[lo(b)] = true;
+                m_todo.push_back(lo(b));
+            }
+            if (!reachable[hi(b)]) {
+                reachable[hi(b)] = true;
+                m_todo.push_back(hi(b));
+            }
+        }
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (!reachable[i]) {
+                m_nodes[i].set_internal();
+                SASSERT(m_nodes[i].m_refcount == 0);
+                m_free_nodes.push_back(i);                
+            }
+        }
+        // sort free nodes so that adjacent nodes are picked in order of use
+        std::sort(m_free_nodes.begin(), m_free_nodes.end());
+        m_free_nodes.reverse();
+
+        ptr_vector<op_entry> to_delete, to_keep;
+        for (auto* e : m_op_cache) {            
+            if (e->m_result != -1) {
+                to_delete.push_back(e);
+            }
+            else {
+                to_keep.push_back(e);
+            }
+        }
+        m_op_cache.reset();
+        for (op_entry* e : to_delete) {
+            m_alloc.deallocate(sizeof(*e), e);
+        }
+        for (op_entry* e : to_keep) {
+            m_op_cache.insert(e);
+        }
+
+        m_node_table.reset();
+        // re-populate node cache
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (reachable[i]) {
+                SASSERT(m_nodes[i].m_index == i);
+                m_node_table.insert(m_nodes[i]);
+            }
+        }
+        SASSERT(well_formed());
+    }
+
+    void bdd_manager::init_mark() {
+        m_mark.resize(m_nodes.size());
+        ++m_mark_level;
+        if (m_mark_level == 0) {
+            m_mark.fill(0);
+            ++m_mark_level;
+        }
+    }
+
+    std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) {
+        init_mark();
+        m_todo.push_back(b.root);
+        m_reorder_rc.reserve(m_nodes.size());
+        while (!m_todo.empty()) {
+            BDD r = m_todo.back();
+            if (is_marked(r)) {
+                m_todo.pop_back();
+            }
+            else if (lo(r) == 0 && hi(r) == 0) {
+                set_mark(r);
+                m_todo.pop_back();
+            }
+            else if (!is_marked(lo(r))) {
+                m_todo.push_back(lo(r));
+            }
+            else if (!is_marked(hi(r))) {
+                m_todo.push_back(hi(r));
+            }
+            else {
+                out << r << " : " << var(r) << " @ " << level(r) << " " << lo(r) << " " << hi(r) << " " << m_reorder_rc[r] << "\n";
+                set_mark(r);
+                m_todo.pop_back();
+            }
+        }
+        return out;
+    }
+
+    bool bdd_manager::well_formed() {
+        bool ok = true;
+        for (unsigned n : m_free_nodes) {
+            ok &= (lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0);
+            if (!ok) {
+                IF_VERBOSE(0, 
+                           verbose_stream() << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n";
+                           display(verbose_stream()););
+                UNREACHABLE();
+                return false;
+            }
+        }
+        for (bdd_node const& n : m_nodes) {
+            if (n.is_internal()) continue;
+            unsigned lvl = n.m_level;
+            BDD lo = n.m_lo;
+            BDD hi = n.m_hi;
+            ok &= is_const(lo) || level(lo) < lvl;
+            ok &= is_const(hi) || level(hi) < lvl;
+            ok &= is_const(lo) || !m_nodes[lo].is_internal();
+            ok &= is_const(hi) || !m_nodes[hi].is_internal();
+            if (!ok) {
+                IF_VERBOSE(0, display(verbose_stream() << n.m_index << " lo " << lo << " hi " << hi << "\n"););
+                UNREACHABLE();
+                return false;
+            }
+        }
+        return ok;
+    }
+
+    std::ostream& bdd_manager::display(std::ostream& out) {
+        m_reorder_rc.reserve(m_nodes.size());
+        for (unsigned i = 0; i < m_nodes.size(); ++i) {
+            bdd_node const& n = m_nodes[i];
+            if (n.is_internal()) continue;
+            out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << " rc " << m_reorder_rc[i] << "\n";
+        }
+        for (unsigned i = 0; i < m_level2nodes.size(); ++i) {
+            out << "level: " << i << " : " << m_level2nodes[i] << "\n";
+        }
+        return out;
+    }
+
+    bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; }
+    std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
+
+}
diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h
new file mode 100644
index 000000000..41d1115b9
--- /dev/null
+++ b/src/sat/sat_bdd.h
@@ -0,0 +1,258 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_bdd
+
+Abstract:
+
+    Simple BDD package modeled after BuDDy, which is modeled after CUDD.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-13
+
+Revision History:
+
+--*/
+#ifndef SAT_BDD_H_
+#define SAT_BDD_H_
+
+#include "util/vector.h"
+#include "util/map.h"
+#include "util/small_object_allocator.h"
+
+namespace sat {
+
+    class bdd;
+
+    class bdd_manager {
+        friend bdd;
+
+        typedef unsigned BDD;
+
+        enum bdd_op {
+            bdd_and_op = 2,
+            bdd_or_op = 3,
+            bdd_xor_op = 4,
+            bdd_not_op = 5,
+            bdd_and_proj_op = 6,
+            bdd_or_proj_op = 7,
+            bdd_no_op = 8,
+        };
+
+        struct bdd_node {
+            bdd_node(unsigned level, BDD lo, BDD hi):
+                m_refcount(0),
+                m_level(level),
+                m_lo(lo),
+                m_hi(hi),
+                m_index(0)
+            {}
+            bdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {}
+            unsigned m_refcount : 10;
+            unsigned m_level : 22;
+            BDD      m_lo;
+            BDD      m_hi;
+            unsigned m_index;
+            unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); }
+            bool is_internal() const { return m_lo == 0 && m_hi == 0; }
+            void set_internal() { m_lo = 0; m_hi = 0; }
+        };
+
+        enum cost_metric {
+            cnf_cost,
+            dnf_cost,
+            bdd_cost
+        };
+
+        struct hash_node {
+            unsigned operator()(bdd_node const& n) const { return n.hash(); }
+        };
+
+        struct eq_node {
+            bool operator()(bdd_node const& a, bdd_node const& b) const {
+                return a.m_lo == b.m_lo && a.m_hi == b.m_hi && a.m_level == b.m_level;
+            }
+        };
+        
+        typedef hashtable<bdd_node, hash_node, eq_node> node_table;
+
+        struct op_entry {
+            op_entry(BDD l, BDD r, BDD op):
+                m_bdd1(l),
+                m_bdd2(r),
+                m_op(op),
+                m_result(0)
+            {}
+
+            BDD      m_bdd1;
+            BDD      m_bdd2;
+            BDD      m_op;
+            BDD      m_result;
+            unsigned hash() const { return mk_mix(m_bdd1, m_bdd2, m_op); }
+        };
+
+        struct hash_entry {
+            unsigned operator()(op_entry* e) const { return e->hash(); }
+        };
+
+        struct eq_entry {
+            bool operator()(op_entry * a, op_entry * b) const { 
+                return a->m_bdd1 == b->m_bdd2 && a->m_bdd2 == b->m_bdd2 && a->m_op == b->m_op;
+            }
+        };
+
+        typedef ptr_hashtable<op_entry, hash_entry, eq_entry> op_table;
+
+        svector<bdd_node>          m_nodes;
+        op_table                   m_op_cache;
+        node_table                 m_node_table;
+        unsigned_vector            m_apply_const;
+        svector<BDD>               m_bdd_stack;
+        op_entry*                  m_spare_entry;
+        svector<BDD>               m_var2bdd;
+        unsigned_vector            m_var2level, m_level2var;
+        unsigned_vector            m_free_nodes;
+        small_object_allocator     m_alloc;
+        mutable svector<unsigned>  m_mark;
+        mutable unsigned           m_mark_level;
+        mutable svector<double>    m_count;
+        mutable svector<BDD>       m_todo;
+        bool                       m_disable_gc;
+        bool                       m_is_new_node;
+        unsigned                   m_max_num_bdd_nodes;
+        unsigned_vector            m_S, m_T, m_to_free;  // used for reordering
+        vector<unsigned_vector>    m_level2nodes;
+        unsigned_vector            m_reorder_rc;
+        cost_metric                m_cost_metric;
+        BDD                        m_cost_bdd;
+
+        BDD make_node(unsigned level, BDD l, BDD r);
+        bool is_new_node() const { return m_is_new_node; }
+
+        BDD apply_const(BDD a, BDD b, bdd_op op);
+        BDD apply(BDD arg1, BDD arg2, bdd_op op);
+        BDD mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op);
+
+        BDD apply_rec(BDD arg1, BDD arg2, bdd_op op);
+        BDD mk_not_rec(BDD b);
+        BDD mk_ite_rec(BDD a, BDD b, BDD c);
+        BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op);
+
+        void push(BDD b);
+        void pop(unsigned num_scopes);
+        BDD read(unsigned index);
+
+        op_entry* pop_entry(BDD l, BDD r, BDD op);
+        void push_entry(op_entry* e);
+        bool check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c);
+        
+        double count(BDD b, unsigned z);
+
+        void alloc_free_nodes(unsigned n);
+        void init_mark();
+        void set_mark(unsigned i) { m_mark[i] = m_mark_level; }
+        bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
+
+        void init_reorder();
+        void reorder_incref(unsigned n);
+        void reorder_decref(unsigned n);
+        void sift_up(unsigned level);
+        void sift_var(unsigned v);
+        double current_cost();
+        bool is_bad_cost(double new_cost, double best_cost) const;
+
+        static const BDD false_bdd = 0;
+        static const BDD true_bdd = 1;
+        static const unsigned max_rc = (1 << 10) - 1;
+
+        inline bool is_true(BDD b) const { return b == true_bdd; }
+        inline bool is_false(BDD b) const { return b == false_bdd; }
+        inline bool is_const(BDD b) const { return b <= 1; }
+        inline unsigned level(BDD b) const { return m_nodes[b].m_level; }
+        inline unsigned var(BDD b) const { return m_level2var[level(b)]; }
+        inline BDD lo(BDD b) const { return m_nodes[b].m_lo; }
+        inline BDD hi(BDD b) const { return m_nodes[b].m_hi; }
+        inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; VERIFY(!m_free_nodes.contains(b)); }
+        inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; VERIFY(!m_free_nodes.contains(b)); }
+        inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; }
+
+        double dnf_size(BDD b) { return count(b, 0); }
+        double cnf_size(BDD b) { return count(b, 1); }
+        unsigned bdd_size(bdd const& b);
+
+        bdd mk_not(bdd b);
+        bdd mk_and(bdd const& a, bdd const& b);
+        bdd mk_or(bdd const& a, bdd const& b);
+        bdd mk_xor(bdd const& a, bdd const& b);
+
+        void reserve_var(unsigned v);
+        bool well_formed();
+
+    public:
+        struct mem_out {};
+
+        bdd_manager(unsigned nodes);
+        ~bdd_manager();
+
+        void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; }
+
+        bdd mk_var(unsigned i);
+        bdd mk_nvar(unsigned i);
+
+        bdd mk_true();
+        bdd mk_false();
+
+        bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b);
+        bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b);
+        bdd mk_exists(unsigned v, bdd const& b);
+        bdd mk_forall(unsigned v, bdd const& b);
+        bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
+
+        std::ostream& display(std::ostream& out);
+        std::ostream& display(std::ostream& out, bdd const& b);
+
+        void gc();
+        void try_reorder();
+        void try_cnf_reorder(bdd const& b);
+    };
+
+    class bdd {
+        friend class bdd_manager;
+        unsigned     root;
+        bdd_manager* m;
+        bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
+    public:
+        bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
+        bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); }
+        bdd& operator=(bdd const& other);
+        ~bdd() { m->dec_ref(root); }
+        bdd lo() const { return bdd(m->lo(root), m); }
+        bdd hi() const { return bdd(m->hi(root), m); }
+        unsigned var() const { return m->var(root); }
+
+        bool is_true() const { return root == bdd_manager::true_bdd; }
+        bool is_false() const { return root == bdd_manager::false_bdd; }        
+
+        bdd operator!() { return m->mk_not(*this); }
+        bdd operator&&(bdd const& other) { return m->mk_and(*this, other); }
+        bdd operator||(bdd const& other) { return m->mk_or(*this, other); }
+        bdd operator^(bdd const& other) { return m->mk_xor(*this, other); }
+        bdd operator|=(bdd const& other) { return *this = *this || other; }
+        bdd operator&=(bdd const& other) { return *this = *this && other; }
+        std::ostream& display(std::ostream& out) const { return m->display(out, *this); }
+        bool operator==(bdd const& other) const { return root == other.root; }
+        bool operator!=(bdd const& other) const { return root != other.root; }
+        double cnf_size() const { return m->cnf_size(root); }
+        double dnf_size() const { return m->dnf_size(root); }
+        unsigned bdd_size() const { return m->bdd_size(*this); }
+    };
+
+    std::ostream& operator<<(std::ostream& out, bdd const& b);
+
+}
+
+
+#endif
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
new file mode 100644
index 000000000..86954d037
--- /dev/null
+++ b/src/sat/sat_elim_vars.cpp
@@ -0,0 +1,335 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_elim_vars.cpp
+
+Abstract:
+
+    Helper class for eliminating variables
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-14
+
+Revision History:
+
+--*/
+
+#include "sat/sat_simplifier.h"
+#include "sat/sat_elim_vars.h"
+#include "sat/sat_solver.h"
+
+namespace sat{
+
+    elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) {
+        m_mark_lim = 0;
+        m_max_literals = 11; 
+        m_miss = 0;
+        m_hit1 = 0;
+        m_hit2 = 0;
+    }
+
+    bool elim_vars::operator()(bool_var v) {
+        if (s.value(v) != l_undef)
+            return false;
+
+        literal pos_l(v, false);
+        literal neg_l(v, true);
+        unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l);
+        if (num_bin_pos > m_max_literals) return false;
+        unsigned num_bin_neg = simp.get_num_non_learned_bin(neg_l);
+        if (num_bin_neg > m_max_literals) return false;
+        clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
+        clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
+        unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size();
+        if (clause_size == 0) {
+            return false;
+        }
+        reset_mark();
+        mark_var(v);
+        if (!mark_literals(pos_occs)) return false;
+        if (!mark_literals(neg_occs)) return false;
+        if (!mark_literals(pos_l)) return false;
+        if (!mark_literals(neg_l)) return false;
+        
+        // associate index with each variable.
+        sort_marked();
+        bdd b1 = elim_var(v);
+        double sz1 = b1.cnf_size();
+        if (sz1 > 2*clause_size) {
+            ++m_miss;
+            return false;
+        }        
+        if (sz1 <= clause_size) {
+            ++m_hit1;
+            return elim_var(v, b1);
+        }
+        m.try_cnf_reorder(b1);
+        sz1 = b1.cnf_size();
+        if (sz1 <= clause_size) {
+            ++m_hit2;
+            return elim_var(v, b1);
+        } 
+        ++m_miss;
+        return false;
+    }
+
+    bool elim_vars::elim_var(bool_var v, bdd const& b) {
+        literal pos_l(v, false);
+        literal neg_l(v, true);
+        clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
+        clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
+
+        // eliminate variable
+        simp.m_pos_cls.reset();
+        simp.m_neg_cls.reset();
+        simp.collect_clauses(pos_l, simp.m_pos_cls);
+        simp.collect_clauses(neg_l, simp.m_neg_cls);
+        model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
+        simp.save_clauses(mc_entry, simp.m_pos_cls);
+        simp.save_clauses(mc_entry, simp.m_neg_cls);
+        s.m_eliminated[v] = true;
+        ++s.m_stats.m_elim_var_bdd;
+        simp.remove_bin_clauses(pos_l);
+        simp.remove_bin_clauses(neg_l);
+        simp.remove_clauses(pos_occs, pos_l);
+        simp.remove_clauses(neg_occs, neg_l);
+        pos_occs.reset();
+        neg_occs.reset();
+        literal_vector lits;
+        add_clauses(b, lits);        
+        return true;
+    }
+
+    bdd elim_vars::elim_var(bool_var v) {
+        unsigned index = 0;
+        for (bool_var w : m_vars) {
+            m_var2index[w] = index++;
+        }
+        literal pos_l(v, false);
+        literal neg_l(v, true);
+        clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
+        clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
+
+        bdd b1 = make_clauses(pos_l);
+        bdd b2 = make_clauses(neg_l);
+        bdd b3 = make_clauses(pos_occs);
+        bdd b4 = make_clauses(neg_occs);
+        bdd b0 = b1 && b2 && b3 && b4;
+        bdd b =  m.mk_exists(m_var2index[v], b0);       
+        TRACE("elim_vars",
+              tout << "eliminate " << v << "\n";
+              for (watched const& w : simp.get_wlist(~pos_l)) {
+                  if (w.is_binary_non_learned_clause()) {
+                      tout << pos_l << " " << w.get_literal() << "\n";
+                  }
+              }
+              m.display(tout, b1);
+              for (watched const& w : simp.get_wlist(~neg_l)) {
+                  if (w.is_binary_non_learned_clause()) {
+                      tout << neg_l << " " << w.get_literal() << "\n";
+                  }
+              }
+              m.display(tout, b2);
+              clause_use_list::iterator itp = pos_occs.mk_iterator();
+              while (!itp.at_end()) {
+                  clause const& c = itp.curr();
+                  tout << c << "\n";
+                  itp.next();
+              }
+              m.display(tout, b3);
+              clause_use_list::iterator itn = neg_occs.mk_iterator();
+              while (!itn.at_end()) {
+                  clause const& c = itn.curr();
+                  tout << c << "\n";
+                  itn.next();
+              }
+              m.display(tout, b4);
+              tout << "eliminated:\n";
+              tout << b << "\n";
+              tout << b.cnf_size() << "\n";
+              );
+
+        return b;
+    }
+
+    void elim_vars::add_clauses(bdd const& b, literal_vector& lits) {
+        if (b.is_true()) {
+            // no-op
+        }
+        else if (b.is_false()) {
+            SASSERT(lits.size() > 0);
+            literal_vector c(lits);
+            if (simp.cleanup_clause(c)) 
+                return;
+            
+            switch (c.size()) {
+            case 0:
+                s.set_conflict(justification());
+                break;
+            case 1: 
+                simp.propagate_unit(c[0]);
+                break;
+            case 2:
+                s.m_stats.m_mk_bin_clause++;
+                simp.add_non_learned_binary_clause(c[0], c[1]);
+                simp.back_subsumption1(c[0], c[1], false);
+                break;
+            default: {
+                if (c.size() == 3)
+                    s.m_stats.m_mk_ter_clause++;
+                else
+                    s.m_stats.m_mk_clause++;
+                clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false);
+                s.m_clauses.push_back(cp);
+                simp.m_use_list.insert(*cp);
+                if (simp.m_sub_counter > 0)
+                    simp.back_subsumption1(*cp);
+                else
+                    simp.back_subsumption0(*cp);
+                break;
+            }
+            }
+        }
+        else {
+            unsigned v = m_vars[b.var()];
+            lits.push_back(literal(v, false));
+            add_clauses(b.lo(), lits);
+            lits.pop_back();
+            lits.push_back(literal(v, true));
+            add_clauses(b.hi(), lits);
+            lits.pop_back();
+        }
+    }
+
+
+    void elim_vars::get_clauses(bdd const& b, literal_vector & lits, clause_vector& clauses, literal_vector& units) {
+        if (b.is_true()) {
+            return;
+        }
+        if (b.is_false()) {
+            if (lits.size() > 1) {
+                clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false);
+                clauses.push_back(c);
+            }
+            else {
+                units.push_back(lits.back());
+            }
+            return;
+        }
+
+        // if (v hi lo)
+        // (v | lo) & (!v | hi)
+        // if (v T lo) -> (v | lo) 
+        unsigned v = m_vars[b.var()];
+        lits.push_back(literal(v, false));
+        get_clauses(b.lo(), lits, clauses, units);
+        lits.pop_back();
+        lits.push_back(literal(v, true));
+        get_clauses(b.hi(), lits, clauses, units);
+        lits.pop_back();
+    }
+
+    void elim_vars::reset_mark() {
+        m_vars.reset();
+        m_mark.resize(s.num_vars());
+        m_var2index.resize(s.num_vars());
+        m_occ.resize(s.num_vars());
+        ++m_mark_lim;
+        if (m_mark_lim == 0) {
+            ++m_mark_lim;
+            m_mark.fill(0);
+        }
+    }
+
+    class elim_vars::compare_occ {
+        elim_vars& ev;
+    public:
+        compare_occ(elim_vars& ev):ev(ev) {}
+
+        bool operator()(bool_var v1, bool_var v2) const {
+            return ev.m_occ[v1] < ev.m_occ[v2];
+        }
+    };
+
+    void elim_vars::sort_marked() {
+        std::sort(m_vars.begin(), m_vars.end(), compare_occ(*this));
+    }
+
+    void elim_vars::shuffle_vars() {
+        unsigned sz = m_vars.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            unsigned x = m_rand(sz);
+            unsigned y = m_rand(sz);
+            std::swap(m_vars[x], m_vars[y]);
+        }
+    }
+
+    void elim_vars::mark_var(bool_var v) {
+        if (m_mark[v] != m_mark_lim) {
+            m_mark[v] = m_mark_lim;
+            m_vars.push_back(v);
+            m_occ[v] = 1;
+        }
+        else {
+            ++m_occ[v];
+        }
+    }
+
+    bool elim_vars::mark_literals(clause_use_list & occs) {
+        clause_use_list::iterator it = occs.mk_iterator();
+        while (!it.at_end()) {
+            clause const& c = it.curr();
+            for (literal l : c) {
+                mark_var(l.var());
+            }
+            if (num_vars() > m_max_literals) return false;
+            it.next();
+        }
+        return true;
+    }
+
+    bool elim_vars::mark_literals(literal lit) {
+        watch_list& wl = simp.get_wlist(lit);
+        for (watched const& w : wl) {
+            if (w.is_binary_non_learned_clause()) {
+                mark_var(w.get_literal().var());
+            }
+        }
+        return num_vars() <= m_max_literals;
+    }
+
+    bdd elim_vars::make_clauses(clause_use_list & occs) {
+        bdd result = m.mk_true();
+        clause_use_list::iterator it = occs.mk_iterator();
+        while (!it.at_end()) {
+            clause const& c = it.curr();
+            bdd cl = m.mk_false();
+            for (literal l : c) {
+                cl |= mk_literal(l);
+            }
+            it.next();
+            result &= cl;
+        }
+        return result;
+    }
+
+    bdd elim_vars::make_clauses(literal lit) {
+        bdd result = m.mk_true();
+        watch_list& wl = simp.get_wlist(~lit);
+        for (watched const& w : wl) {
+            if (w.is_binary_non_learned_clause()) {
+                result &= (mk_literal(lit) || mk_literal(w.get_literal()));
+            }
+        }        
+        return result;
+    }
+
+    bdd elim_vars::mk_literal(literal l) {
+        return l.sign() ? m.mk_nvar(m_var2index[l.var()]) : m.mk_var(m_var2index[l.var()]);
+    }
+
+};
+
diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h
new file mode 100644
index 000000000..ba5a02d67
--- /dev/null
+++ b/src/sat/sat_elim_vars.h
@@ -0,0 +1,74 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_elim_vars.h
+
+Abstract:
+
+    Helper class for eliminating variables
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-10-14
+
+Revision History:
+
+--*/
+#ifndef SAT_ELIM_VARS_H_
+#define SAT_ELIM_VARS_H_
+
+#include "sat/sat_types.h"
+#include "sat/sat_bdd.h"
+
+namespace sat {
+    class solver;
+    class simplifier;
+
+    class elim_vars {
+        class compare_occ;
+
+        simplifier& simp;
+        solver&     s;
+        bdd_manager m;
+        random_gen  m_rand;
+
+
+        svector<bool_var> m_vars;
+        unsigned_vector   m_mark;
+        unsigned          m_mark_lim;
+        unsigned_vector   m_var2index;
+        unsigned_vector   m_occ;
+        unsigned          m_miss;
+        unsigned          m_hit1;
+        unsigned          m_hit2;
+
+        unsigned m_max_literals;
+
+        unsigned num_vars() const { return m_vars.size(); }
+        void reset_mark();
+        void mark_var(bool_var v);
+        void sort_marked();
+        void shuffle_vars();
+        bool mark_literals(clause_use_list & occs);
+        bool mark_literals(literal lit);
+        bdd make_clauses(clause_use_list & occs);
+        bdd make_clauses(literal lit);
+        bdd mk_literal(literal l);
+        void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
+        void add_clauses(bdd const& b, literal_vector& lits);
+        bool elim_var(bool_var v, bdd const& b);
+        bdd  elim_var(bool_var v);
+
+    public:
+        elim_vars(simplifier& s);
+        bool operator()(bool_var v);
+        unsigned hit2() const { return m_hit1; } // first round bdd construction is minimal
+        unsigned hit1() const { return m_hit2; } // minimal after reshufling
+        unsigned miss() const { return m_miss; } // not-minimal
+    };
+
+};
+
+#endif
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 7e9e2d230..b15a32e32 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -415,14 +415,21 @@ namespace sat {
     }
 
     bool lookahead::missed_propagation() const {
+        if (inconsistent()) return false;
         for (literal l1 : m_trail) {
             SASSERT(is_true(l1));
             for (literal l2 : m_binary[l1.index()]) {
+                VERIFY(is_true(l2));
                 if (is_undef(l2)) return true;
             }
             unsigned sz = m_ternary_count[(~l1).index()];
             for (binary b : m_ternary[(~l1).index()]) {
                 if (sz-- == 0) break;
+                if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) {
+                    std::cout << b.m_u << " " << b.m_v << "\n";
+                    std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n"; 
+                    UNREACHABLE();
+                }
                 if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
                     return true;
             }
@@ -430,6 +437,7 @@ namespace sat {
         for (nary * n : m_nary_clauses) {
             if (n->size() == 1 && !is_true(n->get_head())) {
                 for (literal lit : *n) {
+                    VERIFY(!is_undef(lit));
                     if (is_undef(lit)) return true;
                 }
             }
@@ -1465,35 +1473,7 @@ namespace sat {
                     m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2);
                     break;
                 case ternary_reward:
-                    if (nonfixed == 2) {
-                        literal l1 = null_literal;
-                        literal l2 = null_literal;
-                        for (literal lit : *n) {
-                            if (!is_fixed(lit)) {
-                                if (l1 == null_literal) {
-                                    l1 = lit;
-                                }
-                                else {
-                                    SASSERT(l2 != null_literal);
-                                    l2 = lit;
-                                    break;
-                                }
-                            }
-                        }
-                        if (l1 == null_literal) {
-                            set_conflict();
-                            continue;
-                        }
-                        else if (l2 == null_literal) {
-                            propagated(l1);
-                        }
-                        else {
-                            m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()];
-                        }
-                    }
-                    else {
-                        m_lookahead_reward += (double)0.001;            
-                    }
+                    UNREACHABLE();
                     break;
                 case unit_literal_reward:
                     break;
@@ -1662,7 +1642,7 @@ namespace sat {
         }
         SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
         //SASSERT(!missed_conflict());
-        //SASSERT(inconsistent() || !missed_propagation());
+        //VERIFY(!missed_propagation());
         TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
     }
 
@@ -1705,6 +1685,7 @@ namespace sat {
                     unsat = inconsistent();
                     pop_lookahead1(lit, num_units);
                 }
+                // VERIFY(!missed_propagation());
                 if (unsat) {
                     TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
                     lookahead_backtrack();
@@ -1790,74 +1771,10 @@ namespace sat {
 
     bool lookahead::check_autarky(literal l, unsigned level) {
         return false;
-#if 0
-        // no propagations are allowed to reduce clauses.
-        for (nary * cp : m_nary[(~l).index()]) {
-            clause& c = *cp;
-            unsigned sz = c.size();
-            bool found = false;                
-            for (unsigned i = 0; !found && i < sz; ++i) {
-                found = is_true(c[i]);
-                if (found) {
-                    TRACE("sat", tout << c[i] << " is true in " << c << "\n";);
-                }
-            }
-            IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";);
-            if (!found) return false;
-        }
-        //
-        // bail out if there is a pending binary propagation.
-        // In general, we would have to check, recursively that 
-        // a binary propagation does not create reduced clauses.
-        // 
-        literal_vector const& lits = m_binary[l.index()];
-        TRACE("sat", tout << l << ": " << lits << "\n";);
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            literal l2 = lits[i];
-            if (is_true(l2)) continue;
-            SASSERT(!is_false(l2));
-            return false;
-        }
-
-        return true;
-#endif
     }
 
-
-    void lookahead::update_lookahead_reward(literal l, unsigned level) {
-        if (m_lookahead_reward == 0) {
-            if (!check_autarky(l, level)) {
-                // skip
-            }
-            else if (get_lookahead_reward(l) == 0) {
-                ++m_stats.m_autarky_propagations;
-                IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
-                    
-                TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] 
-                      << " " 
-                      << (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
-                lookahead_backtrack();
-                assign(l);
-                propagate();
-            }
-            else {
-                ++m_stats.m_autarky_equivalences;
-                // l => p is known, but p => l is possibly not. 
-                // add p => l.
-                // justification: any consequence of l
-                // that is not a consequence of p does not
-                // reduce the clauses.
-                literal p = get_parent(l);
-                SASSERT(p != null_literal);
-                if (m_stamp[p.var()] > m_stamp[l.var()]) {
-                    TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout););
-                    IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";);
-                    add_binary(~l, p);
-                    set_level(l, p);
-                }
-            }
-        }
-        else {            
+    void lookahead::update_lookahead_reward(literal l, unsigned level) {        
+        if (m_lookahead_reward != 0) {
             inc_lookahead_reward(l, m_lookahead_reward);
         }
     }
@@ -1900,7 +1817,6 @@ namespace sat {
         literal last_changed = null_literal;
         unsigned num_iterations = 0;
         while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
-            change = false;
             num_iterations++;
             for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
                 literal lit = m_lookahead[i].m_lit;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index e84213cfe..f98a117c8 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -248,6 +248,7 @@ namespace sat {
         inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
         inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; }
         void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
+        unsigned get_level(literal d) const { return m_stamp[d.var()]; }
         lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; }
         
         // set the level within a scope of the search.
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index e9d047086..14443a2f7 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -38,6 +38,21 @@ namespace sat {
         return *this;
     }
 
+    void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
+        SASSERT(!stack.empty());
+        unsigned sz = stack.size();
+        for (unsigned i = sz; i-- > 0; ) {
+            unsigned csz = stack[i].first;
+            literal lit = stack[i].second;
+            bool sat = false;
+            for (unsigned j = 0; !sat && j < csz; ++j) {
+                sat = value_at(c[j], m) == l_true;
+            }
+            if (!sat) {
+                m[lit.var()] = lit.sign() ? l_false : l_true;
+            }
+        }
+    }
     
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
@@ -49,17 +64,25 @@ namespace sat {
             // and the following procedure flips its value.
             bool sat = false;
             bool var_sign = false;
+            unsigned index = 0;
+            literal_vector clause;
             for (literal l : it->m_clauses) {
                 if (l == null_literal) {
                     // end of clause
                     if (!sat) {
                         m[it->var()] = var_sign ? l_false : l_true;
-                        break;
+                    }
+                    elim_stack* s = it->m_elim_stack[index];
+                    if (s) {
+                        process_stack(m, clause, s->stack());
                     }
                     sat = false;
-                    continue;
+                    ++index;
+                    clause.reset();
+                    continue;                    
                 }
 
+                clause.push_back(l);
                 if (sat)
                     continue;
                 bool sign  = l.sign();
@@ -142,6 +165,7 @@ namespace sat {
         SASSERT(&e < m_entries.end());
         for (literal l : c) e.m_clauses.push_back(l);
         e.m_clauses.push_back(null_literal);
+        e.m_elim_stack.push_back(nullptr);
         TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
     }
 
@@ -152,6 +176,7 @@ namespace sat {
         e.m_clauses.push_back(l1);
         e.m_clauses.push_back(l2);
         e.m_clauses.push_back(null_literal);
+        e.m_elim_stack.push_back(nullptr);
         TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";);
     }
 
@@ -163,9 +188,21 @@ namespace sat {
         for (unsigned i = 0; i < sz; ++i) 
             e.m_clauses.push_back(c[i]);
         e.m_clauses.push_back(null_literal);
+        e.m_elim_stack.push_back(nullptr);
         // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
     }
 
+    void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) {
+        SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
+        SASSERT(m_entries.begin() <= &e);
+        SASSERT(&e < m_entries.end());
+        for (literal l : c) e.m_clauses.push_back(l);
+        e.m_clauses.push_back(null_literal);
+        e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
+        TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
+    }
+
+
     bool model_converter::check_invariant(unsigned num_vars) const {
         // After a variable v occurs in an entry n and the entry has kind ELIM_VAR,
         // then the variable must not occur in any other entry occurring after it.
@@ -226,13 +263,8 @@ namespace sat {
 
     unsigned model_converter::max_var(unsigned min) const {
         unsigned result = min;
-        vector<entry>::const_iterator it = m_entries.begin();
-        vector<entry>::const_iterator end = m_entries.end();
-        for (; it != end; ++it) {
-            literal_vector::const_iterator lvit = it->m_clauses.begin();
-            literal_vector::const_iterator lvend = it->m_clauses.end();
-            for (; lvit != lvend; ++lvit) {
-                literal l = *lvit;
+        for (entry const& e : m_entries) {
+            for (literal l : e.m_clauses) {
                 if (l != null_literal) {
                     if (l.var() > result)
                         result = l.var();
diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h
index aae3ad479..dcbe450a8 100644
--- a/src/sat/sat_model_converter.h
+++ b/src/sat/sat_model_converter.h
@@ -20,6 +20,7 @@ Revision History:
 #define SAT_MODEL_CONVERTER_H_
 
 #include "sat/sat_types.h"
+#include "util/ref_vector.h"
 
 namespace sat {
     /**
@@ -36,25 +37,47 @@ namespace sat {
        it can be converted into a general Z3 model_converter
     */
     class model_converter {
+        
     public:
+        typedef svector<std::pair<unsigned, literal>> elim_stackv;
+
+        class elim_stack {
+            unsigned       m_refcount;
+            elim_stackv     m_stack;
+        public:
+            elim_stack(elim_stackv const& stack): 
+                m_refcount(0), 
+                m_stack(stack) {
+            }
+            ~elim_stack() { }
+            void inc_ref() { ++m_refcount; }
+            void dec_ref() { if (0 == --m_refcount) dealloc(this); }
+            elim_stackv const& stack() const { return m_stack; }
+        };
+
         enum kind { ELIM_VAR = 0, BLOCK_LIT };
         class entry {
             friend class model_converter;
             unsigned           m_var:31;
             unsigned           m_kind:1;
             literal_vector     m_clauses; // the different clauses are separated by null_literal
+            sref_vector<elim_stack>  m_elim_stack;
             entry(kind k, bool_var v):m_var(v), m_kind(k) {}
         public:
             entry(entry const & src):
                 m_var(src.m_var),
                 m_kind(src.m_kind),
-                m_clauses(src.m_clauses) {
+                m_clauses(src.m_clauses),
+                m_elim_stack(src.m_elim_stack) {
             }
             bool_var var() const { return m_var; }
             kind get_kind() const { return static_cast<kind>(m_kind); }
         };
     private:
         vector<entry>          m_entries;
+
+        void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
+
     public:
         model_converter();
         ~model_converter();
@@ -65,6 +88,7 @@ namespace sat {
         void insert(entry & e, clause const & c);
         void insert(entry & e, literal l1, literal l2);
         void insert(entry & e, clause_wrapper const & c);
+        void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack);
 
         bool empty() const { return m_entries.empty(); }
 
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 296c75180..d803617f5 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -39,6 +39,7 @@ def_module_params('sat',
                           ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
                           ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
+                          ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
                           ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 4d5946795..cd46f1916 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "sat/sat_simplifier.h"
 #include "sat/sat_simplifier_params.hpp"
 #include "sat/sat_solver.h"
+#include "sat/sat_elim_vars.h"
 #include "util/stopwatch.h"
 #include "util/trace.h"
 
@@ -190,6 +191,12 @@ namespace sat {
 
         // scoped_finalize _scoped_finalize(*this);
 
+        for (bool_var v = 0; v < s.num_vars(); ++v) {
+            if (!s.m_eliminated[v] && !is_external(v)) {
+                insert_elim_todo(v);
+            }
+        }
+
         do {
             if (m_subsumption)
                 subsume();
@@ -323,19 +330,15 @@ namespace sat {
         cs.set_end(it2);
     }
 
-    void simplifier::mark_all_but(clause const & c, literal l) {
-        unsigned sz = c.size();
-        for (unsigned i = 0; i < sz; i++) {
-            if (c[i] == l)
-                continue;
-            mark_visited(c[i]);
-        }
+    void simplifier::mark_all_but(clause const & c, literal l1) {
+        for (literal l2 : c) 
+            if (l2 != l1)
+                mark_visited(l2);
     }
 
     void simplifier::unmark_all(clause const & c) {
-        unsigned sz = c.size();
-        for (unsigned i = 0; i < sz; i++)
-            unmark_visited(c[i]);
+        for (literal l : c)
+            unmark_visited(l);
     }
 
     /**
@@ -945,7 +948,7 @@ namespace sat {
         }
 
         bool process_var(bool_var v) {
-            return !s.s.is_assumption(v) &&  !s.was_eliminated(v);
+            return !s.s.is_assumption(v) &&  !s.was_eliminated(v) && !s.is_external(v);
         }
 
         void operator()(unsigned num_vars) {
@@ -962,6 +965,169 @@ namespace sat {
                 literal l = m_queue.next();
                 process(l);
             }
+            cce();
+        }
+
+        //
+        // Resolve intersection
+        // Find literals that are in the intersection of all resolvents with l.
+        //
+        bool ri(literal l, literal_vector& inter) {
+            if (!process_var(l.var())) return false;
+            bool first = true;
+            for (watched & w : s.get_wlist(l)) {
+                if (w.is_binary_non_learned_clause()) {
+                    literal lit = w.get_literal();
+                    if (s.is_marked(~lit) && lit != ~l) continue;
+                    if (!first) {
+                        inter.reset();
+                        return false;
+                    }
+                    first = false;
+                    inter.push_back(lit);
+                }
+            }
+            clause_use_list & neg_occs = s.m_use_list.get(~l);
+            clause_use_list::iterator it = neg_occs.mk_iterator();
+            while (!it.at_end()) {
+                bool tautology = false;
+                clause & c = it.curr();
+                for (literal lit : c) {
+                    if (s.is_marked(~lit) && lit != ~l) {
+                        tautology = true;
+                        break;
+                    }
+                }
+                if (!tautology) {
+                    if (first) {
+                        for (literal lit : c) {
+                            if (lit != ~l) inter.push_back(lit);
+                        }
+                        first = false;
+                    }
+                    else {
+                        unsigned j = 0;
+                        unsigned sz = inter.size();
+                        for (unsigned i = 0; i < sz; ++i) {
+                            literal lit1 = inter[i];
+                            for (literal lit2 : c) {
+                                if (lit1 == lit2) {
+                                    inter[j++] = lit1;
+                                    break;
+                                }
+                            }
+                        }
+                        inter.shrink(j);
+                        if (j == 0) return false;
+                    }
+                }
+                it.next();
+            }
+            return first;
+        }
+
+        literal_vector m_covered_clause;
+        literal_vector m_intersection;
+        sat::model_converter::elim_stackv m_elim_stack;
+        unsigned m_ala_qhead;
+
+        /*
+         * C \/ l     l \/ lit
+         * -------------------
+         *    C \/ l \/ ~lit
+         */
+        void add_ala() {
+            for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
+                literal l = m_covered_clause[m_ala_qhead];
+                for (watched & w : s.get_wlist(~l)) {
+                    if (w.is_binary_clause()) {
+                        literal lit = w.get_literal();
+                        if (!s.is_marked(lit) && !s.is_marked(~lit)) {
+                            //std::cout << "ALA " << ~lit << "\n";
+                            m_covered_clause.push_back(~lit);
+                            s.mark_visited(~lit);
+                        }
+                    }
+                }
+            }
+        }
+
+        bool add_cla(literal& blocked) {
+            for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
+                m_intersection.reset();
+                if (ri(m_covered_clause[i], m_intersection)) {
+                    blocked = m_covered_clause[i];
+                    return true;
+                }
+                for (literal l : m_intersection) {
+                    if (!s.is_marked(l)) {
+                        s.mark_visited(l);
+                        m_covered_clause.push_back(l);
+                    }
+                }
+                if (!m_intersection.empty()) {
+                    m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
+                }
+            }
+            return false;
+        }
+
+        bool cla(literal& blocked) {
+            bool is_tautology = false;
+            for (literal l : m_covered_clause) s.mark_visited(l);
+            unsigned num_iterations = 0, sz;
+            m_elim_stack.reset();
+            m_ala_qhead = 0;
+            do {
+                do {
+                    ++num_iterations;
+                    sz = m_covered_clause.size();
+                    is_tautology = add_cla(blocked);
+                }
+                while (m_covered_clause.size() > sz && !is_tautology);
+                break;
+                //if (is_tautology) break;
+                //sz = m_covered_clause.size();
+                // unsound? add_ala();
+            }
+            while (m_covered_clause.size() > sz);
+            for (literal l : m_covered_clause) s.unmark_visited(l);
+            // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
+            return is_tautology;
+        }
+
+        // perform covered clause elimination.
+        // first extract the covered literal addition (CLA).
+        // then check whether the CLA is blocked.
+        bool cce(clause& c, literal& blocked) {
+            m_covered_clause.reset();
+            for (literal l : c) m_covered_clause.push_back(l);
+            return cla(blocked);
+        }
+
+        bool cce(literal lit, literal l2, literal& blocked) {
+            m_covered_clause.reset();
+            m_covered_clause.push_back(lit);
+            m_covered_clause.push_back(l2);
+            return cla(blocked);            
+        }
+
+        void cce() {
+            m_to_remove.reset();
+            literal blocked;
+            for (clause* cp : s.s.m_clauses) {
+                clause& c = *cp;
+                if (c.was_removed()) continue;
+                if (cce(c, blocked)) {
+                    model_converter::entry * new_entry = 0;
+                    block_covered_clause(c, blocked, new_entry);
+                    s.m_num_covered_clauses++;                    
+                }
+            }
+            for (clause* c : m_to_remove) {
+                s.remove_clause(*c);
+            }
+            m_to_remove.reset();
         }
 
         void process(literal l) {
@@ -971,6 +1137,7 @@ namespace sat {
                 return;
             }
 
+            literal blocked = null_literal;
             m_to_remove.reset();
             {
                 clause_use_list & occs = s.m_use_list.get(l);
@@ -981,19 +1148,8 @@ namespace sat {
                     SASSERT(c.contains(l));
                     s.mark_all_but(c, l);
                     if (all_tautology(l)) {
-                        TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
-                        if (new_entry == 0)
-                            new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
-                        m_to_remove.push_back(&c);
+                        block_clause(c, l, new_entry);
                         s.m_num_blocked_clauses++;
-                        mc.insert(*new_entry, c);
-                        unsigned sz = c.size();
-                        for (unsigned i = 0; i < sz; i++) {
-                            literal lit = c[i];
-                            if (lit != l && process_var(lit.var())) {
-                                m_queue.decreased(~lit);
-                            }
-                        }
                     }
                     s.unmark_all(c);
                     it.next();
@@ -1017,13 +1173,13 @@ namespace sat {
                     literal l2 = it->get_literal();
                     s.mark_visited(l2);
                     if (all_tautology(l)) {
-                        if (new_entry == 0)
-                            new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
-                        TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
-                        s.remove_bin_clause_half(l2, l, it->is_learned());
+                        block_binary(it, l, new_entry);
                         s.m_num_blocked_clauses++;
-                        m_queue.decreased(~l2);
-                        mc.insert(*new_entry, l, l2);
+                    }
+                    else if (cce(l, l2, blocked)) {
+                        model_converter::entry * blocked_entry = 0;
+                        block_covered_binary(it, l, blocked, blocked_entry);
+                        s.m_num_covered_clauses++;
                     }
                     else {
                         *it2 = *it;
@@ -1035,6 +1191,47 @@ namespace sat {
             }
         }
 
+        void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) {
+            TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
+            if (new_entry == 0)
+                new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
+            m_to_remove.push_back(&c);
+            for (literal lit : c) {
+                if (lit != l && process_var(lit.var())) {
+                    m_queue.decreased(~lit);
+                }
+            }
+        }
+
+        void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            prepare_block_clause(c, l, new_entry);
+            mc.insert(*new_entry, c);
+        }
+
+        void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            prepare_block_clause(c, l, new_entry);
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
+        }
+        
+        void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
+            if (new_entry == 0)
+                new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var()));
+            literal l2 = it->get_literal();
+            TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
+            s.remove_bin_clause_half(l2, l, it->is_learned());
+            m_queue.decreased(~l2);
+        }
+
+        void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+            prepare_block_binary(it, l, l, new_entry);
+            mc.insert(*new_entry, l, it->get_literal());
+        }
+
+        void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
+            prepare_block_binary(it, l, blocked, new_entry);
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
+        }
+
         bool all_tautology(literal l) {
             watch_list & wlist = s.get_wlist(l);
             m_counter -= wlist.size();
@@ -1076,9 +1273,11 @@ namespace sat {
         simplifier & m_simplifier;
         stopwatch    m_watch;
         unsigned     m_num_blocked_clauses;
+        unsigned     m_num_covered_clauses;
         blocked_cls_report(simplifier & s):
             m_simplifier(s),
-            m_num_blocked_clauses(s.m_num_blocked_clauses) {
+            m_num_blocked_clauses(s.m_num_blocked_clauses),
+            m_num_covered_clauses(s.m_num_covered_clauses) {
             m_watch.start();
         }
 
@@ -1087,6 +1286,8 @@ namespace sat {
             IF_VERBOSE(SAT_VB_LVL,
                        verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
                        << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
+                       << " :elim-covered-clauses " 
+                       << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
                        << mem_stat()
                        << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
@@ -1308,7 +1509,6 @@ namespace sat {
         clause_use_list & neg_occs = m_use_list.get(neg_l);
         unsigned num_pos = pos_occs.size() + num_bin_pos;
         unsigned num_neg = neg_occs.size() + num_bin_neg;
-        m_elim_counter -= num_pos + num_neg;
 
         TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
 
@@ -1349,7 +1549,6 @@ namespace sat {
         collect_clauses(pos_l, m_pos_cls);
         collect_clauses(neg_l, m_neg_cls);
 
-        m_elim_counter -= num_pos * num_neg + before_lits;
 
         TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
         unsigned before_clauses = num_pos + num_neg;
@@ -1371,7 +1570,10 @@ namespace sat {
         TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
 
 
+        m_elim_counter -= num_pos * num_neg + before_lits;
+
         // eliminate variable
+        ++s.m_stats.m_elim_var_res;
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);
@@ -1454,14 +1656,17 @@ namespace sat {
         elim_var_report rpt(*this);
         bool_var_vector vars;
         order_vars_for_elim(vars);
-
+        sat::elim_vars elim_bdd(*this);
         for (bool_var v : vars) {
             checkpoint();
-            if (m_elim_counter < 0)
+            if (m_elim_counter < 0) 
                 break;
             if (try_eliminate(v)) {
                 m_num_elim_vars++;
             }
+            else if (elim_bdd(v)) {
+                m_num_elim_vars++;
+            }
         }
 
         m_pos_cls.finalize();
@@ -1498,12 +1703,13 @@ namespace sat {
         st.update("subsumed", m_num_subsumed);
         st.update("subsumption resolution", m_num_sub_res);
         st.update("elim literals", m_num_elim_lits);
-        st.update("elim bool vars", m_num_elim_vars);
         st.update("elim blocked clauses", m_num_blocked_clauses);
+        st.update("elim covered clauses", m_num_covered_clauses);
     }
 
     void simplifier::reset_statistics() {
         m_num_blocked_clauses = 0;
+        m_num_covered_clauses = 0;
         m_num_subsumed = 0;
         m_num_sub_res = 0;
         m_num_elim_lits = 0;
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index a38df3d3c..fdfabb513 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -49,6 +49,7 @@ namespace sat {
 
     class simplifier {
         friend class ba_solver;
+        friend class elim_vars;
         solver &               s;
         unsigned               m_num_calls;
         use_list               m_use_list;
@@ -89,6 +90,7 @@ namespace sat {
 
         // stats
         unsigned               m_num_blocked_clauses;
+        unsigned               m_num_covered_clauses;
         unsigned               m_num_subsumed;
         unsigned               m_num_elim_vars;
         unsigned               m_num_sub_res;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8004c9635..ca1fc7801 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -4038,6 +4038,8 @@ namespace sat {
         st.update("dyn subsumption resolution", m_dyn_sub_res);
         st.update("blocked correction sets", m_blocked_corr_sets);
         st.update("units", m_units);
+        st.update("elim bool vars", m_elim_var_res);
+        st.update("elim bool vars bdd", m_elim_var_bdd);
     }
 
     void stats::reset() {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 020c1dc42..58d2824c7 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -67,6 +67,8 @@ namespace sat {
         unsigned m_dyn_sub_res;
         unsigned m_non_learned_generation;
         unsigned m_blocked_corr_sets;
+        unsigned m_elim_var_res;
+        unsigned m_elim_var_bdd;
         unsigned m_units;
         stats() { reset(); }
         void reset();
@@ -179,6 +181,7 @@ namespace sat {
         friend class local_search;
         friend struct mk_stat;
         friend class ccc;
+        friend class elim_vars;
     public:
         solver(params_ref const & p, reslimit& l);
         ~solver();
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 3db2908ed..d7b0e0892 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -1153,6 +1153,8 @@ struct sat2goal::imp {
                 }
             }
         }
+        //s.display(std::cout);
+        //r.display(std::cout);
     }
 
     void add_clause(sat::literal_vector const& lits, expr_ref_vector& lemmas) {
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index 9bacbe6a0..4eb2fbbe9 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/src/tactic/portfolio/parallel_tactic.cpp
@@ -63,12 +63,16 @@ class parallel_tactic : public tactic {
 
         unsigned num_units() const { return m_units; }
 
+        unsigned cube_size() const { return m_cube.size(); }
+
         solver& get_solver() { return *m_solver; }
 
         solver const& get_solver() const { return *m_solver; }
 
         params_ref const& params() const { return m_params; }
 
+        params_ref& params() { return m_params; }
+
         solver_state* clone(params_ref const& p, expr* cube) {
             ast_manager& m = m_solver->get_manager();
             ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode());
@@ -114,7 +118,7 @@ private:
         m_conflicts_decay_rate = 75;
         m_max_conflicts = m_conflicts_lower_bound;
         m_progress = 0;
-        m_num_threads = omp_get_num_procs();  // TBD adjust by possible threads used inside each solver.
+        m_num_threads = 2 * omp_get_num_procs();  // TBD adjust by possible threads used inside each solver.
     }
 
     unsigned get_max_conflicts() { 
@@ -175,16 +179,14 @@ private:
         }
     }
 
-    lbool simplify(solver& s) {
-        params_ref p;
-        p.copy(m_params);
-        p.set_uint("max_conflicts", 10);
-        p.set_bool("lookahead_simplify", true);
-        s.updt_params(p);
-        lbool is_sat = s.check_sat(0,0);
-        p.set_uint("max_conflicts", get_max_conflicts());
-        p.set_bool("lookahead_simplify", false);
-        s.updt_params(p);
+    lbool simplify(solver_state& s) {
+        s.params().set_uint("max_conflicts", 10);
+        s.params().set_bool("lookahead_simplify", true);
+        s.get_solver().updt_params(s.params());
+        lbool is_sat = s.get_solver().check_sat(0,0);
+        s.params().set_uint("max_conflicts", get_max_conflicts());
+        s.params().set_bool("lookahead_simplify", false);
+        s.get_solver().updt_params(s.params());
         return is_sat;
     }
 
@@ -228,12 +230,10 @@ private:
         return l_undef;
     }
 
-    lbool solve(solver& s) {
-        params_ref p;
-        p.copy(m_params);
-        p.set_uint("max_conflicts", get_max_conflicts());
-        s.updt_params(p);
-        return s.check_sat(0, 0);
+    lbool solve(solver_state& s) {
+        s.params().set_uint("max_conflicts", get_max_conflicts());
+        s.get_solver().updt_params(s.params());
+        return s.get_solver().check_sat(0, 0);
     }
 
     void remove_unsat(svector<int>& unsat) {
@@ -260,6 +260,25 @@ private:
     }
 
     lbool solve(model_ref& mdl) {        
+
+        {
+            solver_state& st = *m_solvers[0];
+            st.params().set_uint("restart.max", 200);
+            st.get_solver().updt_params(st.params());
+            lbool is_sat = st.get_solver().check_sat(0, 0);
+            st.params().set_uint("restart.max", UINT_MAX);
+            st.get_solver().updt_params(st.params());
+            switch (is_sat) {
+            case l_true: 
+                get_model(mdl, 0);
+                return l_true;
+            case l_false:
+                return l_false;
+            default:
+                break;
+            }
+        }
+            
         while (true) {
             int sz = pick_solvers();
 
@@ -276,7 +295,7 @@ private:
 
             #pragma omp parallel for
             for (int i = 0; i < sz; ++i) {
-                lbool is_sat = simplify(m_solvers[i]->get_solver());
+                lbool is_sat = simplify(*m_solvers[i]);
                 switch (is_sat) {
                 case l_false: 
                     #pragma omp critical (parallel_tactic)
@@ -305,7 +324,7 @@ private:
 
             #pragma omp parallel for
             for (int i = 0; i < sz; ++i) {
-                lbool is_sat = solve(m_solvers[i]->get_solver());
+                lbool is_sat = solve(*m_solvers[i]);
                 switch (is_sat) {
                 case l_false: 
                     #pragma omp critical (parallel_tactic)
@@ -328,6 +347,7 @@ private:
             remove_unsat(unsat);
 
             sz = std::min(max_num_splits(), sz);
+            sz = std::min(static_cast<int>(m_num_threads/2), sz);
             if (sz == 0) continue;
             
 
@@ -360,9 +380,9 @@ private:
     }
 
     std::ostream& display(std::ostream& out) {
+        out << "branches: " << m_solvers.size() << "\n";
         for (solver_state* s : m_solvers) {
-            out << "solver units " << s->num_units() << "\n";
-            out << "cube " << s->cube() << "\n";
+            out << "cube " << s->cube_size() << " units " << s->num_units() << "\n";
         }
         m_stats.display(out);
         return out;
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 1c1665363..b487fe9ba 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -16,6 +16,7 @@ add_executable(test-z3
   arith_rewriter.cpp
   arith_simplifier_plugin.cpp
   ast.cpp
+  bdd.cpp
   bit_blaster.cpp
   bits.cpp
   bit_vector.cpp
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
new file mode 100644
index 000000000..ea5a0bc34
--- /dev/null
+++ b/src/test/bdd.cpp
@@ -0,0 +1,83 @@
+#include "sat/sat_bdd.h"
+
+namespace sat {
+    static void test1() {
+        bdd_manager m(20);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        bdd c1 = v0 && v1 && v2;
+        bdd c2 = v2 && v0 && v1;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
+        std::cout << "cnf size: " << c1.cnf_size() << "\n";
+
+        c1 = v0 || v1 || v2;
+        c2 = v2 || v1 || v0;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
+        std::cout << "cnf size: " << c1.cnf_size() << "\n";
+    }
+
+    static void test2() {
+        bdd_manager m(20);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1));
+        SASSERT(m.mk_ite(v0,v1,v1) == v1);
+        SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1));
+        SASSERT(m.mk_ite(v1,v0,v0) == v0);
+        SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1));
+        SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1));
+        SASSERT(!(v0 && v1) == (!v0 || !v1));
+        SASSERT(!(v0 || v1) == (!v0 && !v1));
+    }
+
+    static void test3() {
+        bdd_manager m(20);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        bdd c1 = (v0 && v1) || v2;
+        bdd c2 = m.mk_exists(0, c1);
+        std::cout << c1 << "\n";
+        std::cout << c2 << "\n";
+        SASSERT(c2 == (v1 || v2));
+        c2 = m.mk_exists(1, c1);
+        SASSERT(c2 == (v0 || v2));
+        c2 = m.mk_exists(2, c1);
+        SASSERT(c2.is_true());
+        SASSERT(m.mk_exists(3, c1) == c1);
+        c1 = (v0 && v1) || (v1 && v2) || (!v0 && !v2);
+        c2 = m.mk_exists(0, c1);
+        SASSERT(c2 == (v1 || (v1 && v2) || !v2));
+        c2 = m.mk_exists(1, c1);
+        SASSERT(c2 == (v0 || v2 || (!v0 && !v2)));
+        c2 = m.mk_exists(2, c1);
+        SASSERT(c2 == ((v0 && v1) || v1 || !v0));
+    }
+
+    void test4() {
+        bdd_manager m(3);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        bdd c1 = (v0 && v2) || v1;
+        std::cout << "before reorder:\n";
+        std::cout << c1 << "\n";
+        std::cout << c1.bdd_size() << "\n";
+        m.gc();
+        m.try_reorder();
+        std::cout << "after reorder:\n";
+        std::cout << c1 << "\n";
+        std::cout << c1.bdd_size() << "\n";
+    }
+}
+
+void tst_bdd() {
+    sat::test1();
+    sat::test2();
+    sat::test3();
+    sat::test4();
+}
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 4aeba26c5..33d0abae5 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -245,6 +245,7 @@ int main(int argc, char ** argv) {
     TST_ARGV(sat_lookahead);
     TST_ARGV(sat_local_search);
     TST_ARGV(cnf_backbones);
+    TST(bdd);
     //TST_ARGV(hs);
 }
 
diff --git a/src/util/vector.h b/src/util/vector.h
index 2e2640de3..f068481db 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -410,7 +410,7 @@ public:
 
     void fill(unsigned sz, T const & elem) {
         resize(sz);
-        fill(sz, elem);
+        fill(elem);
     }
 
     bool contains(T const & elem) const {
@@ -472,6 +472,11 @@ typedef svector<char> char_vector;
 typedef svector<signed char> signed_char_vector;
 typedef svector<double> double_vector;
 
+inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) {
+    for (unsigned u : v) out << u << " ";
+    return out;
+}
+
 template<typename Hash, typename Vec>
 struct vector_hash_tpl {
     Hash m_hash;