Build x86-64 macOS solvers on macos-13

.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

.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

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)

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 <cstdlib>
+ #include <functional>
+
+ 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 <cstdlib>
++
+ 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 <bitwuzla/cpp/bitwuzla.h>
+
++#include <algorithm>
+ #include <cassert>
+ #include <iomanip>
+ #include <iostream>
+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 <algorithm>
+ #include <iostream>
+
+ 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 <bitwuzla/cpp/bitwuzla.h>
+ #include <bitwuzla/cpp/parser.h>
+
++#include <algorithm>
+ #include <chrono>
+ #include <fstream>
+

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 <cstddef>
+ #include <iosfwd>
+
+ 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 <cstddef>
+ #include <iosfwd>
+
+ 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 <cstddef>
+ #include <cstdint>
+ #include <iosfwd>
+