diff --git a/src/ast/ast.h b/src/ast/ast.h
index e579e4565..682660638 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -622,6 +622,9 @@ public:
     sort * const * get_domain() const { return m_domain; }
     sort * get_range() const { return m_range; }
     unsigned get_size() const { return get_obj_size(m_arity); }
+    sort * const * begin() const { return get_domain(); }
+    sort * const * end() const { return get_domain() + get_arity(); }
+
 };
 
 // -----------------------------------
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index 0df4b0fc5..5d47170ee 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -20,20 +20,15 @@ Revision History:
 #include "ast/decl_collector.h"
 
 void decl_collector::visit_sort(sort * n) {
+    SASSERT(!m_visited.is_marked(n));
     family_id fid = n->get_family_id();
     if (m().is_uninterp(n))
         m_sorts.push_back(n);
-    if (fid == m_dt_fid) {
+    else if (fid == m_dt_fid) {
         m_sorts.push_back(n);
-
-        unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
-        for (unsigned i = 0; i < num_cnstr; i++) {
-            func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
+        for (func_decl* cnstr : *m_dt_util.get_datatype_constructors(n)) {
             m_decls.push_back(cnstr);
-            ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
-            unsigned num_cas = cnstr_acc.size();
-            for (unsigned j = 0; j < num_cas; j++) {
-                func_decl * accsr = cnstr_acc.get(j);
+            for (func_decl * accsr : *m_dt_util.get_constructor_accessors(cnstr)) {
                 m_decls.push_back(accsr);
             }
         }
@@ -53,6 +48,7 @@ void decl_collector::visit_func(func_decl * n) {
             else
                 m_decls.push_back(n);
         }
+        m_visited.mark(n, true);
     }
 }
 
@@ -72,11 +68,10 @@ void decl_collector::visit(ast* n) {
         if (!m_visited.is_marked(n)) {
             switch(n->get_kind()) {
             case AST_APP: {
-                app * a = to_app(n);
-                for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                    m_todo.push_back(a->get_arg(i));
+                for (expr * e : *to_app(n)) {
+                    m_todo.push_back(e);
                 }
-                m_todo.push_back(a->get_decl());
+                m_todo.push_back(to_app(n)->get_decl());
                 break;
             }
             case AST_QUANTIFIER: {
@@ -96,8 +91,8 @@ void decl_collector::visit(ast* n) {
                 break;
             case AST_FUNC_DECL: {
                 func_decl * d = to_func_decl(n);
-                for (unsigned i = 0; i < d->get_arity(); ++i) {
-                    m_todo.push_back(d->get_domain(i));
+                for (sort* srt : *d) {
+                    m_todo.push_back(srt);
                 }
                 m_todo.push_back(d->get_range());
                 visit_func(d);
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index 0a812bb2c..36d7c930b 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -41,7 +41,7 @@ class decl_collector {
 
 public:
     // if preds == true, then predicates are stored in a separate collection.
-    decl_collector(ast_manager & m, bool preds=true);
+    decl_collector(ast_manager & m, bool preds = true);
     ast_manager & m() { return m_manager; }
 
     void visit_func(func_decl* n);
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 eb7be411a..e3543ff0f 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"
 
@@ -65,14 +65,14 @@ namespace sat {
         }
     };
 
-    bool asymm_branch::process(scc* scc) {
+    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 (scc) scc->init_big(true);
-            process(scc, s.m_clauses);
-            process(scc, s.m_learned);
+            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;
@@ -86,7 +86,7 @@ namespace sat {
     }
 
 
-    void asymm_branch::process(scc* scc, clause_vector& clauses) {
+    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();
@@ -110,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;
@@ -153,8 +153,8 @@ namespace sat {
             ++counter;
             change = false;
             if (m_asymm_branch_sampled) {
-                scc sc(s, m_params);
-                if (process(&sc)) change = true;
+                big big;
+                if (process(&big)) change = true;
             }
             if (m_asymm_branch) {
                 m_counter  = 0; 
@@ -188,40 +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) {
-        sort(scc, c.begin(), c.end());
+    void asymm_branch::sort(big& big, clause const& c) {
+        sort(big, c.begin(), c.end());
     }
 
-    void asymm_branch::sort(scc& scc, literal const* begin, literal const* end) {
+    void asymm_branch::sort(big& big, literal const* begin, literal const* end) {
         m_pos.reset(); m_neg.reset();
         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++];
             }
@@ -232,10 +232,10 @@ namespace sat {
         return false;
     }
 
-    void asymm_branch::minimize(scc& scc, literal_vector& lemma) {
-        scc.ensure_big(true);
-        sort(scc, lemma.begin(), lemma.end());
-        uhle(scc);
+    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) {
@@ -249,14 +249,13 @@ namespace sat {
         }
     }
 
-    void asymm_branch::uhle(scc& scc) {
+    void asymm_branch::uhle(big& big) {
         m_to_delete.reset();
         if (m_to_delete.empty()) {
-            int right = scc.get_right(m_pos.back());
+            int right = big.get_right(m_pos.back());
             for (unsigned i = m_pos.size() - 1; i-- > 0; ) {
                 literal lit = m_pos[i];
-                SASSERT(scc.get_left(lit) < scc.get_left(last));
-                int right2 = scc.get_right(lit);
+                int right2 = big.get_right(lit);
                 if (right2 > right) {
                     // lit => last, so lit can be deleted
                     m_to_delete.push_back(lit);
@@ -267,10 +266,10 @@ namespace sat {
             }
         }
         if (m_to_delete.empty()) {
-            int 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);
@@ -282,8 +281,8 @@ namespace sat {
         }
     }
 
-    bool asymm_branch::uhle(scoped_detach& scoped_d, scc& scc, clause & c) {
-        uhle(scc);
+    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) {
@@ -384,17 +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) {
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index 14c37427e..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"
 
@@ -51,29 +51,29 @@ namespace sat {
         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, literal const* begin, literal const* end);
-        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);
 
-        void uhle(scc & scc);
+        void uhle(big & big);
 
-        bool uhte(scc & scc, clause & c);
+        bool uhte(big & big, clause & c);
 
         bool re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz);
 
-        bool process(scc* scc);
+        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);
         
@@ -94,7 +94,7 @@ namespace sat {
         void collect_statistics(statistics & st) const;
         void reset_statistics();
 
-        void minimize(scc& scc, literal_vector& lemma);
+        void minimize(big& big, literal_vector& lemma);
 
         void init_search() { m_calls = 0; }
 
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_config.cpp b/src/sat/sat_config.cpp
index 940dc4e43..361e15d91 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -87,8 +87,30 @@ namespace sat {
         else  
             throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
 
+        if (p.lookahead_cube_cutoff() == symbol("depth")) {
+            m_lookahead_cube_cutoff = depth_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("freevars")) {
+            m_lookahead_cube_cutoff = freevars_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("psat")) {
+            m_lookahead_cube_cutoff = psat_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) {
+            m_lookahead_cube_cutoff = adaptive_freevars_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) {
+            m_lookahead_cube_cutoff = adaptive_psat_cutoff;
+        }
+        else {
+            throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'");
+        }
         m_lookahead_cube_fraction = p.lookahead_cube_fraction();
-        m_lookahead_cube_cutoff = p.lookahead_cube_cutoff();
+        m_lookahead_cube_depth = p.lookahead_cube_depth();
+        m_lookahead_cube_freevars = p.lookahead_cube_freevars();
+        m_lookahead_cube_psat_var_exp = p.lookahead_cube_psat_var_exp();
+        m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base();
+        m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger();
         m_lookahead_global_autarky = p.lookahead_global_autarky();
 
         // These parameters are not exposed
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index b2ccb8a1f..da225c26b 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -65,6 +65,14 @@ namespace sat {
         march_cu_reward
     };
 
+    enum cutoff_t {
+        depth_cutoff,
+        freevars_cutoff,
+        psat_cutoff,
+        adaptive_freevars_cutoff,
+        adaptive_psat_cutoff
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -84,8 +92,13 @@ namespace sat {
         bool               m_local_search;
         bool               m_lookahead_simplify;
         bool               m_lookahead_simplify_bca;
-        unsigned           m_lookahead_cube_cutoff;
+        cutoff_t           m_lookahead_cube_cutoff;
         double             m_lookahead_cube_fraction;
+        unsigned           m_lookahead_cube_depth;
+        double             m_lookahead_cube_freevars;
+        double             m_lookahead_cube_psat_var_exp;
+        double             m_lookahead_cube_psat_clause_base;
+        double             m_lookahead_cube_psat_trigger;
         reward_t           m_lookahead_reward;
         bool               m_lookahead_global_autarky;
 
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 7e803eaa5..51bffc72d 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -85,8 +85,8 @@ 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);
+        simp.collect_clauses(pos_l, simp.m_pos_cls);
+        simp.collect_clauses(neg_l, simp.m_neg_cls);
         VERIFY(!s.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);
@@ -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 ef9c0aedf..fd4f63c1e 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -683,7 +683,7 @@ namespace sat {
             // NB. u.index() > l.index() iff u.index() > (~l).index().
             // since indices for the same boolean variables occupy
             // two adjacent numbers.
-            if (u.index() > l.index() && is_stamped(u)) {                
+            if (u.index() > l.index() && is_stamped(u) && ~l != u) {                
                 add_arc(~l, ~u);
                 add_arc( u,  l);
             }
@@ -692,7 +692,8 @@ namespace sat {
             lits.reset();
             if (w.is_ext_constraint() && m_s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), lits)) { 
                 for (literal u : lits) {
-                    if (u.index() > l.index() && is_stamped(u)) {
+                    // u is positive in lits, l is negative:                    
+                    if (~l != u && u.index() > l.index() && is_stamped(u)) {
                         add_arc(~l, ~u);
                         add_arc( u,  l);
                     }
@@ -1033,6 +1034,7 @@ namespace sat {
         }
         propagate();
         m_qhead = m_trail.size();
+        m_init_freevars = m_freevars.size();
         TRACE("sat", m_s.display(tout); display(tout););
     }
 
@@ -2018,6 +2020,35 @@ namespace sat {
         st.update("lh cube conflicts", m_cube_state.m_conflicts);        
     }
 
+    double lookahead::psat_heur() {
+        double h = 0.0;
+        for (bool_var x : m_freevars) {
+            literal l(x, false);
+            for (literal lit : m_binary[l.index()]) {
+                h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0;
+            }
+            for (literal lit : m_binary[(~l).index()]) {
+                h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0;
+            }
+            for (binary b : m_ternary[l.index()]) {
+                h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ?
+                     1.0 / pow(m_config.m_cube_psat_clause_base, 2) :
+                     0.0;
+            }
+            for (binary b : m_ternary[(~l).index()]) {
+                h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ?
+                     1.0 / pow(m_config.m_cube_psat_clause_base, 2) :
+                     0.0;
+            }
+        }
+        for (nary * n : m_nary_clauses) {
+            h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1);
+        }
+        h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp);
+        IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";);
+        return h;
+    }
+
     lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
         scoped_ext _scoped_ext(*this);
         lits.reset();
@@ -2062,9 +2093,14 @@ namespace sat {
             }
             backtrack_level = UINT_MAX;
             depth = m_cube_state.m_cube.size();
-            if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
-                (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
-                m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
+            if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) ||
+                (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) ||
+                (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) ||
+                (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) ||
+                (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) {
+                double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
+                m_cube_state.m_freevars_threshold *= dec;
+                m_cube_state.m_psat_threshold *= dec;
                 set_conflict();
                 m_cube_state.inc_cutoff();
 #if 0
@@ -2077,10 +2113,12 @@ namespace sat {
                 return l_undef;
             }
             int prev_nfreevars = m_freevars.size();
+            double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX;  // MN. only compute PSAT if enabled
             literal lit = choose();
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
                 m_cube_state.m_freevars_threshold = prev_nfreevars;
+                m_cube_state.m_psat_threshold = prev_psat;
                 m_cube_state.inc_conflict();
                 if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
                 continue;
@@ -2332,8 +2370,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);
@@ -2350,14 +2388,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);
@@ -2365,7 +2403,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());
@@ -2457,6 +2495,11 @@ namespace sat {
         m_config.m_reward_type = m_s.m_config.m_lookahead_reward;
         m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff;
         m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction;
+        m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth;
+        m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars;
+        m_config.m_cube_psat_var_exp = m_s.m_config.m_lookahead_cube_psat_var_exp;
+        m_config.m_cube_psat_clause_base = m_s.m_config.m_lookahead_cube_psat_clause_base;
+        m_config.m_cube_psat_trigger = m_s.m_config.m_lookahead_cube_psat_trigger;
     }
 
     void lookahead::collect_statistics(statistics& st) const {
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 2f62c932d..6a7bb7449 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -80,8 +80,13 @@ namespace sat {
             unsigned m_dl_max_iterations;
             unsigned m_tc1_limit;
             reward_t m_reward_type;
-            unsigned m_cube_cutoff;
+            cutoff_t m_cube_cutoff;
+            unsigned m_cube_depth;
             double   m_cube_fraction;
+            double   m_cube_freevars;
+            double   m_cube_psat_var_exp;
+            double   m_cube_psat_clause_base;
+            double   m_cube_psat_trigger;
 
             config() {
                 memset(this, sizeof(*this), 0);
@@ -96,8 +101,13 @@ namespace sat {
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
-                m_cube_cutoff = 0;
+                m_cube_cutoff = adaptive_freevars_cutoff;
+                m_cube_depth = 10;
                 m_cube_fraction = 0.4;
+                m_cube_freevars = 0.8;
+                m_cube_psat_var_exp = 1.0;
+                m_cube_psat_clause_base = 2.0;
+                m_cube_psat_trigger = 5.0;
             }
         };
 
@@ -167,6 +177,7 @@ namespace sat {
             svector<bool>  m_is_decision;
             literal_vector m_cube;
             double         m_freevars_threshold;
+            double         m_psat_threshold;
             unsigned       m_conflicts;
             unsigned       m_cutoffs;
             cube_state() { reset(); }
@@ -175,6 +186,7 @@ namespace sat {
                 m_is_decision.reset(); 
                 m_cube.reset(); 
                 m_freevars_threshold = 0;
+                m_psat_threshold = DBL_MAX;
                 reset_stats();
             }
             void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }
@@ -228,11 +240,12 @@ namespace sat {
         svector<prefix>        m_vprefix;       // var:     prefix where variable participates in propagation
         unsigned               m_rating_throttle; // throttle to recompute rating
         indexed_uint_set       m_freevars;
+        unsigned               m_init_freevars;
         lookahead_mode         m_search_mode;   // mode of search
         stats                  m_stats;
         model                  m_model; 
         cube_state             m_cube_state;
-        scoped_ptr<extension>   m_ext;
+        scoped_ptr<extension>  m_ext;
  
         // ---------------------------------------
         // truth values
@@ -542,6 +555,8 @@ namespace sat {
 
         void add_hyper_binary();
 
+        double psat_heur();
+
     public:
         lookahead(solver& s) : 
             m_s(s),
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index fde5f1272..672e22512 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -38,8 +38,14 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
-                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
-                          ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
+                          ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
+                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'),
+                          ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),
+                          ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'),
+                          ('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..b83f22e35 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,14 @@ 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 87218b735..6d578b4f9 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);
         }
 
 
@@ -1357,7 +1360,7 @@ namespace sat {
         void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
             TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
             VERIFY(!s.is_external(l));
-            if (new_entry == 0 && !s.m_retain_blocked_clauses)
+            if (new_entry == 0)
                 new_entry = &(mc.mk(k, l.var()));
             m_to_remove.push_back(&c);
             for (literal lit : c) {
@@ -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;
@@ -1782,7 +1771,7 @@ namespace sat {
 
         // eliminate variable
         ++s.m_stats.m_elim_var_res;
-        VERIFY(!s.is_external(v));
+        VERIFY(!is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);
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 d4a57a9b1..3fba8d12d 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) {
@@ -1331,6 +1340,7 @@ namespace sat {
     void solver::add_assumption(literal lit) {
         m_assumption_set.insert(lit);
         m_assumptions.push_back(lit);
+        set_external(lit.var());
         VERIFY(is_external(lit.var()));
     }
 
@@ -1419,6 +1429,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 +1442,28 @@ 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());
         }
-
+		si.check_watches();
         if (m_config.m_lookahead_simplify) {
             lookahead lh(*this);
             lh.simplify();
             lh.collect_statistics(m_aux_stats);
         }
-
+		si.check_watches();
         sort_watch_lits();
         CASSERT("sat_simplify_bug", check_invariant());
 
@@ -1575,7 +1589,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)); }