From bddda1674d136ae5afe5f286bdabaa681b5d7871 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 9 Apr 2019 16:54:30 -0700
Subject: [PATCH] Disable collect_equivs_of_fixed_vars() that led to long
 explanations

---
 src/util/lp/nla_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index f55c8992c..6223864af 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -1856,7 +1856,7 @@ struct solver::imp {
                 add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
             }
         }
-        collect_equivs_of_fixed_vars();
+        // collect_equivs_of_fixed_vars();
     }
 
     void collect_equivs_of_fixed_vars() {