From 73988d7c126ba8988ccb9a46abe208a4062cb2de Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Mar 2026 13:51:56 -1000 Subject: [PATCH] Throttle early bounded_nlsat to fire every arith.nl.delay NLA calls The unconditional early call drained rlimit budget on QF_NIA problems where nlsat returns l_undef. Only try early nlsat every arith.nl.delay (default 10) NLA calls, combined with the existing exponential backoff. This preserves the benefit for stuck QF_NRA problems while reducing overhead on problems where the lemma pipeline is effective. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/nla_core.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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;