diff --git a/.github/ci.sh b/.github/ci.sh index 2f08284..83498cb 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -44,6 +44,8 @@ build_abc() { build_bitwuzla() { pushd repos/bitwuzla + # Backport a fix for https://github.com/bitwuzla/bitwuzla/issues/118 + patch -p1 -i $PATCHES/bitwuzla-fix-missing-includes-gcc14.patch if [ "$GITHUB_MATRIX_OS" == 'ubuntu-20.04' ] ; then # Ubuntu 20.04 uses an older version of glibc that is susceptible to # https://gcc.gnu.org/bugzilla/show_bug.cgi?id=58909, so we must apply a @@ -82,6 +84,8 @@ build_boolector() { build_cvc4() { pushd repos/CVC4-archived patch -p1 -i $PATCHES/cvc4-antlr-check-aarch64.patch + # Add missing #include statements that macos-14's version of Clang++ requires. + patch -p1 -i $PATCHES/cvc4-fix-missing-includes.patch ./contrib/get-antlr-3.4 ./contrib/get-symfpu if $IS_WIN ; then diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 372d712..937f9e9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,10 +16,10 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-22.04, ubuntu-20.04, macos-12, macos-14, windows-2019] + os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019] solver: [abc, bitwuzla, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14] steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 with: submodules: true fetch-depth: 0 @@ -65,7 +65,7 @@ jobs: if: runner.os == 'Windows' - name: Install Python - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: '3.10' @@ -94,7 +94,7 @@ jobs: GITHUB_MATRIX_OS: ${{ matrix.os }} if: runner.os == 'Windows' - - uses: actions/upload-artifact@v2 + - uses: actions/upload-artifact@v4 with: path: bin name: ${{ matrix.os }}-${{ runner.arch }}-${{ matrix.solver }}-bin @@ -105,44 +105,44 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-22.04, ubuntu-20.04, macos-12, macos-14, windows-2019] + os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019] steps: - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-abc-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-bitwuzla-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-boolector-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-cvc4-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-cvc5-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-yices-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.8-bin" path: bin - - uses: actions/download-artifact@v2 + - uses: actions/download-artifact@v4 with: name: "${{ matrix.os }}-${{ runner.arch }}-z3-4.8.14-bin" path: bin @@ -155,7 +155,7 @@ jobs: shell: bash run: cp bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3 - - uses: actions/upload-artifact@v2 + - uses: actions/upload-artifact@v4 with: path: bin name: ${{ matrix.os }}-${{ runner.arch }}-bin diff --git a/README.md b/README.md index 6578f92..e2a59fc 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ Currently, `what4-solvers` offers the following solver versions: Built for the following operating systems: -* macOS Monterey 12 (x86-64) +* macOS Ventura 13 (x86-64) * macOS Sonoma 14 (arm64) * Ubuntu 20.04 (x86-64) * Ubuntu 22.04 (x86-64) diff --git a/patches/bitwuzla-fix-missing-includes-gcc14.patch b/patches/bitwuzla-fix-missing-includes-gcc14.patch new file mode 100644 index 0000000..cca6100 --- /dev/null +++ b/patches/bitwuzla-fix-missing-includes-gcc14.patch @@ -0,0 +1,61 @@ +diff --git a/src/lib/bitblast/aig/aig_cnf.cpp b/src/lib/bitblast/aig/aig_cnf.cpp +index a9a00c8e..69a19ad6 100644 +--- a/src/lib/bitblast/aig/aig_cnf.cpp ++++ b/src/lib/bitblast/aig/aig_cnf.cpp +@@ -10,6 +10,7 @@ + + #include "bitblast/aig/aig_cnf.h" + ++#include + #include + + namespace bzla::bb { +diff --git a/src/lib/bitblast/aig/aig_manager.cpp b/src/lib/bitblast/aig/aig_manager.cpp +index 878ef276..7d36b76a 100644 +--- a/src/lib/bitblast/aig/aig_manager.cpp ++++ b/src/lib/bitblast/aig/aig_manager.cpp +@@ -10,6 +10,8 @@ + + #include "bitblast/aig/aig_manager.h" + ++#include ++ + namespace bzla::bb { + + bool +diff --git a/src/main/options.cpp b/src/main/options.cpp +index 0d1e518a..5f3fb97c 100644 +--- a/src/main/options.cpp ++++ b/src/main/options.cpp +@@ -2,6 +2,7 @@ + + #include + ++#include + #include + #include + #include +diff --git a/src/parser/smt2/parser.cpp b/src/parser/smt2/parser.cpp +index 3bd26ffc..164a48be 100644 +--- a/src/parser/smt2/parser.cpp ++++ b/src/parser/smt2/parser.cpp +@@ -10,6 +10,7 @@ + + #include "parser/smt2/parser.h" + ++#include + #include + + namespace bzla { +diff --git a/test/unit/api/test_api.cpp b/test/unit/api/test_api.cpp +index c80bb32d..da7c743d 100644 +--- a/test/unit/api/test_api.cpp ++++ b/test/unit/api/test_api.cpp +@@ -11,6 +11,7 @@ + #include + #include + ++#include + #include + #include + diff --git a/patches/cvc4-fix-missing-includes.patch b/patches/cvc4-fix-missing-includes.patch new file mode 100644 index 0000000..5101b8f --- /dev/null +++ b/patches/cvc4-fix-missing-includes.patch @@ -0,0 +1,36 @@ +diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h +index 55e07747e..250185809 100644 +--- a/src/expr/emptyset.h ++++ b/src/expr/emptyset.h +@@ -19,6 +19,7 @@ + + #pragma once + ++#include + #include + + namespace CVC4 { +diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h +index f8464392a..985a3ca2a 100644 +--- a/src/expr/expr_iomanip.h ++++ b/src/expr/expr_iomanip.h +@@ -19,6 +19,7 @@ + #ifndef CVC4__EXPR__EXPR_IOMANIP_H + #define CVC4__EXPR__EXPR_IOMANIP_H + ++#include + #include + + namespace CVC4 { +diff --git a/src/util/regexp.h b/src/util/regexp.h +index 180bb0c32..25c5c9ad2 100644 +--- a/src/util/regexp.h ++++ b/src/util/regexp.h +@@ -17,6 +17,7 @@ + #ifndef CVC4__UTIL__REGEXP_H + #define CVC4__UTIL__REGEXP_H + ++#include + #include + #include +