Preprocessing, Seeds, and Time: A Simple Sequential Portfolio for QF_NIA

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 QF_NIA. 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