diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 1f236a9c7..db72b847f 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1820,6 +1820,10 @@ namespace sat {
                 }
             }
             
+            ++j;
+            if (j < p.num_watch()) {
+                j = p.num_watch();
+            }
             CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); 
             
             if (_debug_conflict) {
@@ -1845,6 +1849,25 @@ namespace sat {
         SASSERT(validate_unit_propagation(p, r, l));
     }
 
+    bool ba_solver::is_extended_binary(ext_justification_idx idx, literal_vector & r) {
+        constraint const& c = index2constraint(idx);
+        switch (c.tag()) {
+        case card_t: {
+            card const& ca = c.to_card();
+            if (ca.size() == ca.k() + 1 && ca.lit() == null_literal) {
+                r.reset();
+                for (literal l : ca) r.push_back(l);
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+        default:
+            return false;
+        }
+    }
+
     void ba_solver::simplify(xor& x) {
         // no-op
     }
@@ -2110,18 +2133,40 @@ namespace sat {
     /**
        \brief Lex on (glue, size)
     */
-    struct constraint_glue_lt {
+    struct constraint_glue_psm_lt {
         bool operator()(ba_solver::constraint const * c1, ba_solver::constraint const * c2) const {
             return 
                 (c1->glue()  < c2->glue()) ||
-                (c1->glue() == c2->glue() && c1->size() < c2->size());
+                (c1->glue() == c2->glue() && 
+                 (c1->psm() < c2->psm() || 
+                  (c1->psm() == c2->psm() && c1->size() < c2->size())));
         }
     };
 
+    void ba_solver::update_psm(constraint& c) const {
+        unsigned r = 0;
+        switch (c.tag()) {            
+        case card_t: 
+            for (literal l : c.to_card()) {                
+                if (s().m_phase[l.var()] == (l.sign() ? NEG_PHASE : POS_PHASE)) ++r;
+            }
+            break;
+        case pb_t:
+            for (wliteral l : c.to_pb()) {                
+                if (s().m_phase[l.second.var()] == (l.second.sign() ? NEG_PHASE : POS_PHASE)) ++r;
+            }
+            break;
+        default:
+            break;
+        }
+        c.set_psm(r);
+    }
+
     void ba_solver::gc() {
         if (m_learned.size() >= 2 * m_constraints.size()) {
-            std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt());
-            gc_half("glue");
+            for (auto & c : m_learned) update_psm(*c);
+            std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt());
+            gc_half("glue-psm");
             cleanup_constraints(m_learned, true);
         }
     }
@@ -3056,7 +3101,7 @@ namespace sat {
         }
         for (wliteral l : p1) {
             SASSERT(m_weights[l.second.index()] == 0);
-            m_weights[l.second.index()] = l.first;
+            m_weights.setx(l.second.index(), l.first, 0);
             mark_visited(l.second);  
         }
         for (unsigned i = 0; i < p1.num_watch(); ++i) {
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 46e6b15e8..586ecd53e 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -64,12 +64,13 @@ namespace sat {
             bool           m_removed;
             literal        m_lit;
             unsigned       m_glue;
+            unsigned       m_psm;
             unsigned       m_size;
             size_t         m_obj_size;
             bool           m_learned;
             unsigned       m_id;
         public:
-            constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
+            constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
             ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
             unsigned id() const { return m_id; }
             tag_t tag() const { return m_tag; }
@@ -81,7 +82,9 @@ namespace sat {
             void remove() { m_removed = true; }
             void nullify_literal() { m_lit = null_literal; }
             unsigned glue() const { return m_glue; }
-            void set_glue(unsigned g) { m_glue = g; }            
+            void set_glue(unsigned g) { m_glue = g; }          
+            unsigned psm() const { return m_psm; }
+            void set_psm(unsigned p) { m_psm = p; }
             void set_learned(bool f) { m_learned = f; }
             bool learned() const { return m_learned; }            
 
@@ -269,6 +272,7 @@ namespace sat {
         void subsumption(constraint& c1);
         void subsumption(card& c1);
         void gc_half(char const* _method);
+        void update_psm(constraint& c) const;
         void mutex_reduction();
 
         typedef vector<std::pair<rational, lp::var_index>> lhs_t;
@@ -446,6 +450,7 @@ namespace sat {
         virtual void pop_reinit();
         virtual void gc(); 
         virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const;
+        virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r);
         virtual void init_use_list(ext_use_list& ul);
         virtual bool is_blocked(literal l, ext_constraint_idx idx);
 
diff --git a/src/sat/sat_ccc.cpp b/src/sat/sat_ccc.cpp
index 025bbafd4..ee087a60f 100644
--- a/src/sat/sat_ccc.cpp
+++ b/src/sat/sat_ccc.cpp
@@ -36,39 +36,48 @@ using namespace sat;
 // ------------
 // cuber
 
-ccc::cuber::cuber(ccc& c): m_ccc(c), lh(c.m_s), m_branch_id(0) {}
+ccc::cuber::cuber(ccc& c): m_ccc(c), m_lh(alloc(lookahead, c.m_s)), m_branch_id(0) {}
 
 lbool ccc::cuber::search() {
-    m_branch_id = 0;
-    m_last_closure_level = 1000;
-
-    lh.init_search();
-    lh.m_model.reset();
-
-    lookahead::scoped_level _sl(lh, lh.c_fixed_truth);
-    lh.m_search_mode = lookahead_mode::searching;
-    lbool r = research();
-    if (r == l_true) {
-        m_ccc.m_model = lh.get_model();
+    while (true) {
+        m_branch_id = 0;
+        m_last_closure_level = 1000;
+        
+        m_lh->init_search();
+        m_lh->m_model.reset();
+        
+        lookahead::scoped_level _sl(*m_lh.get(), m_lh->c_fixed_truth);
+        m_lh->m_search_mode = lookahead_mode::searching;
+        lbool r = research();
+        if (r == l_true) {
+            m_ccc.m_model = m_lh->get_model();
+        }
+        if (false && r == l_undef) {
+            continue;
+        }
+        m_lh->collect_statistics(m_ccc.m_lh_stats);
+        return r;
     }
-    lh.collect_statistics(m_ccc.m_lh_stats);
-    return r;
 }
 
 lbool ccc::cuber::research() {
     m_ccc.m_s.checkpoint();
     
-    if (lh.inconsistent()) {
+    if (m_lh->inconsistent()) {
         return l_false;
     }
 
+    if (pop_lookahead()) {
+        return l_undef;
+    }
+
     if (get_solved()) {
         return l_false;
     }
 
-    lh.inc_istamp(); 
-    literal l = lh.choose();
-    if (lh.inconsistent()) {
+    m_lh->inc_istamp(); 
+    literal l = m_lh->choose();
+    if (m_lh->inconsistent()) {
         return l_false;
     }
 
@@ -76,34 +85,35 @@ lbool ccc::cuber::research() {
         return l_true;
     }
 
-    if (!decisions.empty()) {
-        m_ccc.put_decision(decisions.back());
+    if (!m_decisions.empty()) {
+        m_ccc.put_decision(m_decisions.back());
     }
 
-    // update trail and decisions
+
+    // update trail and m_decisions
     
-    ++lh.m_stats.m_decisions;
-    unsigned parent_id = decisions.empty() ? 0 : decisions.back().m_id;
+    ++m_lh->m_stats.m_decisions;
+    unsigned parent_id = m_decisions.empty() ? 0 : m_decisions.back().m_id;
     unsigned spawn_id = spawn_conquer();
     unsigned branch1 = m_branch_id++;
     unsigned branch2 = m_branch_id++;
-    decision d(branch1, decisions.size() + 1, l, parent_id, spawn_id);
-    decisions.push_back(d);
+    decision d(branch1, m_decisions.size() + 1, l, parent_id, spawn_id);
+    m_decisions.push_back(d);
     
-    IF_VERBOSE(1, d.pp(verbose_stream() << "select " << m_last_closure_level << " ") << "\n";);
-    IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";);
-    IF_VERBOSE(2, pp(verbose_stream(), decisions) << "\n"; );
+    IF_VERBOSE(2, d.pp(verbose_stream() << "select " << m_last_closure_level << " ") << "\n";);
+    IF_VERBOSE(2, verbose_stream() << "select " << pp_prefix(m_lh->m_prefix, m_lh->m_trail_lim.size()) << ": " << l << " " << m_lh->m_trail.size() << "\n";);
+    IF_VERBOSE(3, pp(verbose_stream(), m_decisions) << "\n"; );
     
     TRACE("sat", tout << "choose: " << l << "\n";);
-    lh.push(l, lh.c_fixed_truth);
+    m_lh->push(l, m_lh->c_fixed_truth);
     lbool r = research();
     if (r == l_false) {
-        lh.pop();
-        if (decisions.back().is_closed()) {
+        m_lh->pop();
+        if (m_decisions.back().is_closed()) {
             // branch was solved by a spawned conquer process
-            IF_VERBOSE(1, decisions.back().pp(verbose_stream() << "closed ") << "\n";);            
+            IF_VERBOSE(1, m_decisions.back().pp(verbose_stream() << "closed ") << "\n";);            
             r = l_false;
-            decisions.pop_back();
+            m_decisions.pop_back();
         }
         else {
             if (spawn_id > 0) {
@@ -111,22 +121,41 @@ lbool ccc::cuber::research() {
                 m_last_closure_level *= 3;
                 m_last_closure_level /= 4;
             }
-            lh.inc_istamp(); 
-            lh.flip_prefix();
-            lh.push(~l, lh.c_fixed_truth);
-            decisions.back().negate();
-            decisions.back().m_id = branch2;
-            decisions.back().m_spawn_id = 0;
+            m_lh->inc_istamp(); 
+            m_lh->flip_prefix();
+            m_lh->push(~l, m_lh->c_fixed_truth);
+            m_decisions.back().negate();
+            m_decisions.back().m_id = branch2;
+            m_decisions.back().m_spawn_id = 0;
             r = research();
             if (r == l_false) {
-                lh.pop();
-                decisions.pop_back();
+                m_lh->pop();
+                m_decisions.pop_back();
             }
         }
     }
     return r;
 }
 
+bool ccc::cuber::pop_lookahead() {
+    return false;
+
+    scoped_ptr<lookahead> new_lh;
+    bool result = false;
+    #pragma omp critical (ccc_new_lh)
+    {
+       if (m_ccc.m_new_lh) {
+           new_lh = m_ccc.m_new_lh.detach();
+           result = true;
+       }
+    }
+    if (new_lh) {
+        m_lh->collect_statistics(m_ccc.m_lh_stats);
+        m_lh = new_lh.detach();        
+    }
+    return result;
+}
+
 void ccc::cuber::update_closure_level(decision const& d, int offset) {
     m_last_closure_level = (d.m_depth + 3*m_last_closure_level) / 4;
     if (m_last_closure_level >= static_cast<unsigned>(abs(offset))) {
@@ -140,13 +169,13 @@ unsigned ccc::cuber::spawn_conquer() {
     // decisions must have been solved at a higher level by a conquer thread
     // 
     if (!m_free_threads.empty()) {
-        if (m_last_closure_level <= decisions.size()) {
+        if (m_last_closure_level <= m_decisions.size()) {
             result = m_free_threads.back();
             ++m_ccc.m_ccc_stats.m_spawn_opened;
             m_free_threads.pop_back();
         }
         else {
-            IF_VERBOSE(1, verbose_stream() << m_last_closure_level << " " << decisions.size() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << m_last_closure_level << " " << m_decisions.size() << "\n";);
         }
     }
     return result;
@@ -181,13 +210,13 @@ bool ccc::cuber::get_solved() {
         unsigned branch_id = sol.m_branch_id;
         unsigned thread_id = sol.m_thread_id;
         bool found = false;
-        for (unsigned i = decisions.size(); i > 0; ) {
+        for (unsigned i = m_decisions.size(); i > 0; ) {
             --i;
-            decision& d = decisions[i];
+            decision& d = m_decisions[i];
             if (branch_id == d.m_id) {
                 if (d.m_spawn_id == thread_id && thread_id != 0) {
                     SASSERT(d.m_spawn_id > 0);
-                    IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": spawn close ") << "\n";);
+                    IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": spawn close ") << "\n";);
                     ++m_ccc.m_ccc_stats.m_spawn_closed;
                     d.close();
                     free_conquer(thread_id);
@@ -195,7 +224,7 @@ bool ccc::cuber::get_solved() {
                     break;
                 }
                 else {
-                    IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": conquer ") << "\n";);
+                    IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": conquer ") << "\n";);
                     ++m_ccc.m_ccc_stats.m_cdcl_closed;
                     update_closure_level(d, 1);
                     return true;
@@ -236,6 +265,7 @@ lbool ccc::conquer::search() {
             s.simplify_problem();
             if (s.check_inconsistent()) return l_false;
             s.gc();     
+            push_lookahead();
         }
     }
     catch (solver::abort_solver) {
@@ -245,16 +275,16 @@ lbool ccc::conquer::search() {
 
 void ccc::conquer::replay_decisions() {
     s.propagate(true);
-    for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < decisions.size(); ++i) {
-        decision const& d = decisions[i];
+    for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < m_decisions.size(); ++i) {
+        decision const& d = m_decisions[i];
         IF_VERBOSE(2, verbose_stream() << thread_id << ": replay " << d.get_literal(thread_id) << " " << s.value(d.get_literal(thread_id)) << "\n";);
         
         if (!push_decision(d)) {
             // negation of decision is implied.
             IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": backjump to level " << i << " ") << "\n";);
-            while (decisions.size() > i) {
-                pop_decision(decisions.back());
-                decisions.pop_back();
+            while (m_decisions.size() > i) {
+                pop_decision(m_decisions.back());
+                m_decisions.pop_back();
             }
             break;
         }
@@ -280,6 +310,19 @@ void ccc::conquer::pop_decision(decision const& d) {
     }
 }
 
+void ccc::conquer::push_lookahead() {
+    return;
+
+    #pragma omp critical (ccc_new_lh)
+    {
+        if (!m_ccc.m_new_lh && m_ccc.m_num_clauses > s.num_clauses()) {
+            std::cout << "push " << s.num_clauses() << "\n";
+            m_ccc.m_new_lh = alloc(lookahead, s);
+            m_ccc.m_num_clauses = s.num_clauses();
+        }
+    }
+}
+
 bool ccc::conquer::push_decision(decision const& d) {
     literal lit = d.get_literal(thread_id);
     switch (s.value(lit)) {
@@ -313,7 +356,7 @@ bool ccc::conquer::cube_decision() {
 
         if (d.is_spawned(thread_id)) IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << " ") << "\n";);
     
-        if (!decisions.empty() && decisions.back().m_depth + 1 < d.m_depth) {
+        if (!m_decisions.empty() && m_decisions.back().m_depth + 1 < d.m_depth) {
             if (d.is_spawned(thread_id)) {
                 pop_decision(d);
             }           
@@ -322,43 +365,43 @@ bool ccc::conquer::cube_decision() {
             break;
         }
     }    
-    SASSERT(decisions.empty() || decisions.back().m_depth + 1 >= d.m_depth);
+    SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
 
-    if (!decisions.empty() && decisions.back().is_spawned(thread_id) && decisions.back().m_depth == d.m_depth) {
+    if (!m_decisions.empty() && m_decisions.back().is_spawned(thread_id) && m_decisions.back().m_depth == d.m_depth) {
         SASSERT(d.m_spawn_id == 0);
-        SASSERT(decisions.back().is_left());
+        SASSERT(m_decisions.back().is_left());
         SASSERT(!d.is_left());
         IF_VERBOSE(1, verbose_stream() << thread_id << " inherit spawn\n";);
-        decisions.back().m_spawn_id = 0;
+        m_decisions.back().m_spawn_id = 0;
         m_spawned = false;
     }
-    SASSERT(decisions.empty() || decisions.back().m_depth + 1 >= d.m_depth);
+    SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
 
-    while (!decisions.empty() && decisions.back().m_depth >= d.m_depth) {
-        // check_non_model("cube decision", decisions);
-        if (decisions.back().is_spawned(thread_id)) {
-            pop_decision(decisions.back());
+    while (!m_decisions.empty() && m_decisions.back().m_depth >= d.m_depth) {
+        // check_non_model("cube decision", m_decisions);
+        if (m_decisions.back().is_spawned(thread_id)) {
+            pop_decision(m_decisions.back());
         }
-        decisions.pop_back();
+        m_decisions.pop_back();
     }
 
-    SASSERT(decisions.empty() || decisions.back().m_depth + 1 == d.m_depth);
-    SASSERT(decisions.empty() || decisions.back().m_id == d.m_parent);
+    SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 == d.m_depth);
+    SASSERT(m_decisions.empty() || m_decisions.back().m_id == d.m_parent);
     if (m_spawned) {
-        decisions.push_back(d);
+        m_decisions.push_back(d);
         return true;
     }
 
-    s.pop_reinit(s.scope_lvl() - decisions.size());
+    s.pop_reinit(s.scope_lvl() - m_decisions.size());
     SASSERT(s.m_qhead == s.m_trail.size());
-    SASSERT(s.scope_lvl() == decisions.size());
+    SASSERT(s.scope_lvl() == m_decisions.size());
     literal lit = d.get_literal(thread_id);
-    IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": cube ") << "\n";);
-    IF_VERBOSE(2, pp(verbose_stream() << thread_id << ": push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
+    IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": cube ") << "\n";);
+    IF_VERBOSE(3, pp(verbose_stream() << thread_id << ": push ", m_decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
                if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";);
     
     if (push_decision(d)) {
-        decisions.push_back(d);
+        m_decisions.push_back(d);
     }    
     else {
         pop_decision(d);
diff --git a/src/sat/sat_ccc.h b/src/sat/sat_ccc.h
index 30c8a3229..348f99b9e 100644
--- a/src/sat/sat_ccc.h
+++ b/src/sat/sat_ccc.h
@@ -74,7 +74,7 @@ namespace sat {
            reslimit          m_limit;
            ccc&              m_ccc;
            solver            s;
-           svector<decision> decisions;
+           svector<decision> m_decisions;
            unsigned          thread_id;
            bool              m_spawned;
            conquer(ccc& super, params_ref const& p, unsigned tid): m_ccc(super), s(p, m_limit), thread_id(tid), m_spawned(false) {}
@@ -84,16 +84,17 @@ namespace sat {
            lbool bounded_search();
            bool  push_decision(decision const& d);
            void  pop_decision(decision const& d);
+           void  push_lookahead();
            void  replay_decisions();
        };
 
         struct cuber {
-            ccc&              m_ccc;
-            lookahead         lh;
-            unsigned          m_branch_id;
-            unsigned          m_last_closure_level;
-            unsigned_vector   m_free_threads;
-            svector<decision> decisions;
+            ccc&                  m_ccc;
+            scoped_ptr<lookahead> m_lh;
+            unsigned              m_branch_id;
+            unsigned              m_last_closure_level;
+            unsigned_vector       m_free_threads;
+            svector<decision>     m_decisions;
 
             cuber(ccc& c);
             lbool search();
@@ -102,11 +103,14 @@ namespace sat {
             void update_closure_level(decision const& d, int offset);            
             unsigned spawn_conquer();
             void     free_conquer(unsigned thread_id);
+            bool pop_lookahead();
         };
 
         solver&         m_s;    
         queue<solution> m_solved;
         vector<queue<decision> > m_decisions;
+        scoped_ptr<lookahead>    m_new_lh;
+        unsigned        m_num_clauses;
         unsigned        m_num_conquer;
         model           m_model;
         volatile bool   m_cancel;
@@ -127,7 +131,7 @@ namespace sat {
 
     public:
 
-        ccc(solver& s): m_s(s) {}
+        ccc(solver& s): m_s(s), m_num_clauses(s.num_clauses()) {}
 
         lbool search();
 
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 0278bdb61..d262d96e0 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -55,6 +55,7 @@ namespace sat {
         virtual bool propagate(literal l, ext_constraint_idx idx) = 0;
         virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const = 0;
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
+        virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) = 0;
         virtual void asserted(literal l) = 0;
         virtual check_result check() = 0;
         virtual lbool resolve_conflict() { return l_undef; } // stores result in sat::solver::m_lemma
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index b5229dc54..bfe5ec686 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -503,6 +503,7 @@ namespace sat {
     // arcs are added in the opposite direction of implications.
     // So for implications l => u we add arcs u -> l
     void lookahead::init_arcs(literal l) {
+        literal_vector lits;
         literal_vector const& succ = m_binary[l.index()];
         for (unsigned i = 0; i < succ.size(); ++i) {
             literal u = succ[i];
@@ -512,6 +513,16 @@ namespace sat {
                 add_arc( u,  l);
             }
         }
+        for (auto w : m_watches[l.index()]) {
+            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)) {
+                        add_arc(~l, ~u);
+                        add_arc( u,  l);
+                    }
+                }
+            }
+        }
     }
 
     void lookahead::get_scc(literal v) {
@@ -852,7 +863,7 @@ namespace sat {
         copy_clauses(m_s.m_clauses);
         copy_clauses(m_s.m_learned);
 
-        m_config.m_use_ternary_reward &= !m_s.m_ext;
+        // m_config.m_use_ternary_reward &= !m_s.m_ext;
 
         // copy units
         unsigned trail_sz = m_s.init_trail_size();
@@ -887,7 +898,7 @@ namespace sat {
             if (c.was_removed()) continue;
             // enable when there is a non-ternary reward system.
             if (c.size() > 3) {
-                m_config.m_use_ternary_reward = false;
+                // m_config.m_use_ternary_reward = false;
             }            
             bool was_eliminated = false;
             for (unsigned i = 0; !was_eliminated && i < c.size(); ++i) {
@@ -1245,7 +1256,12 @@ namespace sat {
     double lookahead::literal_occs(literal l) {
         double result = m_binary[l.index()].size();
         for (clause const* c : m_full_watches[l.index()]) {
-            if (!is_true((*c)[0]) && !is_true((*c)[1])) {
+            bool has_true = false;
+            for (literal l : *c) {
+                has_true = is_true(l);
+                if (has_true) break;
+            }
+            if (!has_true) {
                 result += 1.0 / c->size();
             }
         }
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index ec77ebfbd..15108c7fd 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -33,10 +33,11 @@ namespace sat {
 
     struct frame {
         unsigned  m_lidx;
+        unsigned  m_succ_idx;
         bool      m_first;
         watched * m_it;
         watched * m_end;
-        frame(unsigned lidx, watched * it, watched * end):m_lidx(lidx), m_first(true), m_it(it), m_end(end) {}
+        frame(unsigned lidx, watched * it, watched * end, unsigned sidx = 0):m_lidx(lidx), m_succ_idx(sidx), m_first(true), m_it(it), m_end(end) {}
     };
     typedef svector<frame> frames;
 
@@ -75,7 +76,7 @@ namespace sat {
         index.resize(num_lits, UINT_MAX);
         lowlink.resize(num_lits, UINT_MAX);
         in_s.resize(num_lits, false);
-        literal_vector roots;
+        literal_vector roots, lits;
         roots.resize(m_solver.num_vars(), null_literal);
         unsigned next_index = 0;
         svector<frame>   frames;
@@ -106,6 +107,7 @@ namespace sat {
                 frame & fr = frames.back();
                 unsigned l_idx = fr.m_lidx;
                 if (!fr.m_first) {
+                    SASSERT(fr.m_it->is_binary_clause());
                     // after visiting child
                     literal l2 = fr.m_it->get_literal();
                     unsigned l2_idx = l2.index();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f98175823..183a306aa 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -913,6 +913,13 @@ namespace sat {
                 if (check_inconsistent()) return l_false;
                 gc();
 
+#if 0
+                if (m_clauses.size() < 65000) {
+                    return do_ccc();
+                    return lookahead_search();                
+                }
+#endif
+
                 if (m_config.m_restart_max <= m_restarts) {
                     m_reason_unknown = "sat.max.restarts";
                     IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);