Can a fixed, user-deployable tactic string — requiring no solver modification — materially improve Z3's performance on nonlinear integer arithmetic? We show that the answer is yes. Our strategy combines a 6-tactic preprocessing chain, complementary seed selection via greedy set cover, and a front-loaded time allocation (7s/2s/1s within a 10-second budget). Under a multi-run evaluation protocol (5 runs, interleaved block design), it improves Z3's solve rate by +2. 2 percentage points (pp) on a held-out test set (95% CI: +0. 9, +3. 5) and +4. 3pp on held-out validation data (95% CI: +2. 4, +6. 2). External validation on three benchmark families from distinct problem domains — termination analysis, mathematical competition, and memory verification — demonstrates cross-distribution generalization within QFNIA. All 5 benchmark sets show positive mean improvement (one-sided sign test across benchmark sets: p = 0. 031) ; all 19 individual runs confirm this pattern. The resulting strategy is a fixed tactic string that operates through Z3's public tactic API, deployable by any Z3 user. Code and data: https: //github. com/crabsatellite/z3-tactic-evolution
Alex Li (Sun,) studied this question.