mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 07:06:28 +00:00
a75c860899
should_gomory_cut used a deterministic schedule (m_number_of_calls % m_int_gomory_cut_period == 0). On some UNSAT QF_LIA families (e.g. rings_preprocessed, cut_lemmas) this fixed period phase-locks with the search: the solver drowns in theory conflicts (~32k vs ~2k) while the Diophantine tightening that would close the proof is starved, causing timeouts that vanish when the period is changed (4 vs 5). Replace the modulus with a random draw of the same expected rate (random_next(period) == 0). This breaks the deterministic resonance while preserving the average cut frequency. Locally this turns the whole regressing band from timeouts / ~23s into sub-second-to-seconds solves, with no slowdown observed on a regression sample and lp unit tests passing. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||