diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 60efc73a9..1cb17900f 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -447,6 +447,7 @@ public:
     app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
     app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
     app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
+    app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); }
     app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); }
     app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); }
     app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index b677b2197..a04436e63 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2251,11 +2251,49 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
     return false;
 }
 
+br_status bv_rewriter::mk_mul_hoist(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (num_args <= 1)
+        return BR_FAILED;
+    expr* z = nullptr, *u = nullptr;
+    for (unsigned i = 0; i < num_args; ++i) {
+        // ~x = -1 - x
+        if (m_util.is_bv_not(args[i], z)) {
+            unsigned sz = m_util.get_bv_size(z);
+            ptr_vector<expr> new_args(num_args, args);
+            rational p = rational(2).expt(sz) - 1;
+            new_args[i] = m_util.mk_bv_sub(mk_numeral(p, sz), z);
+            result = m_util.mk_bv_mul(num_args, new_args.data());
+            return BR_REWRITE3;
+        }
+        // shl(z, u) * x = shl(x * z, u)
+        if (m_util.is_bv_shl(args[i], z, u)) {
+            ptr_vector<expr> new_args(num_args, args);
+            new_args[i] = z;
+            result = m_util.mk_bv_mul(num_args, new_args.data());
+            result = m_util.mk_bv_shl(result, u);
+            return BR_REWRITE2;
+        }
+    }
+    return BR_FAILED;
+}
+
 br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result) {
     br_status st = mk_mul_core(num_args, args, result);
     if (st != BR_FAILED && st != BR_DONE)
         return st;
-    expr* x, * y, * z, * u;
+    if (st == BR_DONE && is_mul(result)) {
+        st = mk_mul_hoist(to_app(result)->get_num_args(), to_app(result)->get_args(), result);
+        if (st != BR_FAILED)
+            return st;
+        st = BR_DONE;
+    }
+    if (st == BR_FAILED) {
+        st = mk_mul_hoist(num_args, args, result);
+        if (st != BR_FAILED)
+            return st;
+    }
+
+    expr* x, * y;
     if (st == BR_FAILED && num_args == 2) {
         x = args[0]; 
         y = args[1];
@@ -2267,27 +2305,6 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
     else {
         return st;
     }
-    // ~x = -1 - x
-    unsigned sz = m_util.get_bv_size(x);
-    if (m_util.is_bv_not(x, z)) {
-        numeral p = rational(2).expt(sz) - 1;
-        result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), y);
-        return BR_REWRITE3;
-    }
-    if (m_util.is_bv_not(y, z)) {
-        numeral p = rational(2).expt(sz) - 1;
-        result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(p, sz), z), x);
-        return BR_REWRITE3;
-    }
-    // shl(z, u) * x = shl(x * z, u)
-    if (m_util.is_bv_shl(x, z, u)) {
-        result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, y), u);
-        return BR_REWRITE2;
-    }
-    if (m_util.is_bv_shl(y, z, u)) {
-        result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, x), u);
-        return BR_REWRITE2;
-    }
     if (m_mul2concat) {
         numeral v;
         unsigned bv_size;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 23ae67277..703e668b6 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -100,6 +100,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_mul(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_mul(2, args, result); }
     br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_mul_hoist(unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);
diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
index 74ddbdbdb..bbdedab86 100644
--- a/src/sat/sat_cleaner.cpp
+++ b/src/sat/sat_cleaner.cpp
@@ -64,7 +64,9 @@ namespace sat {
                     }
                     TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
                     break;
+#if ENABLE_TERNARY
                 case watched::TERNARY:
+#endif
                 case watched::CLAUSE:
                     // skip
                     break;
diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp
index c8d6ebe7a..ab9bc8857 100644
--- a/src/sat/sat_gc.cpp
+++ b/src/sat/sat_gc.cpp
@@ -198,7 +198,7 @@ namespace sat {
         if (c.on_reinit_stack())
             return false;
 #if ENABLE_TERNARY
-        if (ENABLE_TERNARY && c.size() == 3) {
+        if (c.size() == 3) {
             return
                 can_delete3(c[0],c[1],c[2]) &&
                 can_delete3(c[1],c[0],c[2]) &&
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index 3453884a4..a6086d8a7 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -27,10 +27,12 @@ namespace sat {
         s(_s) {
     }
 
+#if ENABLE_TERNARY
     // for ternary clauses 
     static bool contains_watched(watch_list const & wlist, literal l1, literal l2) {
         return wlist.contains(watched(l1, l2));
     }
+#endif
     
     // for nary clauses
     static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
@@ -63,6 +65,7 @@ namespace sat {
         if (c.frozen())
             return true;
 
+#if ENABLE_TERNARY
         if (c.size() == 3) {
             CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
                    tout << "watch_list:\n";
@@ -71,8 +74,10 @@ namespace sat {
             VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
             VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
             VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
+            return true;
         }
-        else {
+#endif
+        {
             if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
                 bool on_prop_stack = false;
                 for (unsigned i = s.m_qhead; i < s.m_trail.size(); i++) {
@@ -169,11 +174,13 @@ namespace sat {
                        tout << "\n";);
                 VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
                 break;
+#if ENABLE_TERNARY
             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;
+#endif
             case watched::CLAUSE:
                 VERIFY(!s.get_clause(w.get_clause_offset()).was_removed());
                 break;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b456db243..b0faaf6c9 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -269,7 +269,9 @@ namespace sat {
             watch_list::iterator end2   = wlist.end();
             for (; it2 != end2; ++it2) {
                 switch (it2->get_kind()) {
+#if ENABLE_TERNARY
                 case watched::TERNARY:
+#endif
                 case watched::CLAUSE:
                     // consume
                     break;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index eae0b8f73..56dcdf0df 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -372,15 +372,15 @@ namespace sat {
     }
 
     void solver::del_clause(clause& c) {
-        if (!c.is_learned()) {
+        if (!c.is_learned()) 
             m_stats.m_non_learned_generation++;
-        } 
-        if (c.frozen()) {
+        
+        if (c.frozen()) 
             --m_num_frozen;
-        }
-        if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c)) {
+        
+        if (!c.was_removed() && m_config.m_drat && !m_drat.is_cleaned(c)) 
             m_drat.del(c);
-        }
+        
         dealloc_clause(&c);        
         if (m_searching) 
             m_stats.m_del_clause++;
@@ -448,10 +448,10 @@ namespace sat {
             if (redundant && m_par) 
                 m_par->share_clause(*this, lits[0], lits[1]);
             return nullptr;
+#if ENABLE_TERNARY
         case 3:
-            if (ENABLE_TERNARY) 
                 return mk_ter_clause(lits, st);
-            Z3_fallthrough;
+#endif
         default:
             return mk_nary_clause(num_lits, lits, st);
         }
@@ -545,6 +545,7 @@ namespace sat {
         m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
     }
 
+#if ENABLE_TERNARY
     clause * solver::mk_ter_clause(literal * lits, sat::status st) {
         VERIFY(ENABLE_TERNARY);
         m_stats.m_mk_ter_clause++;
@@ -575,7 +576,6 @@ namespace sat {
         return reinit;
     }
 
-#if ENABLE_TERNARY
     bool solver::propagate_ter_clause(clause& c) {
         bool reinit = false;
         if (value(c[1]) == l_false && value(c[2]) == l_false) {
@@ -664,9 +664,11 @@ namespace sat {
     void solver::attach_clause(clause & c, bool & reinit) {
         SASSERT(c.size() > 2);
         reinit = false;
+#if ENABLE_TERNARY
         if (ENABLE_TERNARY && c.size() == 3)
             reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
         else
+#endif
             reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
     }
 
@@ -914,11 +916,14 @@ namespace sat {
         if (m_config.m_drat) m_drat.del(l1, l2);       
     }
 
-    void solver::detach_clause(clause & c) {
-        if (ENABLE_TERNARY && c.size() == 3)
+    void solver::detach_clause(clause& c) {
+#if ENABLE_TERNARY
+        if (c.size() == 3) {
             detach_ter_clause(c);
-        else
-            detach_nary_clause(c);
+            return;
+        }
+#endif
+        detach_nary_clause(c);
     }
 
     void solver::detach_nary_clause(clause & c) {
@@ -927,11 +932,13 @@ namespace sat {
         erase_clause_watch(get_wlist(~c[1]), cls_off);
     }
 
+#if ENABLE_TERNARY
     void solver::detach_ter_clause(clause & c) {
         erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
         erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
         erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
     }
+#endif
 
     // -----------------------
     //
@@ -1060,6 +1067,22 @@ namespace sat {
         return r;
     }
 
+    void solver::propagate_clause(clause& c, bool update, unsigned assign_level, clause_offset cls_off) {
+        unsigned glue;
+        SASSERT(value(c[0]) == l_undef); 
+            m_stats.m_propagate++;          
+            c.mark_used();                                          
+            assign_core(c[0], justification(assign_level, cls_off)); 
+            if (update && c.is_learned() && c.glue() > 2 && num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue)) 
+                c.set_glue(glue);                                   \
+    }
+
+    void solver::set_watch(clause& c, unsigned idx, clause_offset cls_off) {
+        std::swap(c[1], c[idx]);
+        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
+        m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
+    }
+
     bool solver::propagate_literal(literal l, bool update) {
         literal l1, l2;
 
@@ -1139,6 +1162,8 @@ namespace sat {
                 if (c[0] == not_l)
                     std::swap(c[0], c[1]);
                 CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";);
+
+
                 if (c.was_removed() || c.size() == 1 || c[1] != not_l) {
                     // Remark: this method may be invoked when the watch lists are not in a consistent state,
                     // and may contain dead/removed clauses, or clauses with removed literals.
@@ -1155,58 +1180,65 @@ namespace sat {
                     break;
                 }
                 VERIFY(c[1] == not_l);
-                literal* l_it = c.begin() + 2;
-                literal* l_end = c.end();
+                
+                unsigned undef_index = 0;
                 unsigned assign_level = curr_level;
                 unsigned max_index = 1;
-                for (; l_it != l_end; ++l_it) {
-                    if (value(*l_it) != l_false) {
-                        c[1] = *l_it;
-                        *l_it = not_l;
-                        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
-                        m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
+                unsigned num_undef = 0;
+                unsigned sz = c.size();
+
+                for (unsigned i = 2; i < sz && num_undef <= 1; ++i) {
+                    literal lit = c[i];
+                    switch (value(lit)) {
+                    case l_true:
+                        it2->set_clause(lit, cls_off);
+                        it2++;
                         goto end_clause_case;
-                    }
-                }
-                SASSERT(value(c[0]) == l_false || value(c[0]) == l_undef);
-                if (assign_level != scope_lvl()) {
-                    for (unsigned i = 2; i < c.size(); ++i) {
-                        unsigned level = lvl(c[i]);
+                    case l_undef:
+                        undef_index = i;
+                        ++num_undef;
+                        break;
+                    case l_false: {
+                        unsigned level = lvl(lit);
                         if (level > assign_level) {
                             assign_level = level;
                             max_index = i;
                         }
+                        break;
                     }
-                    IF_VERBOSE(20, verbose_stream() << "lower assignment level " << assign_level << " scope: " << scope_lvl() << "\n");
+                    }
+                }
+
+                if (value(c[0]) == l_false)
+                    assign_level = std::max(assign_level, lvl(c[0]));
+
+                if (undef_index != 0) {       
+                    set_watch(c, undef_index, cls_off);
+                    if (value(c[0]) == l_false && num_undef == 1) {   
+                        std::swap(c[0], c[1]);
+                        propagate_clause(c, update, assign_level, cls_off);
+                    }
+                    goto end_clause_case;
                 }
 
                 if (value(c[0]) == l_false) {
-                    assign_level = std::max(assign_level, lvl(c[0]));
                     c.mark_used();
                     CONFLICT_CLEANUP();
                     set_conflict(justification(assign_level, cls_off));
                     return false;
                 }
-                else {
-                    if (max_index != 1) {
-                        IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n");
-                        std::swap(c[1], c[max_index]);
-                        m_watches[(~c[1]).index()].push_back(watched(c[0], cls_off));
-                    }
-                    else {
-                        *it2 = *it;
-                        it2++;
-                    }
-                    m_stats.m_propagate++;
-                    c.mark_used();
-                    assign_core(c[0], justification(assign_level, cls_off));
-                    if (update && c.is_learned() && c.glue() > 2) {
-                        unsigned glue;
-                        if (num_diff_levels_below(c.size(), c.begin(), c.glue() - 1, glue)) {
-                            c.set_glue(glue);
-                        }
-                    }
+
+                // value(c[0]) == l_undef
+
+                if (max_index != 1) {
+                    IF_VERBOSE(20, verbose_stream() << "swap watch for: " << c[1] << " " << c[max_index] << "\n");
+                    set_watch(c, max_index, cls_off);
                 }
+                else {
+                    *it2 = *it;
+                    it2++;
+                }
+                propagate_clause(c, update, assign_level, cls_off);
             end_clause_case:
                 break;
             }
@@ -3425,6 +3457,7 @@ namespace sat {
                         unmark_lit(~l2);
                     }
                 }
+#if ENABLE_TERNARY
                 else if (w.is_ternary_clause()) {
                     literal l2 = w.get_literal1();
                     literal l3 = w.get_literal2();
@@ -3437,6 +3470,7 @@ namespace sat {
                         unmark_lit(~l2);
                     }
                 }
+#endif
                 else {
                     // May miss some binary/ternary clauses, but that is ok.
                     // I sort the watch lists at every simplification round.
@@ -3581,7 +3615,7 @@ namespace sat {
 
         auto cleanup_watch = [&](literal lit) {
             for (auto const& w : get_wlist(lit)) {
-                IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
+                IF_VERBOSE(1, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
             }
         };
         for (bool_var v : m_vars_to_free) {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 2b341185f..88c404c7c 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -305,9 +305,11 @@ namespace sat {
         void mk_bin_clause(literal l1, literal l2, sat::status st);
         void mk_bin_clause(literal l1, literal l2, bool learned) { mk_bin_clause(l1, l2, learned ? sat::status::redundant() : sat::status::asserted()); }
         bool propagate_bin_clause(literal l1, literal l2);
+#if ENABLE_TERNARY
         clause * mk_ter_clause(literal * lits, status st);
         bool attach_ter_clause(clause & c, status st);
         bool propagate_ter_clause(clause& c);
+#endif
         clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
         bool has_variables_to_reinit(clause const& c) const;
         bool has_variables_to_reinit(literal l1, literal l2) const;
@@ -480,6 +482,8 @@ namespace sat {
         bool should_propagate() const;
         bool propagate_core(bool update);
         bool propagate_literal(literal l, bool update);
+        void propagate_clause(clause& c, bool update, unsigned assign_level, clause_offset cls_off);
+        void set_watch(clause& c, unsigned idx, clause_offset cls_off);
         
         // -----------------------
         //
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index d2e2ffc94..7c4e4fb73 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -34,7 +34,7 @@ class params_ref;
 class reslimit;
 class statistics;
 
-#define ENABLE_TERNARY true
+#define ENABLE_TERNARY false
 
 namespace sat {
 #define SAT_VB_LVL 10
diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp
index 8811a4e74..dedbf45f0 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -71,6 +71,7 @@ namespace sat {
         VERIFY(found);
     }
 
+#if ENABLE_TERNARY
     void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) {
         watched w(l1, l2);
         watch_list::iterator it = wlist.begin(), end = wlist.end();
@@ -96,6 +97,7 @@ namespace sat {
         }
 #endif
     }
+#endif
 
     void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
         watch_list::iterator end = wlist.end();
@@ -118,9 +120,11 @@ namespace sat {
                 if (w.is_learned())
                     out << "*";
                 break;
+#if ENABLE_TERNARY
             case watched::TERNARY:
                 out << "(" << w.get_literal1() << " " << w.get_literal2() << ")";
                 break;
+#endif
             case watched::CLAUSE:
                 out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")";
                 break;
diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h
index 3e27f53c0..7e88c8c51 100644
--- a/src/sat/sat_watched.h
+++ b/src/sat/sat_watched.h
@@ -40,7 +40,11 @@ namespace sat {
     class watched {
     public:
         enum kind {
-            BINARY = 0, TERNARY, CLAUSE, EXT_CONSTRAINT
+            BINARY = 0, 
+#if ENABLE_TERNARY
+            TERNARY,
+#endif
+            CLAUSE, EXT_CONSTRAINT
         };
     private:
         size_t   m_val1;
@@ -55,6 +59,7 @@ namespace sat {
             SASSERT(learned || is_binary_non_learned_clause());
         }
 
+#if ENABLE_TERNARY
         watched(literal l1, literal l2) {
             SASSERT(l1 != l2);
             if (l1.index() > l2.index())
@@ -65,6 +70,7 @@ namespace sat {
             SASSERT(get_literal1() == l1);
             SASSERT(get_literal2() == l2);
         }
+#endif
 
         unsigned val2() const { return m_val2; }
 
@@ -95,9 +101,11 @@ namespace sat {
 
         void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); }
                 
+#if ENABLE_TERNARY
         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); }
+#endif
 
         bool is_clause() const { return get_kind() == CLAUSE; }
         clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast<clause_offset>(m_val1); }
@@ -117,7 +125,9 @@ namespace sat {
     };
 
     static_assert(0 <= watched::BINARY && watched::BINARY <= 3, "");
+#if ENABLE_TERNARY
     static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, "");
+#endif
     static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, "");
     static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, "");
 
@@ -125,8 +135,10 @@ namespace sat {
         bool operator()(watched const & w1, watched const & w2) const {
             if (w2.is_binary_clause()) return false;
             if (w1.is_binary_clause()) return true;
+#if ENABLE_TERNARY
             if (w2.is_ternary_clause()) return false;
             if (w1.is_ternary_clause()) return true;
+#endif
             return false;
         }
     };