From b01fc9816f4391dfbc55d24ca37978c951aaf7c0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Sep 2019 16:20:48 -0700 Subject: [PATCH] check the settings before calling grobner basis heuristic Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 92ed6e9cf..8c514a30d 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -144,7 +144,10 @@ public: bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; } - bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; } + bool need_to_call_grobner() const { + return m_nla_settings.run_grobner() && + lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; + } lbool incremental_linearization(bool);