diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
index bbdedab86..8da933fb2 100644
--- a/src/sat/sat_cleaner.cpp
+++ b/src/sat/sat_cleaner.cpp
@@ -64,9 +64,6 @@ 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_drat.cpp b/src/sat/sat_drat.cpp
index 306ff2493..46a608151 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -445,10 +445,6 @@ namespace sat {
             return false;
         case justification::BINARY:
             return contains(c, j.get_literal());
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            return contains(c, j.get_literal1(), j.get_literal2());
-#endif
         case justification::CLAUSE:
             return contains(s.get_clause(j));
         default:
diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp
index ab9bc8857..a655956db 100644
--- a/src/sat/sat_gc.cpp
+++ b/src/sat/sat_gc.cpp
@@ -178,33 +178,9 @@ namespace sat {
         IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
     }
 
-#if ENABLE_TERNARY
-    bool solver::can_delete3(literal l1, literal l2, literal l3) const {                                                           
-        if (value(l1) == l_true && 
-            value(l2) == l_false && 
-            value(l3) == l_false) {
-            justification const& j = m_justification[l1.var()];
-            if (j.is_ternary_clause()) {
-                watched w1(l2, l3);
-                watched w2(j.get_literal1(), j.get_literal2());
-                return w1 != w2;
-            }
-        }
-        return true;
-    }
-#endif
-
     bool solver::can_delete(clause const & c) const {
         if (c.on_reinit_stack())
             return false;
-#if ENABLE_TERNARY
-        if (c.size() == 3) {
-            return
-                can_delete3(c[0],c[1],c[2]) &&
-                can_delete3(c[1],c[0],c[2]) &&
-                can_delete3(c[2],c[0],c[1]);
-        }
-#endif
         literal l0 = c[0];
         if (value(l0) != l_true)
             return true;
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index a6086d8a7..223e58677 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -26,13 +26,6 @@ namespace sat {
     integrity_checker::integrity_checker(solver const & _s):
         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) {
@@ -65,18 +58,6 @@ 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";
-                   s.display_watch_list(tout, s.get_wlist(~c[0]));
-                   tout << "\n";);
-            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;
-        }
-#endif
         {
             if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
                 bool on_prop_stack = false;
@@ -174,13 +155,6 @@ 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_justification.h b/src/sat/sat_justification.h
index 1fc97a38c..f83173aa7 100644
--- a/src/sat/sat_justification.h
+++ b/src/sat/sat_justification.h
@@ -22,11 +22,7 @@ namespace sat {
     
     class justification {
     public:
-        enum kind { NONE = 0, BINARY = 1, 
-#if ENABLE_TERNARY
-            TERNARY = 2, 
-#endif 
-            CLAUSE = 3, EXT_JUSTIFICATION = 4};
+        enum kind { NONE = 0, BINARY = 1, CLAUSE = 2, EXT_JUSTIFICATION = 3};
     private:
         unsigned m_level;
         size_t m_val1;
@@ -36,9 +32,7 @@ namespace sat {
     public:
         justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {}
         explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {}
-#if ENABLE_TERNARY
-        justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
-#endif
+
         explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {}
         static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); }
         
@@ -51,12 +45,6 @@ namespace sat {
         bool is_binary_clause() const { return m_val2 == BINARY; }
         literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); }
 
-#if ENABLE_TERNARY
-        bool is_ternary_clause() const { return get_kind() == TERNARY; }
-        literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); }
-        literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
-#endif
-
         bool is_clause() const { return m_val2 == CLAUSE; }
         clause_offset get_clause_offset() const { return m_val1; }
         
