[snapshot-regression-fix] lp: restore deterministic integer hammer gates by default (random_hammers=false)

[levnach]

Summary

Fixes a Z3 nightly snapshot-regression divergence tracked in Z3Prover/bench discussion #2703.

• Benchmark: iss-6986/small.smt2 (quantified non-linear real arithmetic)
• Originating discussion: https://github.com/Z3Prover/bench/discussions/2703
• Divergence: the recorded oracle expects sat; current z3 produces timeout.

--- small.expected.out (expected)
+++ produced (current z3)
@@ -1 +1 @@
-sat
+timeout

Root cause

Bisection over the z3 history pins the regression to #9958 (lp: gate Gomory-with-dio on genuine dio failures; separate config from runtime state). That commit bundled the earlier lia_w "randomized hammer gates" work and introduced the lp.random_hammers parameter defaulting to true.

With random_hammers=true, the periodic integer-feasibility heuristic gates (find_cube, lcube, hnf, gomory, dio) in int_solver fire at random (1/period rate, via settings().random_next(period) == 0) instead of the long-standing deterministic m_number_of_calls % period == 0 schedule.

iss-6986/small.smt2 is a quantified NRA formula whose div terms introduce integer / Diophantine reasoning routed through the int_solver dio/gomory machinery. Under the deterministic schedule the search finds a model almost immediately (~0.1s sat); under the randomized schedule it thrashes in a final-check / nlsat loop and times out. This is a deterministic regression with the default RNG seed, not flakiness.

Notably, #9958's own commit message documents the same failure mode caused by randomization on dillig/20-14 (100s → 600s timeout), and states that its default behavior is "byte-for-byte equivalent to the previous threshold logic" — which only holds with the deterministic gates.

Bisection detail (rebuilding z3 at each commit and running z3 -T:20 iss-6986/small.smt2):

commit	result
6fd303c4b (pre-#9958)	sat (~0.1s)
57fb71900 (#9958)	timeout
57fb71900 + lp.random_hammers=false	sat (~0.04s)

Fix

Default lp.random_hammers to false, restoring the deterministic hammer-gate schedule as the default (the behavior #9958 documents the default to be). Randomization stays available as an opt-in via lp.random_hammers=true. The headline dio-before-gomory improvement from #9958 — which the commit's own evaluation attributes the +33 problems to, independent of random_hammers — is preserved, as is its config/runtime-state separation bugfix.

Two-line change:

• src/math/lp/lp_params_helper.pyg: random_hammers default True → False
• src/math/lp/lp_settings.h: m_random_hammers initializer true → false

Validation

Rebuilt z3 from this branch (./configure && make -C build -j$(nproc)) and re-ran the failing benchmark with the same option the snapshot capture uses:

$ z3 -T:20 inputs/issues/iss-6986/small.smt2
sat        # ~0.04s; matches the recorded oracle

Additional sanity checks pass: trivial sat/unsat, QF_LIA integer reasoning (dio/gomory path), and the lp.random_hammers=true opt-in still functioning.

Opened as a draft for human review.

Generated by Fix a Z3 snapshot-regression divergence · 2.9K AIC · ⌖ 83.7 AIC · ⊞ 41.2K · ◷