diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp
index aecc77a58..3fbb02c37 100644
--- a/src/sat/dimacs.cpp
+++ b/src/sat/dimacs.cpp
@@ -260,17 +260,6 @@ namespace dimacs {
                 m_record.m_tag = drat_record::tag_t::is_clause;
                 m_record.m_status = sat::status::th(false, theory_id);
                 break;
-            case 'g':
-                // parse garbage collected Boolean variable
-                ++in;
-                skip_whitespace(in);
-                b = parse_int(in, err);
-                e = parse_int(in, err);
-                if (e != 0 || b <= 0)
-                    throw lex_error();
-                m_record.m_tag = drat_record::tag_t::is_var_gc;
-                m_record.m_node_id = b;
-                break;
             case 'e':
                 // parse expression definition
                 parse_ast(drat_record::tag_t::is_node);
diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h
index eaf6a3a5f..690f5b0fc 100644
--- a/src/sat/dimacs.h
+++ b/src/sat/dimacs.h
@@ -53,7 +53,7 @@ namespace dimacs {
     };
 
     struct drat_record {
-        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var_gc };
+        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def };
         tag_t            m_tag{ tag_t::is_clause };
         // a clause populates m_lits and m_status
         // a node populates m_node_id, m_name, m_args
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 6c30d4ad6..20d7c8f1e 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -257,22 +257,6 @@ namespace sat {
         }
     }
 
