Upgrade cvc5 from 1.2.1 to 1.3.4#8886
Merged
Merged
Conversation
There was a problem hiding this comment.
Pull request overview
Updates GitHub Actions workflows to use cvc5 v1.3.3 for CI and release packaging, aligning the toolchain version across pipelines.
Changes:
- Bumped
cvc5-versionfrom1.2.1to1.3.3in release workflow - Bumped
cvc5-versionfrom1.2.1to1.3.3in PR checks workflow - Bumped
cvc5-versionfrom1.2.1to1.3.3in coverage workflow
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| .github/workflows/release-packages.yaml | Updates the cvc5 version used when uploading release assets |
| .github/workflows/pull-request-checks.yaml | Updates the cvc5 version used in pull request CI checks |
| .github/workflows/coverage.yaml | Updates the cvc5 version used in coverage runs |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
kroening
approved these changes
Mar 24, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8886 +/- ##
========================================
Coverage 80.55% 80.55%
========================================
Files 1707 1707
Lines 189051 189051
Branches 73 73
========================================
+ Hits 152298 152299 +1
+ Misses 36753 36752 -1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
cvc5 1.3.4 (released 2026-05-07) is the latest patch on the 1.3
line. The previous pin (1.2.1) was the last of the 1.2.x line, so
this bump skips 1.3.0/1.3.1/1.3.2/1.3.3. Notable user-visible
changes from upstream release notes since 1.2.1:
- 1.3.0: behavioural change -- distinct constraints are now
handled lazily; this can shift solving times in either
direction on adversarial inputs and is the most likely
source of any future performance bisect to land on this
commit.
- 1.3.2: variable-elimination fix for quantified formulas with
variable shadowing; arithmetic-solver updates.
- 1.3.3: get-assertions no longer clears solving state; SyGuS
fix for unconstrained queries; minor non-linear arithmetic
strategy tweak.
- 1.3.4: soundness fix in the --learned-rewrite preprocessing
pass; SymFPU divider-encoding fix that closes upstream cvc5
issues #9505 / #11139 / #12335 (we already carry a marker
for #11139 at regression/smt2_solver/fp-issues/cvc5-11139
-fma.smt2); parser fixes for indexed bit-vector operators of
width >= 2^32; theory-combination fixes for arrays + non-
linear arithmetic.
cvc5 1.3.4 raises its build-time toolchain minimum (GCC >= 10 /
Clang >= 12), but we only consume the prebuilt static binaries
so this does not affect us. All five binary assets we depend on
(Linux x86_64/arm64, macOS x86_64/arm64, Windows x86_64 static
zips) are published on the cvc5-1.3.4 release.
CI exercises the new binary via the cvc5 regression suites under
regression/cbmc-incr-smt2/ and regression/cbmc-output-file/dump
-smt-formula/ on every run.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The cvc5 download-and-install snippet was duplicated 14 times across
.github/workflows/{pull-request-checks,coverage,release-packages}.yaml,
with only the asset filename varying by runner platform. The Z3
download was duplicated twice in the two Windows jobs of
pull-request-checks.yaml, hard-coded to z3-4.8.10 from 2021. With the
inline form a future cvc5 bump touched 14 places verbatim and a Z3
bump touched 2 places verbatim.
This commit introduces two composite actions:
- .github/actions/install-cvc5 -- handles all five supported
runner platforms (Linux x86_64/arm64, macOS x86_64/arm64,
Windows x86_64) by dispatching on runner.os / runner.arch. The
Linux/macOS branch uses bash + wget + unzip; the Windows branch
uses pwsh + Invoke-WebRequest + Expand-Archive and appends to
$env:GITHUB_PATH so the binary is discoverable in subsequent
steps. Both branches verify the install with `cvc5 --version`
(Windows uses an absolute path because the PATH update only takes
effect from the next step onward).
- .github/actions/install-z3 -- Windows-only (Linux installs Z3
via apt and macOS via brew, neither requires a separate version
pin). Mirrors the cvc5 action's Windows branch.
The 16 existing inline blocks (10 in pull-request-checks.yaml, 1 in
coverage.yaml, 3 in release-packages.yaml, plus 2 Z3 blocks inside
the Windows jobs of pull-request-checks.yaml) are replaced with
`uses:` references that read the new env.cvc5-version /
env.z3-version variables. A future bump is now one literal change
per workflow (and pulls in any improvements to the install-cvc5 /
install-z3 actions for free).
The refactor is behaviour-preserving:
- same upstream URL pattern for both binaries;
- same install location (/usr/local/bin on Linux/macOS, C:\tools
on Windows);
- same PATH update strategy on Windows;
- same `cvc5 --version` / `z3 --version` self-check.
actionlint reports no new warnings introduced by this change
(pre-existing save-always and shellcheck SC2086 warnings on
unrelated steps are unchanged in count).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Until now the install-cvc5 and install-z3 composite actions trusted
whatever bytes were served by github.com for a given release tag.
That works in practice -- and the tag-based URL is itself a strong
hint of integrity -- but it does not catch:
- upstream republishing a tag with different content (uncommon for
cvc5 / Z3 releases, but observed elsewhere);
- a transparent-proxy or mirror compromise on the runner; or
- a typo in the version pin that happens to resolve to a different
real artifact.
This commit pins the expected SHA-256 of every supported (binary,
version, platform) tuple inside the composite actions, computes the
hash of the downloaded archive, and aborts the step on mismatch
*before* unzipping or moving the binary onto PATH. The hashes are
hard-coded in a small case statement next to the asset names, so
the next bump is mechanically "version + 5 cvc5 hashes (1 z3 hash)
in the same PR"; an unknown version is rejected with a pointer to
the file to edit.
Hashes for cvc5 1.3.4 were obtained from the upstream release API
(.assets[].digest) and cross-checked against locally computed
sha256sum of the same downloads:
cvc5-Linux-x86_64-static.zip dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6
cvc5-Linux-arm64-static.zip 2a4c108367f20b0c8990abd6b9535a5d62e08908d471d4671c00734e408f85bc
cvc5-macOS-x86_64-static.zip 5a7976affaf37dcf03ee44c3d0297c8e0ba08afd44ac832dab97400da726b852
cvc5-macOS-arm64-static.zip 3840aa53f6ee6fc357415dcfe291d7f5ffec6cfb1ccca6fef64120a0d2be4cb6
cvc5-Win64-x86_64-static.zip 279fe7e95810cfb62433fcfc2932f35325a665f32d3697ff33f75e31d5c6a179
The Z3 4.8.10 release predates the API .digest field, so the hash
z3-4.8.10-x64-win.zip 688c8f96f4f89cb474de4ecd740c812c6e695318e4b50fd790722513285b2fcb
was computed locally from the upstream artifact.
Implementation notes:
- On Linux/macOS the verification uses `sha256sum` if available and
falls back to `shasum -a 256` (macOS does not ship sha256sum but
does ship shasum).
- On Windows the verification uses PowerShell's built-in
Get-FileHash -Algorithm SHA256.
- Inputs to the verification step are passed via `env:` rather than
interpolated into the shell script, so an attacker-controlled
version string cannot inject shell or PowerShell commands.
- The hash table is the single source of truth for both the asset
name and the hash, eliminating the previous risk of the two
drifting apart.
actionlint reports no new warnings introduced by this change.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
changed the title
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
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.
cvc5 1.3.3 (released 2026-02-25) includes bug fixes and performance improvements. Static binaries are available for all CI platforms including Windows.