diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
index 88f4f3dd6..d7da09826 100644
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@@ -4,6 +4,7 @@ z3_add_component(sat
     dimacs.cpp
     sat_asymm_branch.cpp
     sat_bdd.cpp
+    sat_big.cpp
     sat_clause.cpp
     sat_clause_set.cpp
     sat_clause_use_list.cpp
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 05dde2331..cd7f23576 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -3158,12 +3158,9 @@ namespace sat {
             if (w.is_binary_clause() && is_marked(w.get_literal())) {
                 ++m_stats.m_num_bin_subsumes;
                 // IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
-                if (w.is_learned()) {
+                if (!w.is_learned()) {
                     c1.set_learned(false);
                 }
-                else if (w.is_blocked()) {
-                    w.set_unblocked();
-                }
             }
             else {
                 if (it != it2) {
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 3a3184141..6d06a3a2e 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -19,7 +19,7 @@ Revision History:
 #include "sat/sat_asymm_branch.h"
 #include "sat/sat_asymm_branch_params.hpp"
 #include "sat/sat_solver.h"
-#include "sat/sat_scc.h"
+#include "sat/sat_big.h"
 #include "util/stopwatch.h"
 #include "util/trace.h"
 
@@ -42,9 +42,13 @@ namespace sat {
         asymm_branch & m_asymm_branch;
         stopwatch      m_watch;
         unsigned       m_elim_literals;
+        unsigned       m_elim_learned_literals;
+        unsigned       m_hidden_tautologies;
         report(asymm_branch & a):
             m_asymm_branch(a),
-            m_elim_literals(a.m_elim_literals) {
+            m_elim_literals(a.m_elim_literals),
+            m_elim_learned_literals(a.m_elim_learned_literals),
+            m_hidden_tautologies(a.m_hidden_tautologies) {
             m_watch.start();
         }
         
@@ -53,13 +57,36 @@ namespace sat {
             IF_VERBOSE(SAT_VB_LVL, 
                        verbose_stream() << " (sat-asymm-branch :elim-literals "
                        << (m_asymm_branch.m_elim_literals - m_elim_literals)
+                       << " :elim-learned-literals " << (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals)
+                       << " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
                        << " :cost " << m_asymm_branch.m_counter
                        << mem_stat()
                        << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
     };
 
-    void asymm_branch::process(scc* scc, clause_vector& clauses) {
+    bool asymm_branch::process(big* big) {
+        unsigned elim0 = m_elim_literals;
+        unsigned eliml0 = m_elim_learned_literals;
+        for (unsigned i = 0; i < m_asymm_branch_rounds; ++i) {
+            unsigned elim = m_elim_literals;
+            if (big) big->init_big(s, true);
+            process(big, s.m_clauses);
+            process(big, s.m_learned);
+            s.propagate(false); 
+            if (s.m_inconsistent)
+                break;
+            //std::cout << "elim: " << m_elim_literals - elim << "\n";
+            if (m_elim_literals == elim)
+                break;
+        }
+        //std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
+        //std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
+        return m_elim_literals > elim0;
+    }
+
+
+    void asymm_branch::process(big* big, clause_vector& clauses) {
         int64 limit = -m_asymm_branch_limit;
         std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
         m_counter -= clauses.size();
@@ -83,7 +110,7 @@ namespace sat {
                 }
                 s.checkpoint();
                 clause & c = *(*it);
-                if (scc ? !process_sampled(*scc, c) : !process(c)) {
+                if (big ? !process_sampled(*big, c) : !process(c)) {
                     continue; // clause was removed
                 }
                 *it2 = *it;
@@ -119,25 +146,23 @@ namespace sat {
         TRACE("asymm_branch_detail", s.display(tout););
         report rpt(*this);
         svector<char> saved_phase(s.m_phase);
-        if (m_asymm_branch) {
-            m_counter  = 0; 
-            process(nullptr, s.m_clauses);
-            m_counter = -m_counter;
-        }
-        if (m_asymm_branch_sampled) {
-            scc scc(s, m_params);
-            while (true) {
-                unsigned elim = m_elim_literals;
-                scc.init_big(true);
-                process(&scc, s.m_clauses);
-                process(&scc, s.m_learned);
-                s.propagate(false); 
-                if (s.m_inconsistent)
-                    break;
-                if (m_elim_literals == elim)
-                    break;
+
+        bool change = true;
+        unsigned counter = 0;
+        while (change && counter < 2) {
+            ++counter;
+            change = false;
+            if (m_asymm_branch_sampled) {
+                big big;
+                if (process(&big)) change = true;
+            }
+            if (m_asymm_branch) {
+                m_counter  = 0; 
+                if (process(nullptr)) change = true;
+                m_counter = -m_counter;
             }
         }
+
         s.m_phase = saved_phase;
         m_asymm_branch_limit *= 2;
         if (m_asymm_branch_limit > UINT_MAX)
@@ -163,35 +188,40 @@ namespace sat {
     }
 
     struct asymm_branch::compare_left {
-        scc& s;
-        compare_left(scc& s): s(s) {}
+        big& s;
+        compare_left(big& s): s(s) {}
         bool operator()(literal u, literal v) const {
             return s.get_left(u) < s.get_left(v);
         }
     };
 
-    void asymm_branch::sort(scc& scc, clause const& c) {
+    void asymm_branch::sort(big& big, clause const& c) {
+        sort(big, c.begin(), c.end());
+    }
+
+    void asymm_branch::sort(big& big, literal const* begin, literal const* end) {
         m_pos.reset(); m_neg.reset();
-        for (literal l : c) {
+        for (; begin != end; ++begin) {
+            literal l = *begin;
             m_pos.push_back(l);
             m_neg.push_back(~l);
         }
-        compare_left cmp(scc);
+        compare_left cmp(big);
         std::sort(m_pos.begin(), m_pos.end(), cmp);
         std::sort(m_neg.begin(), m_neg.end(), cmp);
     }
 
-    bool asymm_branch::uhte(scc& scc, clause & c) {
+    bool asymm_branch::uhte(big& big, clause & c) {
         unsigned pindex = 0, nindex = 0;
         literal lpos = m_pos[pindex++];
         literal lneg = m_neg[nindex++];
         while (true) {
-            if (scc.get_left(lneg) > scc.get_left(lpos)) {
+            if (big.get_left(lneg) > big.get_left(lpos)) {
                 if (pindex == m_pos.size()) return false;
                 lpos = m_pos[pindex++];
             }
-            else if (scc.get_right(lneg) < scc.get_right(lpos) ||
-                     (m_pos.size() == 2 && (lpos == ~lneg || scc.get_parent(lpos) == lneg))) {
+            else if (big.get_right(lneg) < big.get_right(lpos) ||
+                     (m_pos.size() == 2 && (lpos == ~lneg || big.get_parent(lpos) == lneg))) {
                 if (nindex == m_neg.size()) return false;
                 lneg = m_neg[nindex++];
             }
@@ -202,25 +232,44 @@ namespace sat {
         return false;
     }
 
-   bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) {
-        int right = scc.get_right(m_pos.back());
-        m_to_delete.reset();
-        for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
-            literal lit = m_pos[i];
-            int right2 = scc.get_right(lit);
-            if (right2 > right) {
-                // lit => last, so lit can be deleted
-                m_to_delete.push_back(lit);
+    void asymm_branch::minimize(big& big, literal_vector& lemma) {
+        big.ensure_big(s, true);
+        sort(big, lemma.begin(), lemma.end());
+        uhle(big);
+        if (!m_to_delete.empty()) {
+            unsigned j = 0;
+            for (unsigned i = 0; i < lemma.size(); ++i) {
+                literal l = lemma[i];
+                if (!m_to_delete.contains(l)) {
+                    lemma[j++] = l;
+                }
             }
-            else {
-                right = right2;
+            // std::cout << lemma.size() << " -> " << j << "\n";
+            lemma.shrink(j);
+        }
+    }
+
+    void asymm_branch::uhle(big& big) {
+        m_to_delete.reset();
+        if (m_to_delete.empty()) {
+            int right = big.get_right(m_pos.back());
+            for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
+                literal lit = m_pos[i];
+                int right2 = big.get_right(lit);
+                if (right2 > right) {
+                    // lit => last, so lit can be deleted
+                    m_to_delete.push_back(lit);
+                }
+                else {
+                    right = right2;
+                }
             }
         }
         if (m_to_delete.empty()) {
-            right = scc.get_right(m_neg[0]);
+            int right = big.get_right(m_neg[0]);
             for (unsigned i = 1; i < m_neg.size(); ++i) {
                 literal lit = m_neg[i];
-                int right2 = scc.get_right(lit);
+                int right2 = big.get_right(lit);
                 if (right > right2) {
                     // ~first => ~lit
                     m_to_delete.push_back(~lit);
@@ -230,6 +279,10 @@ namespace sat {
                 }
             }
         }
+    }
+
+    bool asymm_branch::uhle(scoped_detach& scoped_d, big& big, clause & c) {
+        uhle(big);
         if (!m_to_delete.empty()) {
             unsigned j = 0;
             for (unsigned i = 0; i < c.size(); ++i) {
@@ -299,10 +352,13 @@ namespace sat {
         return re_attach(scoped_d, c, new_sz);
     }
 
-   bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
-       m_elim_literals += c.size() - new_sz;
-       switch(new_sz) {
-       case 0:
+    bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
+        m_elim_literals += c.size() - new_sz;
+        if (c.is_learned()) {
+            m_elim_learned_literals += c.size() - new_sz; 
+        }
+        switch(new_sz) {
+        case 0:
             s.set_conflict(justification());
             return false;
         case 1:
@@ -314,7 +370,7 @@ namespace sat {
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
-            s.mk_bin_clause(c[0], c[1], false);
+            s.mk_bin_clause(c[0], c[1], c.is_learned());
             scoped_d.del_clause();
             SASSERT(s.m_qhead == s.m_trail.size());
             return false;
@@ -327,16 +383,17 @@ namespace sat {
         }
     }
 
-    bool asymm_branch::process_sampled(scc& scc, clause & c) {
+    bool asymm_branch::process_sampled(big& big, clause & c) {
         scoped_detach scoped_d(s, c);
-        sort(scc, c);
+        sort(big, c);
 #if 0
-        if (uhte(scc, c)) {
+        if (uhte(big, c)) {
+            ++m_hidden_tautologies;
             scoped_d.del_clause();
             return false;
         }
 #endif
-        return uhle(scoped_d, scc, c);        
+        return uhle(scoped_d, big, c);        
     }
 
     bool asymm_branch::process(clause & c) {
@@ -368,7 +425,7 @@ namespace sat {
         // clause must not be used for propagation
         scoped_detach scoped_d(s, c);
         unsigned new_sz = c.size();
-        unsigned flip_position = 2 + m_rand(c.size() - 2); // don't flip on the watch literals.
+        unsigned flip_position = m_rand(c.size()); 
         bool found_conflict = flip_literal_at(c, flip_position, new_sz);
         SASSERT(!s.inconsistent());
         SASSERT(s.scope_lvl() == 0);
@@ -386,11 +443,12 @@ namespace sat {
     
     void asymm_branch::updt_params(params_ref const & _p) {
         sat_asymm_branch_params p(_p);
-        m_asymm_branch        = p.asymm_branch();
-        m_asymm_branch_delay = p.asymm_branch_delay();
+        m_asymm_branch         = p.asymm_branch();
+        m_asymm_branch_rounds  = p.asymm_branch_rounds();
+        m_asymm_branch_delay   = p.asymm_branch_delay();
         m_asymm_branch_sampled = p.asymm_branch_sampled();
-        m_asymm_branch_limit  = p.asymm_branch_limit();
-        m_asymm_branch_all    = p.asymm_branch_all();
+        m_asymm_branch_limit   = p.asymm_branch_limit();
+        m_asymm_branch_all     = p.asymm_branch_all();
         if (m_asymm_branch_limit > UINT_MAX)
             m_asymm_branch_limit = UINT_MAX;
     }
@@ -401,10 +459,13 @@ namespace sat {
     
     void asymm_branch::collect_statistics(statistics & st) const {
         st.update("elim literals", m_elim_literals);
+        st.update("hidden tautologies", m_hidden_tautologies);
     }
 
     void asymm_branch::reset_statistics() {
         m_elim_literals = 0;
+        m_elim_learned_literals = 0;
+        m_hidden_tautologies = 0;
     }
 
 };
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index 4510aaddf..b18c549ac 100644
--- a/src/sat/sat_asymm_branch.h
+++ b/src/sat/sat_asymm_branch.h
@@ -20,7 +20,7 @@ Revision History:
 #define SAT_ASYMM_BRANCH_H_
 
 #include "sat/sat_types.h"
-#include "sat/sat_scc.h"
+#include "sat/sat_big.h"
 #include "util/statistics.h"
 #include "util/params.h"
 
@@ -39,6 +39,7 @@ namespace sat {
         
         // config
         bool       m_asymm_branch;
+        unsigned   m_asymm_branch_rounds;
         unsigned   m_asymm_branch_delay;
         bool       m_asymm_branch_sampled;
         bool       m_asymm_branch_propagate;
@@ -47,25 +48,32 @@ namespace sat {
 
         // stats
         unsigned   m_elim_literals;
+        unsigned   m_elim_learned_literals;
+        unsigned   m_hidden_tautologies;
 
-        literal_vector m_pos, m_neg; // literals (complements of literals) in clauses sorted by discovery time (m_left in scc).
+        literal_vector m_pos, m_neg; // literals (complements of literals) in clauses sorted by discovery time (m_left in BIG).
         literal_vector m_to_delete;
        
         struct compare_left;
 
-        void sort(scc & scc, clause const& c);
+        void sort(big& big, literal const* begin, literal const* end);
+        void sort(big & big, clause const& c);
 
-        bool uhle(scoped_detach& scoped_d, scc & scc, clause & c);
+        bool uhle(scoped_detach& scoped_d, big & big, clause & c);
 
-        bool uhte(scc & scc, clause & c);
+        void uhle(big & big);
+
+        bool uhte(big & big, clause & c);
 
         bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz);
 
+        bool process(big* big);
+
         bool process(clause & c);
 
-        bool process_sampled(scc& scc, clause & c);
+        bool process_sampled(big& big, clause & c);
 
-        void process(scc* scc, clause_vector & c);
+        void process(big* big, clause_vector & c);
         
         bool process_all(clause & c);
         
@@ -86,6 +94,8 @@ namespace sat {
         void collect_statistics(statistics & st) const;
         void reset_statistics();
 
+        void minimize(big& big, literal_vector& lemma);
+
         void init_search() { m_calls = 0; }
 
         inline void dec(unsigned c) { m_counter -= c; }
diff --git a/src/sat/sat_asymm_branch_params.pyg b/src/sat/sat_asymm_branch_params.pyg
index a457220be..0fd19d500 100644
--- a/src/sat/sat_asymm_branch_params.pyg
+++ b/src/sat/sat_asymm_branch_params.pyg
@@ -2,6 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_asymm_branch_params',
                   export=True,
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
+                          ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
                           ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
                           ('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'),
                           ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
new file mode 100644
index 000000000..aa4a62745
--- /dev/null
+++ b/src/sat/sat_big.cpp
@@ -0,0 +1,133 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_big.cpp
+
+Abstract:
+
+    binary implication graph structure.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-12-13.
+
+Revision History:
+
+--*/
+#include "sat/sat_big.h"
+#include "sat/sat_solver.h"
+
+namespace sat {
+
+    big::big() {}
+
+    void big::init_big(solver& s, bool learned) {
+        m_num_vars = s.num_vars();
+        unsigned num_lits = m_num_vars * 2;
+        m_dag.reset();
+        m_roots.reset();
+        m_dag.resize(num_lits, 0);
+        m_roots.resize(num_lits, true);
+        literal_vector lits;
+        SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
+        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
+            literal u = to_literal(l_idx);
+            if (s.was_eliminated(u.var())) 
+                continue;
+            auto& edges = m_dag[l_idx];
+            for (watched const& w : s.get_wlist(l_idx)) {
+                if (learned ? w.is_binary_clause() : w.is_binary_non_learned_clause()) {
+                    literal v = w.get_literal();
+                    m_roots[v.index()] = false;
+                    edges.push_back(v);
+                }
+            }
+            shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
+        }
+        init_dfs_num(learned);
+    }
+
+    struct big::pframe {
+        literal m_parent;
+        literal m_child;
+        pframe(literal p, literal c):
+            m_parent(p), m_child(c) {}
+        literal child() const { return m_child; }
+        literal parent() const { return m_parent; }
+    };
+
+    void big::init_dfs_num(bool learned) {
+        unsigned num_lits = m_num_vars * 2;
+        m_left.reset();
+        m_right.reset();
+        m_root.reset();
+        m_parent.reset();
+        m_left.resize(num_lits, 0);
+        m_right.resize(num_lits, -1);
+        m_root.resize(num_lits, null_literal);
+        m_parent.resize(num_lits, null_literal);
+        for (unsigned i = 0; i < num_lits; ++i) {
+            m_root[i]   = to_literal(i);
+            m_parent[i] = to_literal(i);            
+        }
+        svector<pframe> todo;
+        // retrieve literals that have no predecessors
+        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
+            literal u(to_literal(l_idx));
+            if (m_roots[u.index()]) {
+                todo.push_back(pframe(null_literal, u));
+            }
+        }
+        shuffle<pframe>(todo.size(), todo.c_ptr(), m_rand);
+        int dfs_num = 0;
+        while (!todo.empty()) {
+            literal u = todo.back().child();
+            if (m_left[u.index()] > 0) {
+                // already visited
+                if (m_right[u.index()] < 0) {
+                    m_right[u.index()] = ++dfs_num;
+                }
+                todo.pop_back();
+            }
+            else {
+                SASSERT(m_left[u.index()] == 0);
+                m_left[u.index()] = ++dfs_num;
+                literal p = todo.back().parent();
+                if (p != null_literal) {
+                    m_root[u.index()] = m_root[p.index()];
+                    m_parent[u.index()] = p;
+                }
+                for (literal v : m_dag[u.index()]) {
+                    if (m_left[v.index()] == 0) {
+                        todo.push_back(pframe(u, v));
+                    }
+                }
+            }
+        }
+        for (unsigned i = 0; i < num_lits; ++i) {
+            if (m_right[i] < 0) {
+                VERIFY(m_left[i] == 0);
+                m_left[i]  = ++dfs_num;
+                m_right[i] = ++dfs_num;
+            }
+        }
+        for (unsigned i = 0; i < num_lits; ++i) {
+            VERIFY(m_left[i] < m_right[i]);
+        }
+    }
+
+    void big::display(std::ostream& out) const {
+        unsigned idx = 0;
+        for (auto& next : m_dag) {
+            if (!next.empty()) {
+                out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n";
+            }
+            ++idx;
+        }
+    }
+
+
+
+};
diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h
new file mode 100644
index 000000000..ca9f131eb
--- /dev/null
+++ b/src/sat/sat_big.h
@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    sat_big.h
+
+Abstract:
+
+    binary implication graph structure.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-12-13.
+
+Revision History:
+
+--*/
+#ifndef SAT_BIG_H_
+#define SAT_BIG_H_
+
+#include "sat/sat_types.h"
+#include "util/statistics.h"
+#include "util/params.h"
+
+namespace sat {
+    class solver;
+
+    class big {
+        random_gen             m_rand;
+        unsigned               m_num_vars;
+        vector<literal_vector> m_dag;
+        svector<bool>          m_roots;
+        svector<int>           m_left, m_right;
+        literal_vector         m_root, m_parent;
+
+        void init_dfs_num(bool learned);
+        struct pframe;
+
+    public:
+
+        big();
+        void init_big(solver& s, bool learned);
+        void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); }
+        int get_left(literal l) const { return m_left[l.index()]; }
+        int get_right(literal l) const { return m_right[l.index()]; }
+        literal get_parent(literal l) const { return m_parent[l.index()]; }
+        literal get_root(literal l) const { return m_root[l.index()]; }
+        bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }        
+        bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
+        void display(std::ostream& out) const;
+    };
+};
+
+#endif
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 584433cc1..379888b15 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -85,9 +85,9 @@ namespace sat{
         // eliminate variable
         simp.m_pos_cls.reset();
         simp.m_neg_cls.reset();
-        simp.collect_clauses(pos_l, simp.m_pos_cls, false);
-        simp.collect_clauses(neg_l, simp.m_neg_cls, false);
-        //VERIFY(!s.is_external(v));
+        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);
@@ -295,7 +295,7 @@ namespace sat{
     bool elim_vars::mark_literals(literal lit) {
         watch_list& wl = simp.get_wlist(lit);
         for (watched const& w : wl) {
-            if (w.is_binary_unblocked_clause()) {
+            if (w.is_binary_non_learned_clause()) {
                 mark_var(w.get_literal().var());
             }
         }
@@ -321,7 +321,7 @@ namespace sat{
         bdd result = m.mk_true();
         watch_list& wl = simp.get_wlist(~lit);
         for (watched const& w : wl) {
-            if (w.is_binary_unblocked_clause()) {
+            if (w.is_binary_non_learned_clause()) {
                 result &= (mk_literal(lit) || mk_literal(w.get_literal()));
             }
         }        
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index 81db67dc7..bdc72602d 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -34,13 +34,11 @@ namespace sat {
     
     // for nary clauses
     static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
-        watch_list::const_iterator it  = wlist.begin();
-        watch_list::const_iterator end = wlist.end();
-        for (; it != end; ++it) {
-            if (it->is_clause()) {
-                if (it->get_clause_offset() == cls_off) {
+        for (watched const& w : wlist) {
+            if (w.is_clause()) {
+                if (w.get_clause_offset() == cls_off) {
                     // the blocked literal must be in the clause.
-                    SASSERT(c.contains(it->get_blocked_literal()));
+                    SASSERT(c.contains(w.get_blocked_literal()));
                     return true;
                 }
             }
@@ -96,13 +94,13 @@ namespace sat {
             }
             
             // the first two literals must be watched.
-           VERIFY(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
+            VERIFY(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c)));
             VERIFY(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c)));
         }
         return true;
     }
 
-    bool integrity_checker::check_clauses(clause * const * begin, clause * const * end) const {
+    bool integrity_checker::check_clauses(clause * const * begin, clause * const * end) const {        
         for (clause * const * it = begin; it != end; ++it) {
             SASSERT(check_clause(*(*it)));
         }
@@ -152,49 +150,54 @@ namespace sat {
         return true;
     }
 
+    bool integrity_checker::check_watches(literal l) const {
+        return check_watches(l, s.get_wlist(~l));
+    }
+
+    bool integrity_checker::check_watches(literal l, watch_list const& wlist) const {
+        for (watched const& w : wlist) {
+            switch (w.get_kind()) {
+            case watched::BINARY:
+                SASSERT(!s.was_eliminated(w.get_literal().var()));
+                CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())),
+                       tout << "l: " << l << " l2: " << w.get_literal() << "\n"; 
+                       tout << "was_eliminated1: " << s.was_eliminated(l.var());
+                       tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var());
+                       tout << " learned: " << w.is_learned() << "\n";
+                       sat::display_watch_list(tout, s.m_cls_allocator, wlist);
+                       tout << "\n";
+                       sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~(w.get_literal())));
+                       tout << "\n";);
+                VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
+                break;
+            case watched::TERNARY:
+                VERIFY(!s.was_eliminated(w.get_literal1().var()));
+                VERIFY(!s.was_eliminated(w.get_literal2().var()));
+                VERIFY(w.get_literal1().index() < w.get_literal2().index());
+                break;
+            case watched::CLAUSE:
+                SASSERT(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed());
+                break;
+            default:
+                break;
+            }
+        }
+        return true;
+    }
+
     bool integrity_checker::check_watches() const {
-        DEBUG_CODE(
-        vector<watch_list>::const_iterator it  = s.m_watches.begin();
-        vector<watch_list>::const_iterator end = s.m_watches.end();
-        for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
-            literal l = ~to_literal(l_idx);            
-            watch_list const & wlist = *it;
+        unsigned l_idx = 0;
+        for (watch_list const& wlist : s.m_watches) {
+            literal l = ~to_literal(l_idx++);            
             CTRACE("sat_bug", 
                    s.was_eliminated(l.var()) && !wlist.empty(),
                    tout << "l: " << l << "\n";
                    s.display_watches(tout);
                    s.display(tout););
             SASSERT(!s.was_eliminated(l.var()) || wlist.empty());
-            watch_list::const_iterator it2  = wlist.begin();
-            watch_list::const_iterator end2 = wlist.end();
-            for (; it2 != end2; ++it2) {
-                switch (it2->get_kind()) {
-                case watched::BINARY:
-                    SASSERT(!s.was_eliminated(it2->get_literal().var()));
-                    CTRACE("sat_watched_bug", !s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())),
-                           tout << "l: " << l << " l2: " << it2->get_literal() << "\n"; 
-                           tout << "was_eliminated1: " << s.was_eliminated(l.var());
-                           tout << " was_eliminated2: " << s.was_eliminated(it2->get_literal().var());
-                           tout << " learned: " << it2->is_learned() << "\n";
-                           sat::display_watch_list(tout, s.m_cls_allocator, wlist);
-                           tout << "\n";
-                           sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal())));
-                           tout << "\n";);
-                        SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())));
-                    break;
-                case watched::TERNARY:
-                    SASSERT(!s.was_eliminated(it2->get_literal1().var()));
-                    SASSERT(!s.was_eliminated(it2->get_literal2().var()));
-                    SASSERT(it2->get_literal1().index() < it2->get_literal2().index());
-                    break;
-                case watched::CLAUSE:
-                    SASSERT(!s.m_cls_allocator.get_clause(it2->get_clause_offset())->was_removed());
-                    break;
-                default:
-                    break;
-                }
-            }
-        });
+            if (!check_watches(l, wlist)) 
+                return false;
+        }        
         return true;
     }
 
@@ -211,16 +214,12 @@ namespace sat {
 
     bool integrity_checker::check_disjoint_clauses() const {
         uint_set ids;
-        clause_vector::const_iterator it  = s.m_clauses.begin();
-        clause_vector::const_iterator end = s.m_clauses.end();
-        for (; it != end; ++it) {
-            ids.insert((*it)->id());
+        for (clause* cp : s.m_clauses) {
+            ids.insert(cp->id());
         }
-        it = s.m_learned.begin();
-        end = s.m_learned.end();
-        for (; it != end; ++it) {
-            if (ids.contains((*it)->id())) {
-                TRACE("sat", tout << "Repeated clause: " << (*it)->id() << "\n";);
+        for (clause* cp : s.m_learned) {
+            if (ids.contains(cp->id())) {
+                TRACE("sat", tout << "Repeated clause: " << cp->id() << "\n";);
                 return false;
             }
         }
diff --git a/src/sat/sat_integrity_checker.h b/src/sat/sat_integrity_checker.h
index 640fce068..10fd2203c 100644
--- a/src/sat/sat_integrity_checker.h
+++ b/src/sat/sat_integrity_checker.h
@@ -21,6 +21,7 @@ Revision History:
 #define SAT_INTEGRITY_CHECKER_H_
 
 #include "sat/sat_types.h"
+#include "sat/sat_watched.h"
 
 namespace sat {
     class integrity_checker {
@@ -35,6 +36,8 @@ namespace sat {
         bool check_assignment() const;
         bool check_bool_vars() const;
         bool check_watches() const;
+        bool check_watches(literal l, watch_list const& wlist) const;
+        bool check_watches(literal l) const;
         bool check_reinit_stack() const;
         bool check_disjoint_clauses() const;
         bool operator()() const;
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 726fda7f4..376d607ab 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -302,7 +302,7 @@ namespace sat {
                 literal l1 = ~to_literal(l_idx);
                 watch_list const & wlist = s.m_watches[l_idx];
                 for (watched const& w : wlist) {
-                    if (!w.is_binary_unblocked_clause())
+                    if (!w.is_binary_non_learned_clause())
                         continue;
                     literal l2 = w.get_literal();
                     if (l1.index() > l2.index()) 
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 0632d3076..31a9f12e9 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2372,8 +2372,8 @@ namespace sat {
             }
         }
 
-        scc scc(m_s, m_s.m_params);
-        scc.init_big(true);
+        big big;
+        big.init_big(m_s, true);
         svector<std::pair<literal, literal>> candidates;
 
         unsigned_vector bin_size(num_lits);
@@ -2390,14 +2390,14 @@ namespace sat {
                 if (v == get_parent(v) && 
                     !m_s.was_eliminated(v.var()) && 
                     !imp.contains(std::make_pair(u.index(), v.index())) && 
-                    !scc.reaches(u, v)) {
+                    !big.connected(u, v)) {
                     candidates.push_back(std::make_pair(u, v));
                 }
             }
         }
 
         for (unsigned count = 0; count < 5; ++count) {
-            scc.init_big(true);
+            big.init_big(m_s, true);
             unsigned k = 0;
             union_find_default_ctx ufctx;
             union_find<union_find_default_ctx> uf(ufctx);
@@ -2405,7 +2405,7 @@ namespace sat {
             for (unsigned j = 0; j < candidates.size(); ++j) {
                 literal u = candidates[j].first;
                 literal v = candidates[j].second;
-                if (!scc.reaches(u, v)) {
+                if (!big.connected(u, v)) {
                     if (uf.find(u.index()) != uf.find(v.index())) {
                         ++num_bins;
                         uf.merge(u.index(), v.index());
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 3fc5194f0..672e22512 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -45,6 +45,7 @@ def_module_params('sat',
                           ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'),
                           ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'),
                           ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'),
+                          ('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_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 59c53304d..960174e79 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -234,102 +234,10 @@ namespace sat {
         return to_elim.size();
     }
 
-    void scc::init_big(bool learned) {
-        unsigned num_lits = m_solver.num_vars() * 2;
-        m_dag.reset();
-        m_roots.reset();
-        m_dag.resize(num_lits, 0);
-        m_roots.resize(num_lits, true);
-        SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
-        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
-            literal u = to_literal(l_idx);
-            if (m_solver.was_eliminated(u.var())) 
-                continue;
-            auto& edges = m_dag[l_idx];
-            for (watched const& w : m_solver.m_watches[l_idx]) {
-                if (learned ? w.is_binary_clause() : w.is_binary_unblocked_clause()) {
-                    literal v = w.get_literal();
-                    m_roots[v.index()] = false;
-                    edges.push_back(v);
-                }
-            }
-            shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
-        }
-        init_dfs_num(learned);
-    }
-
-    struct scc::pframe {
-        literal m_parent;
-        literal m_child;
-        pframe(literal p, literal c):
-            m_parent(p), m_child(c) {}
-        literal child() const { return m_child; }
-        literal parent() const { return m_parent; }
-    };
-
-    void scc::init_dfs_num(bool learned) {
-        unsigned num_lits = m_solver.num_vars() * 2;
-        m_left.reset();
-        m_right.reset();
-        m_root.reset();
-        m_parent.reset();
-        m_left.resize(num_lits, 0);
-        m_right.resize(num_lits, -1);
-        m_root.resize(num_lits, null_literal);
-        m_parent.resize(num_lits, null_literal);
-        for (unsigned i = 0; i < num_lits; ++i) {
-            m_root[i]   = to_literal(i);
-            m_parent[i] = to_literal(i);            
-        }
-        svector<pframe> todo;
-        // retrieve literals that have no predecessors
-        for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
-            literal u(to_literal(l_idx));
-            if (m_roots[u.index()]) {
-                todo.push_back(pframe(null_literal, u));
-            }
-        }
-        shuffle<pframe>(todo.size(), todo.c_ptr(), m_rand);
-        int dfs_num = 0;
-        while (!todo.empty()) {
-            literal u = todo.back().child();
-            if (m_left[u.index()] > 0) {
-                // already visited
-                if (m_right[u.index()] < 0) {
-                    m_right[u.index()] = ++dfs_num;
-                }
-                todo.pop_back();
-            }
-            else {
-                SASSERT(m_left[u.index()] == 0);
-                m_left[u.index()] = ++dfs_num;
-                literal p = todo.back().parent();
-                if (p != null_literal) {
-                    m_root[u.index()] = m_root[p.index()];
-                    m_parent[u.index()] = p;
-                }
-                for (literal v : m_dag[u.index()]) {
-                    if (m_left[v.index()] == 0) {
-                        todo.push_back(pframe(u, v));
-                    }
-                }
-            }
-        }
-        for (unsigned i = 0; i < num_lits; ++i) {
-            if (m_right[i] < 0) {
-                VERIFY(m_left[i] == 0);
-                m_left[i]  = ++dfs_num;
-                m_right[i] = ++dfs_num;
-            }
-        }
-        for (unsigned i = 0; i < num_lits; ++i) {
-            VERIFY(m_left[i] < m_right[i]);
-        }
-    }
-
     unsigned scc::reduce_tr(bool learned) {        
         unsigned num_lits = m_solver.num_vars() * 2;
         init_big(learned);
+        
         unsigned idx = 0;
         unsigned elim = m_num_elim_bin;
         for (watch_list & wlist : m_solver.m_watches) {
@@ -343,6 +251,7 @@ namespace sat {
                     literal v = w.get_literal();
                     if (reaches(u, v) && u != get_parent(v)) {
                         ++m_num_elim_bin;
+                        m_solver.get_wlist(~v).erase(watched(~u, w.is_learned()));
                     }
                     else {
                         *itprev = *it;
diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h
index 84858ca27..5e61e557e 100644
--- a/src/sat/sat_scc.h
+++ b/src/sat/sat_scc.h
@@ -19,9 +19,10 @@ Revision History:
 #ifndef SAT_SCC_H_
 #define SAT_SCC_H_
 
-#include "sat/sat_types.h"
 #include "util/statistics.h"
 #include "util/params.h"
+#include "sat/sat_types.h"
+#include "sat/sat_big.h"
 
 namespace sat {
     class solver;
@@ -35,24 +36,12 @@ namespace sat {
         // stats
         unsigned   m_num_elim;
         unsigned   m_num_elim_bin;
-        random_gen m_rand;
 
-        // BIG state:
-
-        vector<literal_vector> m_dag;
-        svector<bool>          m_roots;
-        svector<int>           m_left, m_right;
-        literal_vector         m_root, m_parent;
+        big        m_big;
 
         void reduce_tr();
         unsigned reduce_tr(bool learned);
 
-        void init_dfs_num(bool learned);
-
-        struct pframe;
-
-        bool reaches_aux(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } 
-
     public:
 
         scc(solver & s, params_ref const & p);
@@ -67,13 +56,16 @@ namespace sat {
         /*
           \brief create binary implication graph and associated data-structures to check transitivity.
          */
-        void init_big(bool learned);
-        void ensure_big(bool learned) { if (m_left.empty()) init_big(learned); }
-        int get_left(literal l) const { return m_left[l.index()]; }
-        int get_right(literal l) const { return m_right[l.index()]; }
-        literal get_parent(literal l) const { return m_parent[l.index()]; }
-        literal get_root(literal l) const { return m_root[l.index()]; }
-        bool reaches(literal u, literal v) const { return reaches_aux(u, v) || reaches_aux(~v, ~u); }        
+        void init_big(bool learned) { m_big.init_big(m_solver, learned); }
+        void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); }
+        int get_left(literal l) const { return m_big.get_left(l); }
+        int get_right(literal l) const { return m_big.get_right(l); }
+        literal get_parent(literal l) const { return m_big.get_parent(l); }
+        literal get_root(literal l) const { return m_big.get_root(l); }
+        bool reaches(literal u, literal v) const { return m_big.reaches(u, v); }        
+        bool connected(literal u, literal v) const {
+            return m_big.connected(u, v); 
+        }
     };
 };
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 6ceb53265..8a029e4ff 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -22,6 +22,7 @@ Revision History:
 #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"
 
@@ -99,16 +100,16 @@ namespace sat {
             (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled()); 
     }
     bool simplifier::acce_enabled() const { 
-        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; 
+        return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; 
     }
     bool simplifier::cce_enabled()  const { 
-        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); 
+        return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); 
     }
     bool simplifier::abce_enabled() const { 
-        return !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; 
+        return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; 
     }
     bool simplifier::bca_enabled()  const { 
-        return !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); 
+        return !s.m_ext && !m_incremental_mode && !s.tracking_assumptions() && m_bca && m_learned_in_use_lists && single_threaded(); 
     }
     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(); 
@@ -164,23 +165,11 @@ namespace sat {
     }
 
     inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
-        SASSERT(get_wlist(~l1).contains(watched(l2, learned)));
         get_wlist(~l1).erase(watched(l2, learned));
         m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
         m_sub_bin_todo.erase(bin_clause(l2, l1, learned));
     }
 
-    inline void simplifier::block_bin_clause_half(literal l1, literal l2) {
-        SASSERT(get_wlist(~l1).contains(watched(l2, false)));
-        for (watched & w : get_wlist(~l1)) {
-            if (w.get_literal() == l2) {
-                w.set_blocked();
-                break;
-            }
-        }
-        m_sub_bin_todo.erase(bin_clause(l1, l2, false));
-    }
-
     void simplifier::init_visited() {
         m_visited.reset();
         m_visited.resize(2*s.num_vars(), false);
@@ -213,6 +202,9 @@ namespace sat {
 
     void simplifier::operator()(bool learned) {
 
+        integrity_checker si(s);
+        si.check_watches();
+
         if (s.inconsistent())
             return;
         if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled())
@@ -239,6 +231,7 @@ namespace sat {
         if (bce_enabled() || abce_enabled() || bca_enabled()) {
             elim_blocked_clauses();
         }
+        si.check_watches();
 
         if (!learned) {
             m_num_calls++;
@@ -260,7 +253,7 @@ namespace sat {
             if (s.inconsistent())
                 return;
             if (!learned && elim_vars_enabled())
-                elim_vars();
+                elim_vars();            
             if (s.inconsistent())
                 return;
             if (!m_subsumption || m_sub_counter < 0)
@@ -276,12 +269,14 @@ namespace sat {
             cleanup_clauses(s.m_learned, true, vars_eliminated,  m_learned_in_use_lists);
             cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
         }
+        si.check_watches();
 
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
         finalize();
 
+        si.check_watches();
     }
 
     /**
@@ -736,7 +731,7 @@ namespace sat {
             // should not traverse wlist using iterators, since back_subsumption1 may add new binary clauses there
             for (unsigned j = 0; j < wlist.size(); j++) {
                 watched w  = wlist[j];
-                if (w.is_binary_unblocked_clause()) {
+                if (w.is_binary_non_learned_clause()) {
                     literal l2 = w.get_literal();
                     if (l.index() < l2.index()) {
                         m_dummy.set(l, l2, w.is_learned());
@@ -744,9 +739,9 @@ namespace sat {
                         back_subsumption1(c);
                         if (w.is_learned() && !c.is_learned()) {
                             SASSERT(wlist[j] == w);
-                            TRACE("mark_not_learned_bug",
+                            TRACE("set_not_learned_bug",
                                   tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";);
-                            wlist[j].mark_not_learned();
+                            wlist[j].set_not_learned();
                             mark_as_not_learned_core(get_wlist(~l2), l);
                         }
                         if (s.inconsistent())
@@ -763,7 +758,7 @@ namespace sat {
     void simplifier::mark_as_not_learned_core(watch_list & wlist, literal l2) {
         for (watched & w : wlist) {
             if (w.is_binary_clause() && w.get_literal() == l2 && w.is_learned()) {
-                w.mark_not_learned();
+                w.set_not_learned();
                 return;
             }
         }
@@ -983,14 +978,20 @@ namespace sat {
         }
 
         void operator()() {
+            integrity_checker si(s.s);
+            si.check_watches();
             if (s.bce_enabled())
                 block_clauses();
+            si.check_watches();
             if (s.abce_enabled())
                 cce<false>();
+            si.check_watches();
             if (s.cce_enabled()) 
                 cce<true>();
+            si.check_watches();
             if (s.bca_enabled())
                 bca();
+            si.check_watches();
         }
 
         void block_clauses() {
@@ -1013,12 +1014,14 @@ namespace sat {
 
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
-            model_converter::entry * new_entry = 0;
             if (!process_var(l.var())) {
                 return;
             }
+            integrity_checker si(s.s);
+            //si.check_watches();
             process_clauses(l);
             process_binary(l);
+            //si.check_watches();
         }
 
         void process_binary(literal l) {
@@ -1029,11 +1032,9 @@ namespace sat {
             watch_list::iterator it2 = it;
             watch_list::iterator end = wlist.end();
 
-#define INC() if (!s.m_retain_blocked_clauses) { *it2 = *it; it2++; }
-
             for (; it != end; ++it) {
-                if (!it->is_binary_clause() || it->is_blocked()) {
-                    INC();
+                if (!it->is_binary_non_learned_clause()) {
+                    *it2 = *it; it2++;
                     continue;
                 }
                 literal l2 = it->get_literal();
@@ -1043,11 +1044,11 @@ namespace sat {
                     s.m_num_blocked_clauses++;
                 }
                 else {
-                    INC();
+                    *it2 = *it; it2++;
                 }
                 s.unmark_visited(l2);
             }
-            if (!s.m_retain_blocked_clauses) wlist.set_end(it2);
+            wlist.set_end(it2);
         }
 
         void process_clauses(literal l) {
@@ -1094,7 +1095,7 @@ namespace sat {
             for (watched & w : s.get_wlist(l)) {
                 // when adding a blocked clause, then all non-learned clauses have to be considered for the
                 // resolution intersection.
-                bool process_bin = adding ? w.is_binary_clause() : w.is_binary_unblocked_clause();
+                bool process_bin = adding ? w.is_binary_clause() : w.is_binary_non_learned_clause();
                 if (process_bin) {
                     literal lit = w.get_literal();
                     if (s.is_marked(~lit) && lit != ~l) {
@@ -1146,7 +1147,7 @@ namespace sat {
         bool check_abce_tautology(literal l) {
             if (!process_var(l.var())) return false;
             for (watched & w : s.get_wlist(l)) {
-                if (w.is_binary_unblocked_clause()) {
+                if (w.is_binary_non_learned_clause()) {
                     literal lit = w.get_literal();
                     if (!s.is_marked(~lit) || lit == ~l) return false;
                 }
@@ -1176,7 +1177,7 @@ namespace sat {
             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_unblocked_clause()) {
+                    if (w.is_binary_non_learned_clause()) {
                         literal lit = w.get_literal();
                         if (!s.is_marked(lit) && !s.is_marked(~lit)) {
                             m_covered_clause.push_back(~lit);
@@ -1318,8 +1319,9 @@ namespace sat {
             watch_list::iterator end = wlist.end();
             model_converter::kind k;
             for (; it != end; ++it) {
-                if (!it->is_binary_clause() || it->is_blocked()) {
-                    INC();
+                if (!it->is_binary_non_learned_clause()) {
+                    *it2 = *it; 
+                    it2++;
                     continue;
                 }
                 literal l2 = it->get_literal();
@@ -1328,10 +1330,11 @@ namespace sat {
                     s.m_num_covered_clauses++;
                 }
                 else {
-                    INC();
+                    *it2 = *it; 
+                    it2++;
                 }
             }
-            if (!s.m_retain_blocked_clauses) wlist.set_end(it2);
+            wlist.set_end(it2);
         }
 
 
@@ -1382,24 +1385,18 @@ namespace sat {
         
         void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
             SASSERT(!s.is_external(blocked));
-            //VERIFY(!s.is_external(blocked));
             if (new_entry == 0) 
                 new_entry = &(mc.mk(k, blocked.var()));
             literal l2 = it->get_literal();
             TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
-            if (s.m_retain_blocked_clauses && !it->is_learned()) {
-                s.block_bin_clause_half(l2, l1);
-                s.block_bin_clause_half(l1, l2);
-            }
-            else {
-                s.remove_bin_clause_half(l2, l1, it->is_learned());
-            }
+            s.remove_bin_clause_half(l2, l1, it->is_learned());            
             m_queue.decreased(~l2);
         }
         
         void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+            literal l2 = it->get_literal();
             prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT);
-            mc.insert(*new_entry, l, it->get_literal());
+            mc.insert(*new_entry, l, l2);
         }
 
         void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) {
@@ -1431,19 +1428,12 @@ namespace sat {
             }
             for (literal l2 : m_intersection) {
                 l2.neg();
-                bool found = false;
-                for (watched w : s.get_wlist(~l)) {
-                    found = w.is_binary_clause() && l2 == w.get_literal();
-                    if (found) break;
-                }                
-                if (!found) {
+                watched* w = find_binary_watch(s.get_wlist(~l), l2);
+                if (!w) {
                     IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
-                    watched w1(l2, false);
-                    w1.set_blocked();
-                    watched w2(l, false);
-                    w2.set_blocked();
-                    s.get_wlist(~l).push_back(w1);
-                    s.get_wlist(~l2).push_back(w2);
+                    s.get_wlist(~l).push_back(watched(l2, true));
+                    VERIFY(!find_binary_watch(s.get_wlist(~l2), l));
+                    s.get_wlist(~l2).push_back(watched(l, true));
                     ++s.m_num_bca;
                 }
             }
@@ -1453,7 +1443,7 @@ namespace sat {
             watch_list & wlist = s.get_wlist(l);
             m_counter -= wlist.size();
             for (auto const& w : wlist) {
-                if (w.is_binary_unblocked_clause() && 
+                if (w.is_binary_non_learned_clause() && 
                     !s.is_marked(~w.get_literal()))
                     return false;
             }
@@ -1525,7 +1515,7 @@ namespace sat {
         unsigned r = 0;
         watch_list const & wlist = get_wlist(~l);
         for (auto & w : wlist) {
-            if (w.is_binary_unblocked_clause())
+            if (w.is_binary_non_learned_clause())
                 r++;
         }
         return r;
@@ -1574,10 +1564,10 @@ namespace sat {
     /**
        \brief Collect clauses and binary clauses containing l.
     */
-    void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) {
+    void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
         clause_use_list const & cs = m_use_list.get(l);
         for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
-            if (!it.curr().is_blocked() || include_blocked) {
+            if (!it.curr().is_blocked()) {
                 r.push_back(clause_wrapper(it.curr()));
                 SASSERT(r.back().size() == it.curr().size());
             }
@@ -1585,7 +1575,7 @@ namespace sat {
 
         watch_list & wlist = get_wlist(~l);
         for (auto & w : wlist) {
-            if (include_blocked ? w.is_binary_non_learned_clause() : w.is_binary_unblocked_clause()) {
+            if (w.is_binary_non_learned_clause()) {
                 r.push_back(clause_wrapper(l, w.get_literal()));
                 SASSERT(r.back().size() == 2);
             }
@@ -1643,27 +1633,26 @@ namespace sat {
     }
 
     void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
+        watched* w;
         watch_list & wlist1 = get_wlist(~l1);
         watch_list & wlist2 = get_wlist(~l2);
-        bool found = false;
-        for (watched& w : wlist1) {
-            if (w.is_binary_clause() && w.get_literal() == l2) {
-                if (w.is_learned()) w.mark_not_learned();
-                found = true;
-                break;
-            }
+        w = find_binary_watch(wlist1, l2);
+        if (w) {
+            if (w->is_learned())
+                w->set_not_learned();
+        }
+        else {
+            wlist1.push_back(watched(l2, false));
         }
-        if (!found) wlist1.push_back(watched(l2, false));
 
-        found = false;
-        for (watched& w : wlist2) {
-            if (w.is_binary_clause() && w.get_literal() == l1) {
-                if (w.is_learned()) w.mark_not_learned();
-                found = true;
-                break;
-            }
+        w = find_binary_watch(wlist2, l1);
+        if (w) {
+            if (w->is_learned())
+                w->set_not_learned();
+        }
+        else {
+            wlist2.push_back(watched(l1, false));
         }
-        if (!found) wlist2.push_back(watched(l1, false));
     }
 
     /**
@@ -1755,8 +1744,8 @@ namespace sat {
 
         m_pos_cls.reset();
         m_neg_cls.reset();
-        collect_clauses(pos_l, m_pos_cls, false);
-        collect_clauses(neg_l, m_neg_cls, false);
+        collect_clauses(pos_l, m_pos_cls);
+        collect_clauses(neg_l, m_neg_cls);
 
         TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
         unsigned before_clauses = num_pos + num_neg;
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 75703e34b..589061df5 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -132,7 +132,6 @@ namespace sat {
         void remove_clause(clause & c);
         void remove_clause(clause & c, literal l);
         void block_clause(clause & c);
-        void block_bin_clause_half(literal l1, literal l2);
         void unblock_clause(clause & c);
         void remove_bin_clause_half(literal l1, literal l2, bool learned);
 
@@ -185,7 +184,7 @@ namespace sat {
         unsigned get_num_unblocked_bin(literal l) const;
         unsigned get_to_elim_cost(bool_var v) const;
         void order_vars_for_elim(bool_var_vector & r);
-        void collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked);
+        void collect_clauses(literal l, clause_wrapper_vector & r);
         clause_wrapper_vector m_pos_cls;
         clause_wrapper_vector m_neg_cls;
         literal_vector m_new_cls;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 03f56a497..0e51c3332 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -137,10 +137,6 @@ namespace sat {
                                         
                     watched w1(l2, wi.is_learned());
                     watched w2(l, wi.is_learned());
-                    if (wi.is_blocked()) {
-                        w1.set_blocked();
-                        w2.set_blocked();
-                    }
                     m_watches[(~l).index()].push_back(w1);
                     m_watches[(~l2).index()].push_back(w2);
                 }
@@ -315,6 +311,19 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
+        watched* w0 = find_binary_watch(get_wlist(~l1), l2);
+        if (w0) {
+            if (w0->is_learned() && !learned) {
+                w0->set_not_learned();
+            }            
+            w0 = find_binary_watch(get_wlist(~l2), l1);
+        }
+        if (w0) {
+            if (w0->is_learned() && !learned) {
+                w0->set_not_learned();
+            }            
+            return;
+        }
         if (m_config.m_drat) 
             m_drat.add(l1, l2, learned);
         if (propagate_bin_clause(l1, l2)) {
@@ -324,8 +333,8 @@ namespace sat {
                 m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
         }
         m_stats.m_mk_bin_clause++;
-        m_watches[(~l1).index()].push_back(watched(l2, learned));
-        m_watches[(~l2).index()].push_back(watched(l1, learned));
+        get_wlist(~l1).push_back(watched(l2, learned));
+        get_wlist(~l2).push_back(watched(l1, learned));        
     }
 
     bool solver::propagate_bin_clause(literal l1, literal l2) {
@@ -1419,6 +1428,8 @@ namespace sat {
         if (m_conflicts_since_init < m_next_simplify) {
             return;
         }
+        integrity_checker si(*this);
+        si.check_watches();
         m_simplifications++;
         IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";);
 
@@ -1430,26 +1441,26 @@ namespace sat {
 
         m_cleaner();
         CASSERT("sat_simplify_bug", check_invariant());
+        si.check_watches();
 
         m_scc();
         CASSERT("sat_simplify_bug", check_invariant());
+        si.check_watches();
         
         m_simplifier(false);
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
-        
+		si.check_watches();
         if (!m_learned.empty()) {
             m_simplifier(true);
             CASSERT("sat_missed_prop", check_missed_propagation());
             CASSERT("sat_simplify_bug", check_invariant());
         }
-
         if (m_config.m_lookahead_simplify) {
             lookahead lh(*this);
             lh.simplify();
             lh.collect_statistics(m_aux_stats);
         }
-
         sort_watch_lits();
         CASSERT("sat_simplify_bug", check_invariant());
 
@@ -1575,7 +1586,7 @@ namespace sat {
             literal l = ~to_literal(l_idx);
             if (value_at(l, m) != l_true) {
                 for (watched const& w : wlist) {
-                    if (!w.is_binary_unblocked_clause())
+                    if (!w.is_binary_non_learned_clause())
                         continue;
                     literal l2 = w.get_literal();
                     if (value_at(l2, m) != l_true) {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 37290940d..ec6746763 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -169,6 +169,7 @@ namespace sat {
         friend class cleaner;
         friend class simplifier;
         friend class scc;
+        friend class big;
         friend class elim_eqs;
         friend class asymm_branch;
         friend class probing;
diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp
index af4fd598e..369e95034 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -40,6 +40,38 @@ namespace sat {
         return false;                                           
     }
 
+    watched* find_binary_watch(watch_list & wlist, literal l) {
+        for (watched& w : wlist) {
+            if (w.is_binary_clause() && w.get_literal() == l) return &w;
+        }
+        return nullptr;
+    }
+
+    watched const* find_binary_watch(watch_list const& wlist, literal l) {
+        for (watched const& w : wlist) {
+            if (w.is_binary_clause() && w.get_literal() == l) return &w;
+        }
+        return nullptr;
+    }
+
+    void erase_binary_watch(watch_list& wlist, literal l) {
+        watch_list::iterator it = wlist.begin(), end = wlist.end();
+        watch_list::iterator it2 = it;
+        bool found = false;
+        for (; it != end; ++it) {
+            if (it->is_binary_clause() && it->get_literal() == l && !found) {
+                found = true;
+            }
+            else {
+                *it2 = *it;
+                ++it2;
+            }
+        }
+        wlist.set_end(it2);
+        VERIFY(found);
+    }
+
+
     std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist) {
         bool first = true;
         for (watched const& w : wlist) {
diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h
index e2d814f5b..305948251 100644
--- a/src/sat/sat_watched.h
+++ b/src/sat/sat_watched.h
@@ -50,7 +50,7 @@ namespace sat {
             SASSERT(is_binary_clause());
             SASSERT(get_literal() == l);
             SASSERT(is_learned() == learned);
-            SASSERT(learned || is_binary_unblocked_clause());
+            SASSERT(learned || is_binary_non_learned_clause());
         }
 
         watched(literal l1, literal l2) {
@@ -88,15 +88,12 @@ namespace sat {
         void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); }
         bool is_learned() const { SASSERT(is_binary_clause()); return (m_val2 >> 2) == 1; }
 
-        bool is_binary_unblocked_clause() const { return m_val2 == 0; }
         bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
         bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); }
 
-        void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
-        void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); }
-        bool is_blocked() const { SASSERT(is_binary_clause()); return 0 != (m_val2 & (1 << 3)); }
-        void set_unblocked() { SASSERT(is_binary_clause()); SASSERT(is_blocked()); m_val2 &= ~(1u << 3u); }
-        
+        void set_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
+        void set_learned() { SASSERT(!is_learned()); m_val2 = static_cast<unsigned>(BINARY) + (1u << 2); SASSERT(is_learned()); }
+                
         bool is_ternary_clause() const { return get_kind() == TERNARY; }
         literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
         literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); }
@@ -135,6 +132,8 @@ namespace sat {
 
     typedef vector<watched> watch_list;
 
+    watched* find_binary_watch(watch_list & wlist, literal l);
+    watched const* find_binary_watch(watch_list const & wlist, literal l);
     bool erase_clause_watch(watch_list & wlist, clause_offset c);
     inline void erase_ternary_watch(watch_list & wlist, literal l1, literal l2) { wlist.erase(watched(l1, l2)); }
 
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 90a6cb7c8..29f6a32f1 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -180,12 +180,6 @@ public:
         m_solver2->assert_expr(t, a);
     }
 
-    virtual void assert_lemma(expr* t) {
-        m_solver1->assert_lemma(t);
-        if (m_solver2_initialized)
-            m_solver2->assert_lemma(t);
-    }
-
     virtual void push() {
         switch_inc_mode();
         m_solver1->push();
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 2b1824cd3..7a51725a2 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -104,12 +104,6 @@ public:
 
     virtual void assert_expr_core(expr * t, expr * a) = 0;
 
-    /**
-       \brief Add a lemma to the assertion stack. A lemma is assumed to be a consequence of already
-       asserted formulas. The solver is free to ignore lemmas.
-    */
-    virtual void assert_lemma(expr * t) {}
-
     /**
        \brief Create a backtracking point.
     */