-    void drat::gc_var(bool_var v) {
-        sat::literal l(v, false);
-        // TBD: we want to remove all clauses that mention v.
-        std::cout << "GC " << v << "\n";
-        m_watches[l.index()].reset();
-        m_watches[(~l).index()].reset();
-        if (m_assignment[l.var()] != l_undef) {
-            unsigned j = 0;
-            for (literal lit : m_units)
-                if (lit.var() != v)
-                    m_units[j++] = lit;
-            m_units.shrink(j);
-            m_assignment[l.var()] = l_undef;
-        }
-    }
-
     void drat::bool_def(bool_var v, unsigned n) {
         if (m_out)
             (*m_out) << "b " << v << " " << n << " 0\n";
@@ -293,11 +277,6 @@ namespace sat {
             (*m_out) << " 0\n";
     }
 
-    void drat::log_gc_var(bool_var v) {
-        if (m_out)
-            (*m_out) << "g " << v << " 0\n";
-    }
-
     void drat::log_adhoc(std::function<void(std::ostream&)>& fn) {
         if (m_out)
             fn(*m_out);
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index b0f84f7b7..a9690f635 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -131,8 +131,6 @@ namespace sat {
         void add(literal_vector const& c); // add learned clause
         void add(unsigned sz, literal const* lits, status st);
 
-        void gc_var(bool_var v);
-
         // support for SMT - connect Boolean variables with AST nodes
         // associate AST node id with Boolean variable v
         void bool_def(bool_var v, unsigned n);
@@ -142,8 +140,6 @@ namespace sat {
         void def_add_arg(unsigned arg);
         void def_end();
 
-        void log_gc_var(bool_var v);
-
         // ad-hoc logging until a format is developed
         void log_adhoc(std::function<void(std::ostream&)>& fn);
 
diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 86536ac47..7f1f54059 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -12,6 +12,7 @@ z3_add_component(sat_smt
     ba_solver.cpp
     ba_xor.cpp
     bv_ackerman.cpp
+    bv_delay_internalize.cpp
     bv_internalize.cpp
     bv_invariant.cpp
     bv_solver.cpp
@@ -20,7 +21,9 @@ z3_add_component(sat_smt
     euf_invariant.cpp
     euf_model.cpp
     euf_proof.cpp
+    euf_relevancy.cpp
     euf_solver.cpp
+    sat_dual_solver.cpp
     sat_th.cpp
     xor_solver.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
new file mode 100644
index 000000000..8b0c0ba69
--- /dev/null
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -0,0 +1,146 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv_delay_internalize.cpp
+
+Abstract:
+
+    Checking of relevant bv nodes, and if required delay axiomatize
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-22
+
+--*/
+
+#include "sat/smt/bv_solver.h"
+#include "sat/smt/euf_solver.h"
+
+namespace bv {
+
+    bool solver::check_delay_internalized(euf::enode* n) {
+        expr* e = n->get_expr();
+        SASSERT(bv.is_bv(e));
+        SASSERT(get_internalize_mode(e) != internalize_mode::no_delay_i);
+        switch (to_app(e)->get_decl_kind()) {
+        case OP_BMUL:
+            return check_mul(n);
+        default:
+            return check_eval(n);
+        }
+        return true;
+    }
+
+    bool solver::should_bit_blast(expr* e) {
+        return bv.get_bv_size(e) <= 10;
+    }
+
+    void solver::eval_args(euf::enode* n, vector<rational>& args) {
+        rational val;
+        for (euf::enode* arg : euf::enode_args(n)) {
+            theory_var v = arg->get_th_var(get_id());
+            VERIFY(get_fixed_value(v, val));
+            args.push_back(val);
+        }
+    }
+
+    bool solver::check_mul(euf::enode* n) {
+        SASSERT(n->num_args() >= 2);
+        app* e = to_app(n->get_expr());
+        rational val, val_mul(1);        
+        vector<rational> args;
+        eval_args(n, args);
+        for (rational const& val_arg : args)
+            val_mul *= val_arg;
+        theory_var v = n->get_th_var(get_id());
+        VERIFY(get_fixed_value(v, val));
+        val_mul = mod(val_mul, power2(get_bv_size(v)));
+        IF_VERBOSE(12, verbose_stream() << "check_mul " << mk_bounded_pp(n->get_expr(), m) << " " << args << " = " << val_mul << " =? " << val << "\n");
+        if (val_mul == val)
+            return true;
+
+        // Some possible approaches:
+
+        // check base cases: val_mul = 0 or val = 0, some values in product are 1, 
+
+        // check discrepancies in low-order bits
+        // Add axioms for multiplication when fixing high-order bits to 0
+      
+        // Hensel lifting:
+        // The idea is dual to fixing high-order bits. Fix the low order bits where multiplication
+        // is correct, and propagate on the next bit that shows a discrepancy.
+
+        // check Montgommery properties: (x*y) mod p = (x mod p)*(y mod p) for small primes p
+
+        // check ranges lo <= x <= hi, lo' <= y <= hi', lo*lo' < x*y <= hi*hi' for non-overflowing values.
+
+        // check tangets hi >= y >= y0 and hi' >= x => x*y >= x*y0
+
+        // compute S-polys for a set of constraints.
+
+        set_delay_internalize(e, internalize_mode::no_delay_i);
+        internalize_circuit(e, v);
+        return false;
+    }
+
+    bool solver::check_eval(euf::enode* n) {
+        expr_ref_vector args(m);
+        expr_ref r1(m), r2(m);
+        rational val;
+        app* a = to_app(n->get_expr());
+        theory_var v = n->get_th_var(get_id());
+        VERIFY(get_fixed_value(v, val));
+        r1 = bv.mk_numeral(val, get_bv_size(v));
+        SASSERT(bv.is_bv(a));
+        for (euf::enode* arg : euf::enode_args(n)) {
+            SASSERT(bv.is_bv(arg->get_expr()));
+            theory_var v_arg = arg->get_th_var(get_id());
+            VERIFY(get_fixed_value(v_arg, val));
+            args.push_back(bv.mk_numeral(val, get_bv_size(v_arg)));
+        }
+        r2 = m.mk_app(a->get_decl(), args);        
+        ctx.get_rewriter()(r2);
+        if (r1 == r2)
+            return true;
+        set_delay_internalize(a, internalize_mode::no_delay_i);
+        internalize_circuit(a, v);
+        return false;
+    }
+
+    void solver::set_delay_internalize(expr* e, internalize_mode mode) {
+        if (!m_delay_internalize.contains(e))
+            ctx.push(insert_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e));
+        m_delay_internalize.insert(e, mode);
+    }
+
+    solver::internalize_mode solver::get_internalize_mode(expr* e) {
+        if (!bv.is_bv(e))
+            return internalize_mode::no_delay_i;
+        if (!get_config().m_bv_delay)
+            return internalize_mode::no_delay_i;
+        switch (to_app(e)->get_decl_kind()) {
+        case OP_BMUL: 
+        case OP_BSMUL_NO_OVFL:
+        case OP_BSMUL_NO_UDFL:
+        case OP_BUMUL_NO_OVFL:
+        case OP_BSMOD_I:
+        case OP_BUREM_I:
+        case OP_BSREM_I:
+        case OP_BUDIV_I:
+        case OP_BSDIV_I: {
+            if (should_bit_blast(e))
+                return internalize_mode::no_delay_i;
+            internalize_mode mode = internalize_mode::init_bits_i;
+            if (!m_delay_internalize.find(e, mode))
+                set_delay_internalize(e, mode);
+            return mode;
+        }
+        default:
+            return internalize_mode::no_delay_i;
+        }
+    }
+
+
+}
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index df37c8ee7..0af6cc1cd 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -148,15 +148,23 @@ namespace bv {
     bool solver::post_visit(expr* e, bool sign, bool root) {
         euf::enode* n = expr2enode(e);
         app* a = to_app(e);
-        
+
         SASSERT(!n || !n->is_attached_to(get_id()));
         bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
-        if (!n) 
+        if (!n)
             n = mk_enode(e, suppress_args);
 
         SASSERT(!n->is_attached_to(get_id()));
         theory_var v = mk_var(n);
         SASSERT(n->is_attached_to(get_id()));
+        if (internalize_mode::init_bits_i == get_internalize_mode(a)) 
+            mk_bits(n->get_th_var(get_id()));
+        else
+            internalize_circuit(a, v);
+        return true;
+    }
+
+    bool solver::internalize_circuit(app* a, theory_var v) {
 
         std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits)> bin;
         std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref& bit)> ebin;
@@ -507,30 +515,30 @@ namespace bv {
         init_bits(n, bits);
     }
 
-    void solver::internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
-        SASSERT(n->get_num_args() == 2);
+    void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
+        SASSERT(e->get_num_args() == 2);
         expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
-        get_arg_bits(n, 0, arg1_bits);
-        get_arg_bits(n, 1, arg2_bits);
+        get_arg_bits(e, 0, arg1_bits);
+        get_arg_bits(e, 1, arg2_bits);
         SASSERT(arg1_bits.size() == arg2_bits.size());
         fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits);
-        init_bits(n, bits);
+        init_bits(e, bits);
     }
 
-    void solver::internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
-        SASSERT(n->get_num_args() >= 2);
+    void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
+        SASSERT(e->get_num_args() >= 2);
         expr_ref_vector bits(m), new_bits(m), arg_bits(m);
-        unsigned i = n->get_num_args() - 1;        
-        get_arg_bits(n, i, bits);
+        unsigned i = e->get_num_args() - 1;
+        get_arg_bits(e, i, bits);
         for (; i-- > 0; ) {
             arg_bits.reset();
-            get_arg_bits(n, i, arg_bits);
+            get_arg_bits(e, i, arg_bits);
             SASSERT(arg_bits.size() == bits.size());
             new_bits.reset();
             fn(arg_bits.size(), arg_bits.c_ptr(), bits.c_ptr(), new_bits);
             bits.swap(new_bits);
         }        
-        init_bits(n, bits);
+        init_bits(e, bits);
         TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";);
     }
 
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 12b669200..bd82410bc 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -378,7 +378,7 @@ namespace bv {
             break;
         }
         ctx.get_drat().add(lits, status());
-        ctx.get_drat().log_gc_var(leq.var()); // TBD, a proper way would be to delete the lemma after use.
+        // TBD, a proper way would be to delete the lemma after use.
     }
 
     void solver::asserted(literal l) {
@@ -493,7 +493,14 @@ namespace bv {
     sat::check_result solver::check() {
         force_push();
         SASSERT(m_prop_queue.size() == m_prop_queue_head);
-        return sat::check_result::CR_DONE;
+        bool ok = true;
+        for (auto kv : m_delay_internalize) {
+            if (ctx.is_relevant(kv.m_key) && 
+                kv.m_value == internalize_mode::init_bits_i &&
+                !check_delay_internalized(expr2enode(kv.m_key)))
+                ok = false;
+        }
+        return ok ? sat::check_result::CR_DONE : sat::check_result::CR_CONTINUE;
     }
 
     void solver::push_core() {
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index 0b8f51683..e29ecffdf 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -53,9 +53,9 @@ namespace bv {
         struct bv_justification {
             enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne };
             kind_t     m_kind;
+            unsigned   m_idx{ UINT_MAX };
             theory_var m_v1{ euf::null_theory_var };
             theory_var m_v2 { euf::null_theory_var };
-            unsigned   m_idx{ UINT_MAX };
             sat::literal m_consequent;
             sat::literal m_antecedent;
             bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
@@ -267,6 +267,7 @@ namespace bv {
         void init_bits(expr* e, expr_ref_vector const & bits);
         void mk_bits(theory_var v);
         void add_def(sat::literal def, sat::literal l);
+        bool internalize_circuit(app* a, theory_var v);
         void internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn);
         void internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
         void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
@@ -288,6 +289,21 @@ namespace bv {
         void assert_int2bv_axiom(app* n);
         void assert_ackerman(theory_var v1, theory_var v2);
 
+        // delay internalize
+        enum class internalize_mode {
+            no_delay_i,
+            init_bits_i
+        };
+
+        obj_map<expr, internalize_mode> m_delay_internalize;
+        bool should_bit_blast(expr * n);
+        bool check_delay_internalized(euf::enode* n);
+        bool check_mul(euf::enode* n);
+        bool check_eval(euf::enode* n);
+        internalize_mode get_internalize_mode(expr* e);
+        void set_delay_internalize(expr* e, internalize_mode mode);
+        void eval_args(euf::enode* n, vector<rational>& args);
+
         // solving
         theory_var find(theory_var v) const { return m_find.find(v); }
         void find_wpos(theory_var v);
@@ -302,6 +318,7 @@ namespace bv {
         bool propagate_eq_occurs(eq_occurs const& occ);
         numeral const& power2(unsigned i) const;
 
+
         // invariants
         bool check_zero_one_bits(theory_var v);
         void check_missing_propagation() const;
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
new file mode 100644
index 000000000..65726a150
--- /dev/null
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    euf_relevancy.cpp
+
+Abstract:
+
+    Features for relevancy tracking.
+    A reduced (minimal) implicant is extracted by running a dual solver.
+    Then the literals in the implicant are used as a basis for marking
+    subterms relevant.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-09-22
+
+--*/
+
+#include "sat/smt/euf_solver.h"
+
+namespace euf {
+
+    void solver::ensure_dual_solver() {
+        if (!m_dual_solver)
+            m_dual_solver = alloc(sat::dual_solver, s().rlimit());
+    }
+
+    void solver::add_root(unsigned n, sat::literal const* lits) {
+        bool_var v = s().add_var(false);
+        ensure_dual_solver();
+        m_dual_solver->add_root(sat::literal(v, false), n, lits);
+    }
+
+    void solver::add_aux(unsigned n, sat::literal const* lits) {
+        ensure_dual_solver();
+        m_dual_solver->add_aux(n, lits);
+    }
+
+    void solver::track_relevancy(sat::bool_var v) {
+        ensure_dual_solver();
+        m_dual_solver->track_relevancy(v);
+    }
+
+    bool solver::init_relevancy() {
+        m_relevant_expr_ids.reset();
+        bool_vector visited;
+        ptr_vector<expr> todo;
+        if (!m_dual_solver)
+            return true;
+        if (!(*m_dual_solver)(s()))
+            return false;
+        unsigned max_id = 0;
+        for (enode* n : m_egraph.nodes())
+            max_id = std::max(max_id, n->get_expr_id());
+        m_relevant_expr_ids.resize(max_id + 1, false);
+        auto const& core = m_dual_solver->core();
+        for (auto lit : core) {
+            expr* e = m_var2expr.get(lit.var(), nullptr);
+            if (e)
+                todo.push_back(e);
+        }
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            expr* e = todo[i];
+            if (visited.get(e->get_id(), false))
+                continue;
+            visited.setx(e->get_id(), true, false);
+            if (!si.is_bool_op(e)) 
+                m_relevant_expr_ids.setx(e->get_id(), true, false);
+            if (!is_app(e))
+                continue;
+            for (expr* arg : *to_app(e))
+                if (!visited.get(arg->get_id(), false))
+                    todo.push_back(arg);
+        }
+
+        TRACE("euf",
+            for (enode* n : m_egraph.nodes())
+                if (is_relevant(n))
+                    tout << "relevant " << mk_bounded_pp(n->get_expr(), m) << "\n";);
+        return true;
+    }
+}
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index d63532bbf..f80a1d25a 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -342,6 +342,10 @@ namespace euf {
         TRACE("euf", s().display(tout););
         bool give_up = false;
         bool cont = false;
+
+        if (!init_relevancy())
+            give_up = true;
+
         for (auto* e : m_solvers)
             switch (e->check()) {
             case sat::check_result::CR_CONTINUE: cont = true; break;
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index ab20d6b41..3fc3b6d56 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -25,6 +25,7 @@ Author:
 #include "sat/sat_extension.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"
+#include "sat/smt/sat_dual_solver.h"
 #include "sat/smt/euf_ackerman.h"
 #include "smt/params/smt_params.h"
 
@@ -37,14 +38,14 @@ namespace euf {
 
     class constraint {
     public:
-        enum class kind_t { conflict, eq, lit};
+        enum class kind_t { conflict, eq, lit };
     private:
         kind_t m_kind;
     public:
         constraint(kind_t k) : m_kind(k) {}
         kind_t kind() const { return m_kind; }
-        static constraint& from_idx(size_t z) { 
-            return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z)); 
+        static constraint& from_idx(size_t z) {
+            return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z));
         }
         size_t to_index() const { return sat::constraint_base::mem2base(this); }
     };
@@ -76,7 +77,7 @@ namespace euf {
             return reinterpret_cast<size_t>(UNTAG(size_t*, p));
         }
 
-        ast_manager&          m;
+        ast_manager& m;
         sat::sat_internalizer& si;
         smt_params            m_config;
         euf::egraph           m_egraph;
@@ -85,28 +86,29 @@ namespace euf {
         th_rewriter           m_rewriter;
         func_decl_ref_vector  m_unhandled_functions;
 
-        sat::solver*           m_solver { nullptr };
-        sat::lookahead*        m_lookahead { nullptr };
-        ast_manager*           m_to_m;
+        sat::solver* m_solver{ nullptr };
+        sat::lookahead* m_lookahead{ nullptr };
+        ast_manager* m_to_m;
         sat::sat_internalizer* m_to_si;
         scoped_ptr<euf::ackerman>   m_ackerman;
+        scoped_ptr<sat::dual_solver> m_dual_solver;
 
         ptr_vector<expr>                                m_var2expr;
         ptr_vector<size_t>                              m_explain;
-        unsigned                                        m_num_scopes { 0 };
+        unsigned                                        m_num_scopes{ 0 };
         unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
         scoped_ptr_vector<th_solver>                    m_solvers;
         ptr_vector<th_solver>                           m_id2solver;
 
-        constraint* m_conflict { nullptr };
-        constraint* m_eq       { nullptr };
-        constraint* m_lit      { nullptr };
+        constraint* m_conflict{ nullptr };
+        constraint* m_eq{ nullptr };
+        constraint* m_lit{ nullptr };
 
         // internalization
         bool visit(expr* e) override;
         bool visited(expr* e) override;
-        bool post_visit(expr* e, bool sign, bool root) override;        
+        bool post_visit(expr* e, bool sign, bool root) override;
         sat::literal attach_lit(sat::literal lit, expr* e);
         void add_distinct_axiom(app* e, euf::enode* const* args);
         void add_not_distinct_axiom(app* e, euf::enode* const* args);
@@ -117,7 +119,7 @@ namespace euf {
 
         // replay
         expr_ref_vector      m_reinit_exprs;
-        
+
         void start_reinit(unsigned num_scopes);
         void finish_reinit();
 
@@ -135,7 +137,7 @@ namespace euf {
         bool include_func_interp(func_decl* f);
         void register_macros(model& mdl);
         void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& mdl);
-        void collect_dependencies(deps_t& deps);        
+        void collect_dependencies(deps_t& deps);
         void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
 
         // solving
@@ -149,17 +151,24 @@ namespace euf {
         void log_antecedents(literal l, literal_vector const& r);
         void drat_log_decl(func_decl* f);
         obj_hashtable<ast> m_drat_asts;
-        
         bool m_drat_initialized{ false };
         void init_drat();
 
+        // relevancy
+        bool_vector m_relevant_expr_ids;
+        void ensure_dual_solver();
+        bool init_relevancy();
+
+
         // invariant
         void check_eqc_bool_assignment() const;
-        void check_missing_bool_enode_propagation() const; 
+        void check_missing_bool_enode_propagation() const;
         void check_missing_eq_propagation() const;
 
+        // diagnosis
         std::ostream& display_justification_ptr(std::ostream& out, size_t* j) const;
 
+        // constraints
         constraint& mk_constraint(constraint*& c, constraint::kind_t k);
         constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
         constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
@@ -168,25 +177,26 @@ namespace euf {
     public:
         solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p = params_ref());
 
-       ~solver() override {
-           if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
-           if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
-           if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
-       }
+        ~solver() override {
+            if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
+            if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
+            if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
+        }
 
-       struct scoped_set_translate {
-           solver& s;
-           scoped_set_translate(solver& s, ast_manager& m, sat::sat_internalizer& si) :
-               s(s) {
-               s.m_to_m = &m;
-               s.m_to_si = &si;
-           }
-           ~scoped_set_translate() {
-               s.m_to_m = &s.m;
-               s.m_to_si = &s.si;
-           }
-       };
+        struct scoped_set_translate {
+            solver& s;
+            scoped_set_translate(solver& s, ast_manager& m, sat::sat_internalizer& si) :
+                s(s) {
+                s.m_to_m = &m;
+                s.m_to_si = &si;
+            }
+            ~scoped_set_translate() {
+                s.m_to_m = &s.m;
+                s.m_to_si = &s.si;
+            }
+        };
 
+        // accessors
         sat::solver& s() { return *m_solver; }
         sat::solver const& s() const { return *m_solver; }
         sat::sat_internalizer& get_si() { return si; }
@@ -194,11 +204,11 @@ namespace euf {
         enode* get_enode(expr* e) { return m_egraph.find(e); }
         sat::literal expr2literal(expr* e) const { return literal(si.to_bool_var(e), false); }
         sat::literal enode2literal(enode* e) const { return expr2literal(e->get_expr()); }
-        smt_params const& get_config() { return m_config; }
+        smt_params const& get_config() const { return m_config; }
         region& get_region() { return m_trail.get_region(); }
         egraph& get_egraph() { return m_egraph; }
         template <typename C>
-        void push(C const& c) { m_trail.push(c);  }
+        void push(C const& c) { m_trail.push(c); }
         euf_trail_stack& get_trail_stack() { return m_trail; }
 
         void updt_params(params_ref const& p);
@@ -214,7 +224,7 @@ namespace euf {
         bool set_root(literal l, literal r) override;
         void flush_roots() override;
 
-        void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) override;
+        void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
         void add_antecedent(enode* a, enode* b);
         void asserted(literal l) override;
         sat::check_result check() override;
@@ -229,8 +239,8 @@ namespace euf {
         std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
         std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
         void collect_statistics(statistics& st) const override;
-        extension* copy(sat::solver* s) override;       
-        void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
+        extension* copy(sat::solver* s) override;
+        void find_mutexes(literal_vector& lits, vector<literal_vector>& mutexes) override;
         void gc() override;
         void pop_reinit() override;
         bool validate() override;
@@ -239,12 +249,12 @@ namespace euf {
         bool check_model(sat::model const& m) const override;
         unsigned max_var(unsigned w) const override;
 
-        bool use_drat() { return s().get_config().m_drat && (init_drat(), true);  }
+        bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
         sat::drat& get_drat() { return s().get_drat(); }
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
-                        std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
+            std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
 
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
 
@@ -262,10 +272,20 @@ namespace euf {
         bool is_shared(euf::enode* n) const;
         void drat_log_node(expr* n);
 
+        // relevancy
+        bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }
+        void add_root(unsigned n, sat::literal const* lits);
+        void add_aux(unsigned n, sat::literal const* lits);
+        void track_relevancy(sat::bool_var v);
+        bool is_relevant(expr* e) const { return m_relevant_expr_ids.get(e->get_id(), true); }
+        bool is_relevant(enode* n) const { return m_relevant_expr_ids.get(n->get_expr_id(), true); }
+
+        // model construction
         void update_model(model_ref& mdl);
 
-        func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }       
-    };    
+        // diagnostics
+        func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
+    };
 };
 
 inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) {
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
new file mode 100644
index 000000000..680cfd865
--- /dev/null
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -0,0 +1,96 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_dual_solver.cpp
+
+Abstract:
+
+    Solver for obtaining implicant.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#include "sat/smt/sat_dual_solver.h"
+
+namespace sat {
+
+    dual_solver::dual_solver(reslimit& l):
+        m_solver(params_ref(), l)
+    {}
+
+    void dual_solver::push() {
+        m_solver.user_push(); 
+        m_roots_lim.push_back(m_roots.size());     
+        m_tracked_lim.push_back(m_tracked_stack.size());
+    }
+
+    void dual_solver::pop(unsigned num_scopes) {
+        m_solver.user_pop(num_scopes);
+        unsigned old_sz = m_roots_lim.size() - num_scopes;
+        m_roots.shrink(m_roots_lim[old_sz]);
+        m_roots_lim.shrink(old_sz);
+        for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; ) 
+            m_is_tracked[v] = false; 
+        m_tracked_stack.shrink(m_tracked_lim[old_sz]);
+        m_tracked_lim.shrink(old_sz);
+    }
+
+    bool_var dual_solver::ext2var(bool_var v) {
+        bool_var w = m_ext2var.get(v, null_bool_var);
+        if (null_bool_var == w) {
+            w = m_solver.mk_var();
+            m_ext2var.setx(v, w, null_bool_var);
+            m_var2ext.setx(w, v, null_bool_var);
+        }
+        return w;
+    }
+
+    void dual_solver::track_relevancy(bool_var v) {
+        v = ext2var(v);
+        if (!m_is_tracked.get(v, false)) {
+            m_is_tracked.setx(v, true, false);
+            m_tracked_stack.push_back(v);
+        }
+    }
+
+    literal dual_solver::ext2lit(literal lit) {
+        return literal(ext2var(lit.var()), lit.sign());
+    }
+
+    literal dual_solver::lit2ext(literal lit) {
+        return literal(m_var2ext[lit.var()], lit.sign());
+    }
+
+    void dual_solver::add_root(literal lit, unsigned sz, literal const* clause) {
+        for (unsigned i = 0; i < sz; ++i)
+            m_solver.mk_clause(ext2lit(lit), ~ext2lit(clause[i]), status::input());
+        m_roots.push_back(~ext2lit(lit));
+    }
+
+    void dual_solver::add_aux(unsigned sz, literal const* clause) {
+        m_lits.reset();
+        for (unsigned i = 0; i < sz; ++i) 
+            m_lits.push_back(ext2lit(clause[i]));
+        m_solver.mk_clause(sz, m_lits.c_ptr(), status::input());
+    }
+
+    bool dual_solver::operator()(solver const& s) {
+        m_solver.user_push();
+        m_solver.add_clause(m_roots.size(), m_roots.c_ptr(), status::input());
+        m_lits.reset();
+        for (bool_var v : m_tracked_stack)
+            m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
+        lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
+        m_core.reset();
+        if (is_sat == l_false) 
+            for (literal lit : m_solver.get_core())
+                m_core.push_back(lit2ext(lit));
+        TRACE("euf", m_solver.display(tout << m_core << "\n"););
+        m_solver.user_pop(1);
+        return is_sat == l_false;
+    }
+}
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
new file mode 100644
index 000000000..374ecbf19
--- /dev/null
+++ b/src/sat/smt/sat_dual_solver.h
@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_dual_solver.h
+
+Abstract:
+
+    Solver for obtaining implicant.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#pragma once
+#include "sat/sat_solver.h"
+
+namespace sat {
+
+    class dual_solver {
+        solver          m_solver;
+        literal_vector  m_roots, m_lits, m_core;
+        bool_var_vector m_is_tracked;
+        unsigned_vector m_tracked_stack;
+        unsigned_vector m_ext2var;
+        unsigned_vector m_var2ext;
+        unsigned_vector m_roots_lim, m_tracked_lim;
+        void add_literal(literal lit);
+
+        bool_var ext2var(bool_var v);
+        bool_var var2ext(bool_var v);
+        literal  ext2lit(literal lit);
+        literal  lit2ext(literal lit);
+    public:
+        dual_solver(reslimit& l);
+        void push();
+        void pop(unsigned num_scopes);
+
+        /*
+        * track model relevancy for variable 
+        */
+        void track_relevancy(bool_var v);
+
+        /*
+        * Add a root clause from the input problem.
+        * At least one literal has to be satisfied in every root.
+        */
+        void add_root(literal lit, unsigned sz, literal const* clause);
+
+        /*
+        * Add auxiliary clauses that originate from compiling definitions.
+        */
+        void add_aux(unsigned sz, literal const* clause);
+
+        /*
+        * Extract a minimized subset of relevant literals from a model for s.
+        */
+        bool operator()(solver const& s);
+
+        literal_vector const& core() const { return m_core; }
+    };
+}
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index 4e408fdab..8f2bad6fd 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -107,8 +107,6 @@ namespace euf {
         */
         virtual bool is_shared(theory_var v) const { return false; }
 
-
-
     };
 
     class th_euf_solver : public th_solver {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 3c001dbbe..174dc06fc 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -74,9 +74,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
     bool                        m_xor_solver;
-    bool                        m_euf;
-    bool                        m_drat;
+    bool                        m_euf { false };
+    bool                        m_drat { false };
     bool                        m_is_redundant { false };
+    bool                        m_top_level { false };
     sat::literal_vector         aig_lits;
     
     imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@@ -113,45 +114,60 @@ struct goal2sat::imp : public sat::sat_internalizer {
     sat::status mk_status() const {
         return sat::status::th(m_is_redundant, m.get_basic_family_id());
     }
+
+
+    bool top_level_relevant() {
+        return m_top_level && m_euf && ensure_euf()->relevancy_enabled();
+    }
+
+    void add_dual_def(unsigned n, sat::literal const* lits) {
+        if (top_level_relevant())
+            ensure_euf()->add_aux(n, lits);        
+    }
+
+    void add_dual_root(unsigned n, sat::literal const* lits) {
+        if (top_level_relevant())
+            ensure_euf()->add_root(n, lits);
+    }
     
     void mk_clause(sat::literal l) {
-        TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
-        m_solver.add_clause(1, &l, mk_status());
+        mk_clause(1, &l);
     }
 
     void mk_clause(sat::literal l1, sat::literal l2) {
-        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
-        m_solver.add_clause(l1, l2, mk_status());
+        sat::literal lits[2] = { l1, l2 };
+        mk_clause(2, lits);
     }
 
     void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
-        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
-        m_solver.add_clause(l1, l2, l3, mk_status());
+        sat::literal lits[3] = { l1, l2, l3 };
+        mk_clause(3, lits);
     }
 
-    void mk_clause(unsigned num, sat::literal * lits) {
-        TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
-        m_solver.add_clause(num, lits, mk_status());
+    void mk_clause(unsigned n, sat::literal * lits) {
+        TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
+        add_dual_def(n, lits);
+        m_solver.add_clause(n, lits, mk_status());
     }
 
     void mk_root_clause(sat::literal l) {
-        TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
-        m_solver.add_clause(1, &l, m_is_redundant ? mk_status() : sat::status::input());        
+        mk_root_clause(1, &l);
     }
 
     void mk_root_clause(sat::literal l1, sat::literal l2) {
-        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
-        m_solver.add_clause(l1, l2, m_is_redundant ? mk_status() : sat::status::input());
+        sat::literal lits[2] = { l1, l2 };
+        mk_root_clause(2, lits);
     }
 
     void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
-        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
-        m_solver.add_clause(l1, l2, l3, m_is_redundant ? mk_status() : sat::status::input());
+        sat::literal lits[3] = { l1, l2, l3 };
+        mk_root_clause(3, lits);
     }
 
-    void mk_root_clause(unsigned num, sat::literal * lits) {
-        TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
-        m_solver.add_clause(num, lits, m_is_redundant ? mk_status() : sat::status::input());
+    void mk_root_clause(unsigned n, sat::literal * lits) {
+        TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
+        add_dual_root(n, lits);
+        m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
     }
 
     sat::bool_var add_var(bool is_ext, expr* n) {
@@ -161,6 +177,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         v = m_solver.add_var(is_ext);
         log_node(n);
         log_def(v, n);
+        if (top_level_relevant() && !is_bool_op(n))
+            ensure_euf()->track_relevancy(v);
         return v;
     }
 
@@ -603,9 +621,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
         SASSERT(m_euf);
         TRACE("goal2sat", tout << "convert-euf " << mk_bounded_pp(e, m, 2) << " root " << root << "\n";);
         euf::solver* euf = ensure_euf();
-        sat::literal lit = euf->internalize(e, sign, root, m_is_redundant);
+        sat::literal lit;
+        {
+            flet<bool> _top(m_top_level, false);
+            lit = euf->internalize(e, sign, root, m_is_redundant);           
+        }
         if (lit == sat::null_literal)
             return;
+        if (top_level_relevant())
+            euf->track_relevancy(lit.var());
         if (root)
             mk_root_clause(lit);
         else
@@ -757,6 +781,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     sat::literal internalize(expr* n, bool redundant) override {
+        flet<bool> _top(m_top_level, false);
         unsigned sz = m_result_stack.size();
         (void)sz;
         SASSERT(n->get_ref_count() > 0);
@@ -797,6 +822,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
     
     void process(expr * n) {
+        flet<bool> _top(m_top_level, true);
         VERIFY(m_result_stack.empty());
         TRACE("goal2sat", tout << "assert: " << mk_bounded_pp(n, m, 3) << "\n";);
         process(n, true, m_is_redundant);
diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp
index af1702700..419d9e281 100644
--- a/src/shell/drat_frontend.cpp
+++ b/src/shell/drat_frontend.cpp
@@ -311,9 +311,6 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
             bool_var2expr.reserve(r.m_node_id+1);
             bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0]));
             break;
-        case dimacs::drat_record::tag_t::is_var_gc:
-            drat_checker.gc_var(r.m_node_id);
-            break;
         default:
             UNREACHABLE();
             break;
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index b3aa7d073..5c77c67c2 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -46,6 +46,7 @@ def_module_params(module_name='smt',
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
 	                  ('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'),
                           ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
+                          ('bv.delay', BOOL, True, 'delay internalize expensive bit-vector operations'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.cheap_eqs', BOOL, True, 'false - do not run, true - run cheap equality heuristic'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp
index 7afa00589..337af657f 100644
--- a/src/smt/params/theory_bv_params.cpp
+++ b/src/smt/params/theory_bv_params.cpp
@@ -27,6 +27,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
     m_bv_reflect = p.bv_reflect();
     m_bv_enable_int2bv2int = p.bv_enable_int2bv(); 
     m_bv_eq_axioms = p.bv_eq_axioms();
+    m_bv_delay = p.bv_delay();
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
@@ -40,4 +41,5 @@ void theory_bv_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_bv_eq_axioms);
     DISPLAY_PARAM(m_bv_blast_max_size);
     DISPLAY_PARAM(m_bv_enable_int2bv2int);
+    DISPLAY_PARAM(m_bv_delay);
 }
diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h
index 339799c81..1fc477c79 100644
--- a/src/smt/params/theory_bv_params.h
+++ b/src/smt/params/theory_bv_params.h
@@ -35,6 +35,7 @@ struct theory_bv_params {
     unsigned     m_bv_blast_max_size;
     bool         m_bv_enable_int2bv2int;
     bool         m_bv_watch_diseq;
+    bool         m_bv_delay;
     theory_bv_params(params_ref const & p = params_ref()):
         m_bv_mode(bv_solver_id::BS_BLASTER),
         m_hi_div0(false),
@@ -44,7 +45,8 @@ struct theory_bv_params {
         m_bv_eq_axioms(true),
         m_bv_blast_max_size(INT_MAX),
         m_bv_enable_int2bv2int(true),
-        m_bv_watch_diseq(false) {
+        m_bv_watch_diseq(false),
+        m_bv_delay(true) {
         updt_params(p);
     }
     
diff --git a/src/util/vector.h b/src/util/vector.h
index 1df5472f1..5a913b580 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -515,6 +515,18 @@ public:
         }
     }
 
+    void init(vector<T, CallDestructors> const& other) {
+        if (this == &other)
+            return;
+        reset();
+        append(other);
+    }
+
+    void init(SZ sz, T const* data) {
+        reset();
+        append(sz, data);
+    }
+
     T * c_ptr() const {
         return m_data;
     }
@@ -637,3 +649,14 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
 
 template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
+
+
+template<typename T>
+inline std::ostream& operator<<(std::ostream& out, vector<T> const& v) {
+    bool first = true;
+    for (auto const& t : v) {
+        if (first) first = false; else out << " ";
+        out << t;
+    }
+    return out;
+ }