Skip to content

D2: cvc5 1.1.2 and 1.4.2 both in CI, and --version reads 1.4 - #100

Merged
SwayamInSync merged 6 commits into
mainfrom
fix/cvc5-range
Oct 27, 2026
Merged

SwayamInSync merged 6 commits into
mainfrom
fix/cvc5-range

Conversation

@SwayamInSync

Copy link
Copy Markdown
Owner

CI ran the test suite only with cvc5 1.1.2, the release Ubuntu 24.04 packages. 1.4 support (#22's arrays-exp) was checked by hand. cpp-verify --version also could not read the version of cvc5 1.4:

$ PATH=cvc5-1.4.2/bin:$PATH cpp-verify --version | grep cvc5
  cvc5   unknown  .../cvc5-Linux-x86_64-static/bin/cvc5 (tested with 1.1.2)

That is because cvc5 1.1.2 prints This is cvc5 version 1.1.2, while 1.4.2 prints cvc5 1.4.2 [git 282d5e0 on branch HEAD].

This is plan item D2, part of exit criterion 9 ("cvc5 1.1.2 and 1.4.x both in CI").

Change

  • CI. The Linux release job installs cvc5 1.1.2 and the assertions job 1.4.2, the newest release. So every cvc5 test runs against both, at no extra job. From 1.2.0 the release archives name the architecture (cvc5-Linux-x86_64-static.zip), so each matrix entry names its archive.
  • --version reads either form of the version line, and names the tested range:
  cvc5   1.4.2    .../cvc5 (tested with 1.1.2 to 1.4.2)
  cvc5   1.1.2    /usr/bin/cvc5 (tested with 1.1.2 to 1.4.2)

The range is two constants in CppVerifyVersion.h, CVC5OldestTestedVersion and CVC5NewestTestedVersion, beside the Lean pin.

Tests

version.test adds a cvc5 that prints its version as 1.4 does, and every case expects the range. On main the new case prints unknown and fails.

Each mutant below, applied alone, fails version.test:

Mutant Change
M1 the version is read only after cvc5 version
M2 the row names only the oldest tested release

The 17 tests that require cvc5 pass with cvc5 1.4.2 (the static Linux release) as with 1.1.2.

Docs

  • README: the tested range, with the link to 1.4.2.
  • tooling.rst: the cvc5 releases CI runs.
  • Release notes: added to the cvc5 1.4 entry.

Checked

  • version.test and docs_coverage.test pass on this branch.
  • cpp-verify --version prints the real version of both cvc5 binaries, as shown above.

@SwayamInSync
SwayamInSync merged commit 546cfaa into main Oct 27, 2026
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant