Skip to content

Commit 67b688b

Browse files
committed
Migrate from cvc5-1.1.1 to 1.3.1
This is primarily motivated by bringing in the changes from cvc5/cvc5#11861, which brings in a newer version of `libpoly` that is compatible with recent versions of Apple `clang++`. (See SRI-CSL/libpoly#85 for the relevant `libpoly` patch.) This, in turn, allows `libpoly` to build with `macos-15` CI runners. Note that recent versions of `cvc5` no longer require patching out the use of the `ld.gold` linker on Windows, so we can remove the corresponding `what4-solvers` patch that does this.
1 parent 6e7d59a commit 67b688b

File tree

4 files changed

+2
-46
lines changed

4 files changed

+2
-46
lines changed

.github/ci.sh

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -119,12 +119,6 @@ build_cvc4() {
119119
build_cvc5() {
120120
pushd repos/cvc5
121121
if $IS_WIN ; then
122-
# GitHub Actions comes preinstalled with Chocolatey's mingw package, which
123-
# includes the ld.gold linker. This does not play nicely with MSYS2's
124-
# mingw-w64-x86_64-gcc, so we must prevent CMake from using ld.gold.
125-
# (Ideally, there would be a CMake configuration option to accomplish this,
126-
# but I have not found one.)
127-
patch -p1 -i $PATCHES/cvc5-no-ld-gold.patch
128122
# Why do we manually override Python_EXECUTABLE below? GitHub Actions comes
129123
# with multiple versions of Python pre-installed, and for some bizarre
130124
# reason, CMake always tries to pick the latest version, even if it is not

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Currently, `what4-solvers` offers the following solver versions:
1313
* Bitwuzla - [0.7.0](https://github.com/bitwuzla/bitwuzla/tree/3cf7c35b97c60016883cc19c4d6a9344a989a4d6)
1414
* Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3)
1515
* CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379)
16-
* CVC5 - [1.1.1](https://github.com/cvc5/cvc5/tree/ebfdf84d5698eeb83e0fa4e45101fe4a8f4543eb)
16+
* CVC5 - [1.3.1](https://github.com/cvc5/cvc5/tree/ea1b484fa54bfe56c0f8b3ac90a6e3e2f46441e7)
1717
* Yices - [2.6.5](https://github.com/SRI-CSL/yices2/tree/8e6297e233299631147f98659224c3118fc6a215)
1818
* Z3 - [4.8.8](https://github.com/Z3Prover/z3/tree/ad55a1f1c617a7f0c3dd735c0780fc758424c7f1) and
1919
[4.8.14](https://github.com/Z3Prover/z3/tree/df8f9d7dcb8b9f9b3de1072017b7c2b7f63f0af8)

patches/cvc5-no-ld-gold.patch

Lines changed: 0 additions & 38 deletions
This file was deleted.

repos/cvc5

Submodule cvc5 updated 3833 files

0 commit comments

Comments
 (0)