From 45c0f2225c313a07235ab441a0a94341a2b75948 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 11 Jan 2020 08:44:03 -0800
Subject: [PATCH] allow unlimited number of Grobner calls

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 7ded80ae5..b2bf682ff 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1398,7 +1398,7 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
 
 void core::run_grobner() {
     unsigned& quota = m_grobner_quota;
-    if (quota == 0) {
+    if (quota == 1) {
         return;
     }
     lp_settings().stats().m_grobner_calls++;
@@ -1418,7 +1418,8 @@ void core::run_grobner() {
         IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
     }
     else {
-        quota >>= 1; 
+        if (quota > 1)
+            quota--;
         IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota <<  "\n");
         IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
     }