From 3f442ecef91b4fa8b6a9370d14d1e7f0803b1214 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 11 Dec 2019 20:07:12 -1000
Subject: [PATCH] remove m_conflict from nla_grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_grobner.cpp | 12 ++++--------
 src/math/lp/nla_grobner.h   |  1 -
 2 files changed, 4 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 44aef516e..3a9e85085 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -583,7 +583,6 @@ void grobner::superpose(equation * eq1, equation * eq2) {
 
 void grobner::register_report() {
     m_reported++;
-    m_conflict = true;
 }
 // Let a be the greatest common divider of ab and bc,
 // then ab/a is stored in b, and ac/a is stored in c
@@ -724,20 +723,17 @@ bool grobner::done() const {
         ||
         canceled()
         ||
-        m_reported > 100000
-        ||
-        m_conflict) {
+        m_reported > 0
+) {
         TRACE("grobner",
               tout << "done() is true because of ";
               if (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()) {
                   tout << "m_num_of_equations = " << num_of_equations() << "\n";
               } else if (canceled()) {
                   tout << "canceled\n";
-              } else if (m_reported > 100000) {
+              } else if (m_reported > 0) {
                   tout << "m_reported = " << m_reported;
-              } else {
-                  tout << "m_conflict = " << m_conflict;
-              }
+              } 
               tout <<    "\n";);
         return true;
     }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index f0dac37a5..46d5dcd8a 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -90,7 +90,6 @@ class grobner : common {
     nex_lt                                       m_lt;
     bool                                         m_changed_leading_term;
     unsigned                                     m_reported;
-    bool                                         m_conflict;
     bool                                         m_look_for_fixed_vars_in_rows;
 public:
     grobner(core *, intervals *);