diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index 2f2c76da6..9d1d8dd7e 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -17,7 +17,6 @@ z3_add_component(sat
     sat_ddfw_wrapper.cpp    
     sat_drat.cpp
     sat_elim_eqs.cpp
-    sat_elim_vars.cpp
     sat_gc.cpp
     sat_integrity_checker.cpp
     sat_local_search.cpp
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
deleted file mode 100644
index e07dcea77..000000000
--- a/src/sat/sat_elim_vars.cpp
+++ /dev/null
@@ -1,335 +0,0 @@
-/*++
-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.num_nonlearned_bin(pos_l);
-        if (num_bin_pos > m_max_literals) return false;
-        unsigned num_bin_neg = simp.num_nonlearned_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.num_irredundant() + neg_occs.num_irredundant();
-        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();
-        dd::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, dd::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);
-        VERIFY(!simp.is_external(v));
-
-        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(v, b, lits);         
-        return true;
-    }
-
-    dd::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);
-
-        dd::bdd b1 = make_clauses(pos_l);
-        dd::bdd b2 = make_clauses(neg_l);
-        dd::bdd b3 = make_clauses(pos_occs);
-        dd::bdd b4 = make_clauses(neg_occs);
-        dd::bdd b0 = b1 && b2 && b3 && b4;
-        dd::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(bool_var v0, dd::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();
-                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.alloc_clause(c.size(), c.data(), 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(v0, b.lo(), lits);
-            lits.pop_back();
-            lits.push_back(literal(v, true));
-            add_clauses(v0, b.hi(), lits);
-            lits.pop_back();
-        }
-    }
-
-
-    void elim_vars::get_clauses(dd::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.alloc_clause(lits.size(), lits.data(), 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;
-    }
-
-    dd::bdd elim_vars::make_clauses(clause_use_list & occs) {
-        dd::bdd result = m.mk_true();       
-        for (auto it = occs.mk_iterator(); !it.at_end(); it.next()) {
-            clause const& c = it.curr();
-            dd::bdd cl = m.mk_false();
-            for (literal l : c) {
-                cl |= mk_literal(l);
-            }           
-            result &= cl;            
-        }
-        return result;
-    }
-
-    dd::bdd elim_vars::make_clauses(literal lit) {
-        dd::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;
-    }
-
-    dd::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
deleted file mode 100644
index 6465cbb87..000000000
--- a/src/sat/sat_elim_vars.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/*++
-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:
-
---*/
-#pragma once
-
-#include "sat/sat_types.h"
-#include "math/dd/dd_bdd.h"
-
-namespace sat {
-    class solver;
-    class simplifier;
-
-    class elim_vars {
-        class compare_occ;
-
-        simplifier& simp;
-        solver&     s;
-        dd::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);
-        dd::bdd make_clauses(clause_use_list & occs);
-        dd::bdd make_clauses(literal lit);
-        dd::bdd mk_literal(literal l);
-        void get_clauses(dd::bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
-        void add_clauses(bool_var v, dd::bdd const& b, literal_vector& lits);
-        bool elim_var(bool_var v, dd::bdd const& b);
-        dd::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
-    };
-
-};
-
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 56b81604d..289afdd75 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -21,7 +21,6 @@ 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 "sat/sat_integrity_checker.h"
 #include "util/stopwatch.h"
 #include "util/trace.h"
@@ -111,9 +110,6 @@ namespace sat {
     bool simplifier::cce_enabled()  const { return bce_enabled_base() && (m_cce || m_acce); }
     bool simplifier::abce_enabled() const { return bce_enabled_base() && m_abce; }
     bool simplifier::bca_enabled()  const { return bce_enabled_base() && m_bca; }
-    bool simplifier::elim_vars_bdd_enabled() const { 
-        return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); 
-    }
     bool simplifier::elim_vars_enabled() const { 
         return !m_incremental_mode && !s.tracking_assumptions() && m_elim_vars && single_threaded(); 
     }    
@@ -2076,24 +2072,19 @@ namespace sat {
     };
 
     void simplifier::elim_vars() {
-        if (!elim_vars_enabled()) return;
+        if (!elim_vars_enabled()) 
+            return;
         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) 
                 break;
-            if (is_external(v)) {
-                // skip
-            }
-            else if (try_eliminate(v)) {
-                m_num_elim_vars++;
-            }
-            else if (elim_vars_bdd_enabled() && elim_bdd(v)) { 
-                m_num_elim_vars++;
-            }
+            if (is_external(v))
+                ; // skip            
+            else if (try_eliminate(v)) 
+                m_num_elim_vars++;            
         }
 
         m_pos_cls.finalize();
@@ -2126,8 +2117,6 @@ namespace sat {
         m_subsumption             = p.subsumption();
         m_subsumption_limit       = p.subsumption_limit();
         m_elim_vars               = p.elim_vars();
-        m_elim_vars_bdd           = false && p.elim_vars_bdd(); // buggy?
-        m_elim_vars_bdd_delay     = p.elim_vars_bdd_delay();
         m_incremental_mode        = s.get_config().m_incremental && !p.override_incremental();
     }
 
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index 93864ce24..0275ef248 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -23,8 +23,6 @@ def_module_params(module_name='sat',
                           ('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
-                          ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
-                          ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
                           ('probing', BOOL, True, 'apply failed literal detection during simplification'),
                           ('probing_limit', UINT, 5000000, 'limit to the number of probe calls'),
                           ('probing_cache', BOOL, True, 'add binary literals as lemmas'),