diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 1c8d2e832..a306c024a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1328,7 +1328,10 @@ lbool core::check(unsigned level) { if (lp_settings().get_cancel_flag()) return l_undef; - if (params().arith_nl_nra_before_lemma_return() && should_run_bounded_nlsat()) { + if (params().arith_nl_nra_before_lemma_return() + && lp_settings().stats().m_nla_calls > 0 + && lp_settings().stats().m_nla_calls % params().arith_nl_delay() == 0 + && should_run_bounded_nlsat()) { ret = bounded_nlsat(); if (ret == l_true) return l_true;