CI: Build ubuntu-24.04-arm binaries

.github/ci.sh

@@ -44,15 +44,6 @@ 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
-    # crude workaround for it. Thankfully, this is not required for the version
-    # of glibc that ships with Ubuntu 22.04.
-    patch -p1 -i $PATCHES/bitwuzla-T58909-workaround.patch
-  fi
   ./configure.py
   cd build
   ninja -j4
@@ -89,6 +80,14 @@ build_cvc4() {
   patch -p1 -i $PATCHES/cvc4-antlr-pointer-to-integer-cast.patch
   # Add missing #include statements that macos-14's version of Clang++ requires.
   patch -p1 -i $PATCHES/cvc4-fix-missing-includes.patch
+  # Backport a fix for https://github.com/cvc5/cvc5/issues/10591, which causes
+  # bash-5.2 to spuriously replace uses of ampersands (&) in text replacement.
+  # This patch was accumulated from the following CVC5 pull requests:
+  #
+  # * https://github.com/cvc5/cvc5/pull/9233
+  # * https://github.com/cvc5/cvc5/pull/9330
+  # * https://github.com/cvc5/cvc5/pull/9338
+  patch -p1 -i $PATCHES/cvc4-fix-spurious-bash-replacements.patch
   ./contrib/get-antlr-3.4
   ./contrib/get-symfpu
   if $IS_WIN ; then

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019]
+        os: [ubuntu-24.04, ubuntu-24.04-arm, ubuntu-22.04, macos-13, macos-14, windows-2019]
         solver: [abc, bitwuzla, boolector, cvc4, cvc5, yices, z3-4.8.8, z3-4.8.14]
     steps:
       # This is necessary to clone the yices2 repo on Windows, as some of the
@@ -35,7 +35,7 @@ jobs:
       - name: Install dependencies (Ubuntu)
         run: |
           sudo apt-get update
-          sudo apt-get install gperf automake autoconf lzip ninja-build
+          sudo apt-get install gperf automake autoconf libreadline-dev lzip ninja-build
         if: runner.os == 'Linux'
 
       - name: Install dependencies (macOS)
@@ -113,7 +113,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-22.04, ubuntu-20.04, macos-13, macos-14, windows-2019]
+        os: [ubuntu-24.04, ubuntu-24.04-arm, ubuntu-22.04, macos-13, macos-14, windows-2019]
     steps:
       - uses: actions/download-artifact@v4
         with:
@@ -175,7 +175,7 @@ jobs:
   # - changes to jobs or job instances don't require a mergify config update
   # - dependencies through `needs:` are validated, CI will fail if it's invalid
   mergify:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-24.04
     needs: [build]
     steps:
       - run: "true"

README.md

@@ -10,7 +10,7 @@ Binary distributions can be found at the
 Currently, `what4-solvers` offers the following solver versions:
 
 * ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674)
-* Bitwuzla - [0.3.0](https://github.com/bitwuzla/bitwuzla/tree/2b5a4a867f3717ba1adc325adf8e69577e3cee5c)
+* Bitwuzla - [0.7.0](https://github.com/bitwuzla/bitwuzla/tree/3cf7c35b97c60016883cc19c4d6a9344a989a4d6)
 * Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3)
 * CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379)
 * CVC5 - [1.1.1](https://github.com/cvc5/cvc5/tree/ebfdf84d5698eeb83e0fa4e45101fe4a8f4543eb)
@@ -22,20 +22,25 @@ Built for the following operating systems:
 
 * macOS Ventura 13 (x86-64)
 * macOS Sonoma 14 (arm64)
-* Ubuntu 20.04 (x86-64)
 * Ubuntu 22.04 (x86-64)
+* Ubuntu 24.04 (x86-64)
+* Ubuntu 24.04 (arm64)
 * Windows Server 2019 (x86-64)
 
 All of the binary distributions are built from CI.
 
 ## FAQ
 
-### Why build for multiple Ubuntu versions?
+### Why build for multiple x86-64 Ubuntu versions?
 
-We attempt to offer somewhat broad coverage of different Linux versions. To
-that end, we build each solver on the two most recent Ubuntu LTS releases. This
-ensures relatively complete coverage of different shared library dependencies
-(e.g., different `glibc` versions).
+We attempt to offer somewhat broad coverage of different x86-64 Linux versions.
+To that end, we build each solver on the two most recent x86-64 Ubuntu LTS
+releases. This ensures relatively complete coverage of different shared library
+dependencies (e.g., different `glibc` versions).
+
+In contrast, we currently only build each solver on the latest arm64 Ubuntu LTS
+release. Please file an issue is this support window is too narrow for your
+needs.
 
 ### Why offer multiple Z3 versions?
 

patches/cvc4-fix-spurious-bash-replacements.patch

@@ -0,0 +1,42 @@
+diff --git a/src/expr/mkexpr b/src/expr/mkexpr
+index c5f12f487..b47c66753 100755
+--- a/src/expr/mkexpr
++++ b/src/expr/mkexpr
+@@ -14,6 +14,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+
+diff --git a/src/expr/mkkind b/src/expr/mkkind
+index fbf37eff4..aabc70afe 100755
+--- a/src/expr/mkkind
++++ b/src/expr/mkkind
+@@ -13,6 +13,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+
+diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
+index e2a733ec8..e56d076d7 100755
+--- a/src/expr/mkmetakind
++++ b/src/expr/mkmetakind
+@@ -16,6 +16,9 @@
+ #
+ # Output is to standard out.
+ #
++# Required to disable this option for bash >=5.2 to avoid automatically
++# replacing & by the substituted text.
++shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
+
+ copyright=2010-2014
+

patches/cvc4-win64-native.patch

@@ -38,45 +38,3 @@ index 21a444082..8b30c8b14 100755
  [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
  [ $muzzle != default ] \
    && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-diff --git a/src/expr/mkexpr b/src/expr/mkexpr
-index c5f12f487..b47c66753 100755
---- a/src/expr/mkexpr
-+++ b/src/expr/mkexpr
-@@ -14,6 +14,9 @@
- #
- # Output is to standard out.
- #
-+# Required to disable this option for bash >=5.2 to avoid automatically
-+# replacing & by the substituted text.
-+shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
-
- copyright=2010-2014
-
-diff --git a/src/expr/mkkind b/src/expr/mkkind
-index fbf37eff4..aabc70afe 100755
---- a/src/expr/mkkind
-+++ b/src/expr/mkkind
-@@ -13,6 +13,9 @@
- #
- # Output is to standard out.
- #
-+# Required to disable this option for bash >=5.2 to avoid automatically
-+# replacing & by the substituted text.
-+shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
-
- copyright=2010-2014
-
-diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
-index e2a733ec8..e56d076d7 100755
---- a/src/expr/mkmetakind
-+++ b/src/expr/mkmetakind
-@@ -16,6 +16,9 @@
- #
- # Output is to standard out.
- #
-+# Required to disable this option for bash >=5.2 to avoid automatically
-+# replacing & by the substituted text.
-+shopt | grep -q '^patsub_replacement\b' &&  shopt -u patsub_replacement
-
- copyright=2010-2014
-