From aa86b62d4117837eadeccb4bcbda5b4a57cad7a5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 21 Jun 2026 16:48:35 -0700 Subject: [PATCH] lp: decrement dio_calls_period toward initial on missed dio calls Fix the recovery direction: decrement (rather than increment) dio_calls_period by one on each call where the diophantine solver is not triggered, so the period shrinks back toward its initial value after being doubled on back-off, gradually re-enabling dio solving. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/int_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 725406311..b75f7e9e6 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -240,7 +240,7 @@ namespace lp { bool should_solve_dioph_eq() { bool ret = lia.settings().dio() && hit_period(settings().dio_calls_period()); if (!ret && lia.settings().dio_calls_period() > m_initial_dio_calls_period) - lia.settings().dio_calls_period() ++; + lia.settings().dio_calls_period() --; return ret; }