From 1e0d49512ba480a4135302c2988e9089d330cfd6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 Jan 2022 12:00:16 -0800
Subject: [PATCH] call mux finder

---
 src/sat/sat_solver.cpp | 4 ++--
 src/sat/sat_solver.h   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 90e31b97a..4d4c2d132 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -4174,7 +4174,7 @@ namespace sat {
     lbool solver::find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes) {
         max_cliques<neg_literal> mc;
         m_user_bin_clauses.reset();
-        m_binary_clause_graph.reset();
+        // m_binary_clause_graph.reset();
         collect_bin_clauses(m_user_bin_clauses, true, false);
         hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
         for (auto const& b : m_user_bin_clauses) {
@@ -4189,7 +4189,7 @@ namespace sat {
         vector<unsigned_vector> _mutexes;
         literal_vector _lits(lits);
         if (m_ext) {
-            // m_ext->find_mutexes(_lits, mutexes);
+            m_ext->find_mutexes(_lits, mutexes);
         }
         unsigned_vector ps;
         for (literal lit : _lits) {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 74bb182e8..98fd32591 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -755,7 +755,7 @@ namespace sat {
 
         u_map<index_set>       m_antecedents;
         literal_vector         m_todo_antecedents;
-        vector<literal_vector> m_binary_clause_graph;
+        // vector<literal_vector> m_binary_clause_graph;
 
         bool extract_assumptions(literal lit, index_set& s);