ci: pin z3 on windows to 4.15.2 (official release binary) - #1081
Merged
Conversation
The windows job installed z3 from msys2's rolling package repo, so every CI run picked up whatever version msys2 currently ships. When msys2 moved from z3 4.15.2 to 4.16.0, three solver tests started failing on windows only (negative-numbers-zero-comp, negative-numbers-zero-comp-simpleassert, eq-issue-with-length-cex-bug679) — the same queries pass with the official upstream z3 4.16.0 build on other platforms, so this is specific to the msys2 4.16.0 package. Install z3 from the official Z3Prover release archive instead, pinned to 4.15.2 (the last version windows CI was green on), exactly like bitwuzla and cvc5 already are in this job. Solver upgrades now happen via an explicit diff instead of silently on the runner. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
elopez
approved these changes
Jul 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
The
build (windows-latest)job currently fails on every PR (e.g. #1080) with 3 test failures:negative-numbers-zero-comp— expected 1 counterexample, got 0negative-numbers-zero-comp-simpleassert— expected 1 counterexample, got 0eq-issue-with-length-cex-bug679— cex found but doesn't match the expected modelThis is unrelated to any recent hevm change: the windows job installs z3 via msys2's rolling package repo (
z3:pin the pacboy list), so each run silently picks up whatever msys2 currently ships.main(Jul 6): msys2 z3 4.15.2-5I could not reproduce any of the three failures with the official z3 4.16.0 release binary (macOS):
hevm symboliconassert(x >= 0)finds the counterexample, and the bug679 equivalence check produces the exact expected0xff…fe0ccalldata. So the breakage looks specific to the msys2 4.16.0 package (or z3-4.16-on-windows), not to upstream z3 4.16 semantics generally.Fix
Install z3 on windows from the official Z3Prover release archive, pinned to 4.15.2 (the last version windows CI was green on) — exactly the pattern this job already uses for bitwuzla (0.8.2) and cvc5 (1.3.0).
$Z3_PATHis added to the test and rpc-test PATH exports.Solver upgrades on windows now happen via an explicit, bisectable diff instead of silently on the runner image.
🤖 Generated with Claude Code