diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index cfa643bb9..9ef0d88db 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -148,10 +148,9 @@ public: // returns true if the combination of the Horner's schema and Grobner Basis should be called bool need_to_call_algebraic_methods() const { return - lp_settings().stats().m_nla_calls < 20 || lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; - } - + } + lbool incremental_linearization(bool); svector sorted_rvars(const factor& f) const;