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);