From 9f290ca0b87c24712a4949e6d43bfb06dc85e6e3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 21 Jun 2026 14:53:55 -0700 Subject: [PATCH] lp: linearly recover dio_calls_period on missed dio calls Increment dio_calls_period by one on each call where the diophantine solver is not triggered (until it returns to the initial period), gradually re-enabling dio solving after it was backed off, instead of leaving the period at its doubled value indefinitely. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/math/lp/int_solver.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index cb22b0635..725406311 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -238,7 +238,10 @@ namespace lp { } bool should_solve_dioph_eq() { - return lia.settings().dio() && hit_period(settings().dio_calls_period()); + 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() ++; + return ret; } // HNF