mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 08:30:28 +00:00
Code Activity

lp: decrement dio_calls_period toward initial on missed dio calls

Browse source 
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>
This commit is contained in:
Lev Nachmanson 2026-06-21 16:48:35 -07:00
parent 9f290ca0b8
commit aa86b62d41
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/int_solver.cpp
View file

@ -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;
}