@@ -73,11 +61,6 @@ namespace sat {
         case justification::BINARY:
             out << "binary " << j.get_literal();
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            out << "ternary " << j.get_literal1() << " " << j.get_literal2();
-            break;
-#endif
         case justification::CLAUSE:
             out << "clause";
             break;
diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp
index 4c4b9ecaf..df55aecd7 100644
--- a/src/sat/sat_proof_trim.cpp
+++ b/src/sat/sat_proof_trim.cpp
@@ -125,10 +125,6 @@ namespace sat {
                     in_coi |= m_in_coi.contains(lit.index());                
             else if (js.is_binary_clause())
                 in_coi = m_in_coi.contains(js.get_literal().index());
-#if ENABLE_TERNARY
-            else if (js.is_ternary_clause())
-                in_coi = m_in_coi.contains(js.get_literal1().index()) || m_in_coi.contains(js.get_literal2().index());
-#endif
             else
                 UNREACHABLE(); // approach does not work for external justifications
             
@@ -226,12 +222,6 @@ namespace sat {
         case justification::BINARY:
             add_dependency(j.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            add_dependency(j.get_literal1());
-            add_dependency(j.get_literal2());
-            break;
-#endif
         case justification::CLAUSE: 
             for (auto lit : s.get_clause(j))
                 if (s.value(lit) == l_false)
@@ -262,13 +252,6 @@ namespace sat {
             m_clause.push_back(l);
             m_clause.push_back(j.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            m_clause.push_back(l);
-            m_clause.push_back(j.get_literal1());
-            m_clause.push_back(j.get_literal2());
-            break;
-#endif
         case justification::CLAUSE:
             s.get_clause(j).mark_used();
             IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index b67ef6a2a..9ba536091 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -271,9 +271,6 @@ 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 56dcdf0df..eea3a2475 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -448,10 +448,6 @@ namespace sat {
             if (redundant && m_par) 
                 m_par->share_clause(*this, lits[0], lits[1]);
             return nullptr;
-#if ENABLE_TERNARY
-        case 3:
-                return mk_ter_clause(lits, st);
-#endif
         default:
             return mk_nary_clause(num_lits, lits, st);
         }
@@ -545,58 +541,6 @@ 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++;
-        clause * r = alloc_clause(3, lits, st.is_redundant());
-        bool reinit = attach_ter_clause(*r, st);
-        if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
-        if (st.is_redundant())
-            m_learned.push_back(r);
-        else
-            m_clauses.push_back(r);
-        for (literal l : *r) {
-            m_touched[l.var()] = m_touch_index;
-        }
-        return r;
-    }
-
-    bool solver::attach_ter_clause(clause & c, sat::status st) {
-        VERIFY(ENABLE_TERNARY);
-        bool reinit = false;
-        if (m_config.m_drat) m_drat.add(c, st);
-        TRACE("sat_verbose", tout << c << "\n";);
-        SASSERT(!c.was_removed());
-        m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
-        m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
-        m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
-        if (!at_base_lvl()) 
-            reinit = propagate_ter_clause(c);        
-        return reinit;
-    }
-
-    bool solver::propagate_ter_clause(clause& c) {
-        bool reinit = false;
-        if (value(c[1]) == l_false && value(c[2]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2]));
-            reinit = !c.is_learned();
-        }
-        else if (value(c[0]) == l_false && value(c[2]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2]));
-            reinit = !c.is_learned();
-        }
-        else if (value(c[0]) == l_false && value(c[1]) == l_false) {
-            m_stats.m_ter_propagate++;
-            assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1]));
-            reinit = !c.is_learned();
-        }
-        return reinit;
-    }
-#endif
-
     clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_stats.m_mk_clause++;
         clause * r = alloc_clause(num_lits, lits, st.is_redundant());
@@ -663,13 +607,7 @@ 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());
+        reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
     }
 
     void solver::set_learned(clause& c, bool redundant) {
@@ -917,12 +855,6 @@ namespace sat {
     }
 
     void solver::detach_clause(clause& c) {
-#if ENABLE_TERNARY
-        if (c.size() == 3) {
-            detach_ter_clause(c);
-            return;
-        }
-#endif
         detach_nary_clause(c);
     }
 
@@ -932,14 +864,6 @@ 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
-
     // -----------------------
     //
     // Basic
@@ -1123,31 +1047,6 @@ namespace sat {
                 *it2 = *it;
                 it2++;
                 break;
-#if ENABLE_TERNARY
-            case watched::TERNARY: {
-                lbool val1, val2;
-                l1 = it->get_literal1();
-                l2 = it->get_literal2();
-                val1 = value(l1);
-                val2 = value(l2);
-                if (val1 == l_false && val2 == l_undef) {
-                    m_stats.m_ter_propagate++;
-                    assign_core(l2, justification(std::max(curr_level, lvl(l1)), l1, not_l));
-                }
-                else if (val1 == l_undef && val2 == l_false) {
-                    m_stats.m_ter_propagate++;
-                    assign_core(l1, justification(std::max(curr_level, lvl(l2)), l2, not_l));
-                }
-                else if (val1 == l_false && val2 == l_false) {
-                    CONFLICT_CLEANUP();
-                    set_conflict(justification(std::max(curr_level, lvl(l1)), l1, not_l), ~l2);
-                    return false;
-                }
-                *it2 = *it;
-                it2++;
-                break;
-            }
-#endif
             case watched::CLAUSE: {
                 if (value(it->get_blocked_literal()) == l_true) {
                     TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
@@ -2534,12 +2433,6 @@ namespace sat {
             case justification::BINARY:
                 process_antecedent(~(js.get_literal()), num_marks);
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                process_antecedent(~(js.get_literal1()), num_marks);
-                process_antecedent(~(js.get_literal2()), num_marks);
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 unsigned i = 0;
@@ -2718,13 +2611,6 @@ namespace sat {
             SASSERT(consequent != null_literal);
             process_antecedent_for_unsat_core(~(js.get_literal()));
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            SASSERT(consequent != null_literal);
-            process_antecedent_for_unsat_core(~(js.get_literal1()));
-            process_antecedent_for_unsat_core(~(js.get_literal2()));
-            break;
-#endif
         case justification::CLAUSE: {
             clause & c = get_clause(js);
             unsigned i = 0;
@@ -2861,12 +2747,6 @@ namespace sat {
         case justification::BINARY:
             level = update_max_level(js.get_literal(), level, unique_max);
             return level;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            level = update_max_level(js.get_literal1(), level, unique_max);
-            level = update_max_level(js.get_literal2(), level, unique_max);
-            return level;
-#endif
         case justification::CLAUSE: 
             for (literal l : get_clause(js)) 
                 level = update_max_level(l, level, unique_max);
@@ -3218,15 +3098,6 @@ namespace sat {
                     return false;
                 }
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                if (!process_antecedent_for_minimization(~(js.get_literal1())) ||
-                    !process_antecedent_for_minimization(~(js.get_literal2()))) {
-                    reset_unmark(old_size);
-                    return false;
-                }
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 unsigned i   = 0;
@@ -3382,12 +3253,6 @@ namespace sat {
             case justification::BINARY:
                 update_lrb_reasoned(js.get_literal());
                 break;
-#if ENABLE_TERNARY
-            case justification::TERNARY:
-                update_lrb_reasoned(js.get_literal1());
-                update_lrb_reasoned(js.get_literal2());
-                break;
-#endif
             case justification::CLAUSE: {
                 clause & c = get_clause(js);
                 for (literal l : c) {
@@ -3457,20 +3322,6 @@ namespace sat {
                         unmark_lit(~l2);
                     }
                 }
-#if ENABLE_TERNARY
-                else if (w.is_ternary_clause()) {
-                    literal l2 = w.get_literal1();
-                    literal l3 = w.get_literal2();
-                    if (is_marked_lit(l2) && is_marked_lit(~l3) && l0 != ~l3) {
-                        // eliminate ~l3 from lemma because we have the clause l \/ l2 \/ l3
-                        unmark_lit(~l3);
-                    }
-                    else if (is_marked_lit(~l2) && is_marked_lit(l3) && l0 != ~l2) {
-                        // eliminate ~l2 from lemma because we have the clause l \/ l2 \/ l3
-                        unmark_lit(~l2);
-                    }
-                }
-#endif
                 else {
                     // May miss some binary/ternary clauses, but that is ok.
                     // I sort the watch lists at every simplification round.
@@ -3735,17 +3586,6 @@ namespace sat {
             }
             else {
                 clause & c = *(cw.get_clause());
-#if ENABLE_TERNARY
-                if (ENABLE_TERNARY && c.size() == 3) {
-                    if (propagate_ter_clause(c) && !at_base_lvl())
-                        m_clauses_to_reinit[j++] = cw;                
-                    else if (has_variables_to_reinit(c) && !at_base_lvl())
-                        m_clauses_to_reinit[j++] = cw;
-                    else 
-                        c.set_reinit_stack(false);
-                    continue;
-                }
-#endif
                 detach_clause(c);
                 attach_clause(c, reinit);
                 if (reinit && !at_base_lvl()) 
@@ -4012,12 +3852,6 @@ namespace sat {
         case justification::BINARY:
             out << "binary " << js.get_literal() << "@" << lvl(js.get_literal());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " ";
-            out << js.get_literal2() << "@" << lvl(js.get_literal2());
-            break;
-#endif
         case justification::CLAUSE: {
             out << "(";
             bool first = true;
@@ -4677,24 +4511,14 @@ namespace sat {
             if (!check_domain(lit, ~js.get_literal())) return false;
             s |= m_antecedents.find(js.get_literal().var());
             break;
-#if ENABLE_TERNARY
-        case justification::TERNARY:
-            if (!check_domain(lit, ~js.get_literal1()) ||
-                !check_domain(lit, ~js.get_literal2())) return false;
-            s |= m_antecedents.find(js.get_literal1().var());
-            s |= m_antecedents.find(js.get_literal2().var());
-            break;
-#endif
         case justification::CLAUSE: {
             clause & c = get_clause(js);
             for (literal l : c) {
                 if (l != lit) {
-                    if (check_domain(lit, ~l) && all_found) {
-                        s |= m_antecedents.find(l.var());
-                    }
-                    else {
-                        all_found = false;
-                    }
+                    if (check_domain(lit, ~l) && all_found) 
+                        s |= m_antecedents.find(l.var());                    
+                    else 
+                        all_found = false;                    
                 }
             }
             break;
@@ -4729,12 +4553,11 @@ namespace sat {
 
     bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
         index_set s;
-        if (m_antecedents.contains(lit.var())) {
+        if (m_antecedents.contains(lit.var())) 
             return true;
-        }
-        if (assumptions.contains(lit)) {
-            s.insert(lit.index());
-        }
+        
+        if (assumptions.contains(lit)) 
+            s.insert(lit.index());        
         else {
             if (!extract_assumptions(lit, s)) {
                 SASSERT(!m_todo_antecedents.empty());
@@ -4806,7 +4629,7 @@ namespace sat {
             clause_vector const & cs = *(vs[i]);
             for (clause* cp : cs) {
                 clause & c = *cp;
-                if (ENABLE_TERNARY && c.size() == 3)
+                if (c.size() == 3)
                     num_ter++;
                 else
                     num_cls++;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 88c404c7c..2e53e4620 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -305,11 +305,6 @@ 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;
@@ -345,7 +340,6 @@ namespace sat {
         void detach_bin_clause(literal l1, literal l2, bool learned);
         void detach_clause(clause & c);
         void detach_nary_clause(clause & c);
-        void detach_ter_clause(clause & c);
         void push_reinit_stack(clause & c);
         void push_reinit_stack(literal l1, literal l2);
 
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 7c4e4fb73..4e119a2ae 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -34,8 +34,6 @@ class params_ref;
 class reslimit;
 class statistics;
 
-#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 dedbf45f0..5573212f5 100644
--- a/src/sat/sat_watched.cpp
+++ b/src/sat/sat_watched.cpp
@@ -71,34 +71,6 @@ 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();
-        watch_list::iterator it2 = it;
-        bool found = false;
-        for (; it != end; ++it) {
-            if (!found && w == *it) {
-                found = true;
-            }
-            else {
-                *it2 = *it;
-                ++it2;    
-            }    
-        }
-        wlist.set_end(it2);
-#if 0
-        VERIFY(found);
-        for (watched const& w2 : wlist) {
-            if (w2 == w) {
-                std::cout << l1 << " " << l2 << "\n";
-            }
-            //VERIFY(w2 != w);
-        }
-#endif
-    }
-#endif
-
     void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {
         watch_list::iterator end = wlist.end();
         for (; it != end; ++it, ++it2) 
@@ -120,11 +92,6 @@ 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 7e88c8c51..6d91434db 100644
--- a/src/sat/sat_watched.h
+++ b/src/sat/sat_watched.h
@@ -40,11 +40,7 @@ namespace sat {
     class watched {
     public:
         enum kind {
-            BINARY = 0, 
-#if ENABLE_TERNARY
-            TERNARY,
-#endif
-            CLAUSE, EXT_CONSTRAINT
+            BINARY = 0, CLAUSE, EXT_CONSTRAINT
         };
     private:
         size_t   m_val1;
@@ -59,18 +55,6 @@ 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())
-                std::swap(l1, l2);
-            m_val1 = l1.to_uint();
-            m_val2 = static_cast<unsigned>(TERNARY) + (l2.to_uint() << 2);
-            SASSERT(is_ternary_clause());
-            SASSERT(get_literal1() == l1);
-            SASSERT(get_literal2() == l2);
-        }
-#endif
 
         unsigned val2() const { return m_val2; }
 
@@ -101,11 +85,6 @@ 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); }
@@ -124,21 +103,14 @@ namespace sat {
         bool operator!=(watched const & w) const { return !operator==(w); }
     };
 
-    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, "");
+    static_assert(0 <= watched::BINARY && watched::BINARY <= 2, "");
+    static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 2, "");
+    static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 2, "");
 
     struct watched_lt {
         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;
         }
     };
@@ -148,8 +120,6 @@ namespace sat {
     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);
-    void erase_ternary_watch(watch_list & wlist, literal l1, literal l2);
-    void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned);
 
     class clause_allocator;
     std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext);
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index c3e43bfbe..424b20d4e 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -690,15 +690,6 @@ namespace pb {
                 inc_coeff(consequent, offset);
                 process_antecedent(js.get_literal(), offset);
                 break;
-#if ENABLE_TERNARY
-            case sat::justification::TERNARY:
-                inc_bound(offset); 
-                SASSERT (consequent != sat::null_literal);
-                inc_coeff(consequent, offset);				
-                process_antecedent(js.get_literal1(), offset);
-                process_antecedent(js.get_literal2(), offset);
-                break;
-#endif
             case sat::justification::CLAUSE: {
                 inc_bound(offset); 
                 sat::clause & c = s().get_clause(js);
@@ -1019,16 +1010,6 @@ namespace pb {
                 inc_coeff(consequent, 1);
                 process_antecedent(js.get_literal());
                 break;
-#if ENABLE_TERNARY
-            case sat::justification::TERNARY:
-                SASSERT(consequent != sat::null_literal);
-                round_to_one(consequent.var());
-                inc_bound(1);
-                inc_coeff(consequent, 1);
-                process_antecedent(js.get_literal1());
-                process_antecedent(js.get_literal2());
-                break;
-#endif
             case sat::justification::CLAUSE: {
                 sat::clause & c = s().get_clause(js);
                 unsigned i = 0;
@@ -3476,15 +3457,6 @@ namespace pb {
             ineq.push(lit, offset);
             ineq.push(js.get_literal(), offset);
             break;
-#if ENABLE_TERNARY
-        case sat::justification::TERNARY:
-            SASSERT(lit != sat::null_literal);
-            ineq.reset(offset);
-            ineq.push(lit, offset);
-            ineq.push(js.get_literal1(), offset);
-            ineq.push(js.get_literal2(), offset);
-            break;
-#endif
         case sat::justification::CLAUSE: {
             ineq.reset(offset);
             sat::clause & c = s().get_clause(js);