lp: randomize the Gomory-cut gate to break period resonance

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>

src/math/lp/int_solver.cpp

@@ -220,7 +220,12 @@ namespace lp {
         bool should_gomory_cut() {
             bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() ||
                                       m_dio.some_terms_are_ignored();
-            return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
+            // Draw the decision at random instead of using a fixed "every k-th
+            // call" modulus. A deterministic period can phase-lock with the
+            // search on some UNSAT families and drown the solver in theory
+            // conflicts while the Diophantine handler is starved; randomizing
+            // the gate (same 1/period expected rate) breaks that resonance.
+            return dio_allows_gomory && settings().random_next(settings().m_int_gomory_cut_period) == 0;
         }
 
         bool should_solve_dioph_eq() {