Build both Z3 4.8.10 and 4.8.14 versions

We now include both Z3 4.8.10 and 4.8.14 so that SAW's CI can revert back to
4.8.10 in certain cases, as 4.8.14 has been known to nondeterministically fail
on certain jobs. See GaloisInc/saw-script#1772.

.github/ci.sh

@@ -169,15 +169,24 @@ build_yices() {
   cleanup_bins
 }
 
+build_z3-4.8.10() {
+  build_z3 "4.8.10"
+}
+
+build_z3-4.8.14() {
+  build_z3 "4.8.14"
+}
+
 build_z3() {
-  pushd repos/z3
+  Z3_BIN="z3-$1"
+  pushd repos/$Z3_BIN
   if $IS_WIN ; then
     sed -i.bak -e 's/STATIC_BIN=False/STATIC_BIN=True/' scripts/mk_util.py
   fi
   python scripts/mk_make.py
-  (cd build && make -j4 && cp z3$EXT $BIN)
+  (cd build && make -j4 && cp z3$EXT $BIN/$Z3_BIN$EXT)
   popd
-  (cd $BIN && ./z3$EXT --version && deps z3$EXT && ./z3$EXT $PROBLEM)
+  (cd $BIN && ./$Z3_BIN$EXT --version && deps $Z3_BIN$EXT && ./$Z3_BIN$EXT $PROBLEM)
   cleanup_bins
 }
 

.github/workflows/ci.yml

@@ -8,6 +8,7 @@ on:
 
 env:
   CACHE_VERSION: 1
+  LATEST_Z3_VERSION: "4.8.14"
 
 jobs:
   build:
@@ -16,7 +17,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019]
-        solver: [abc, boolector, cvc4, cvc5, yices, z3]
+        solver: [abc, boolector, cvc4, cvc5, yices, z3-4.8.10, z3-4.8.14]
     steps:
       - uses: actions/checkout@v2
         with:
@@ -126,6 +127,18 @@ jobs:
           name: "${{ matrix.os }}-z3-bin"
           path: bin
 
+        # Make z3 a symlink for z3-<LATEST_Z3_VERSION>.
+      - name: Alias latest Z3 version (non-Windows)
+        shell: bash
+        run: ln -s bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3
+        if: runner.os != 'Windows'
+
+        # Windows doesn't support symlinks, so just copy the binary on Windows.
+      - name: Alias latest Z3 version (Windows)
+        shell: msys2 {0}
+        run: cp bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3
+        if: runner.os == 'Windows'
+
       - uses: actions/upload-artifact@v2
         with:
           path: bin

.gitmodules

@@ -16,8 +16,11 @@
 [submodule "repos/yices2"]
 	path = repos/yices2
 	url = https://github.com/SRI-CSL/yices2
-[submodule "repos/z3"]
-	path = repos/z3
+[submodule "repos/z3-4.8.10"]
+	path = repos/z3-4.8.10
+	url = https://github.com/Z3Prover/z3
+[submodule "repos/z3-4.8.14"]
+	path = repos/z3-4.8.14
 	url = https://github.com/Z3Prover/z3
 [submodule "repos/cvc5"]
 	path = repos/cvc5

README.md

@@ -1,2 +1,50 @@
 # what4-solvers
-Multi-platform binary creation for solvers of the versions most suitable for use with What4
+
+Multi-platform binary creation for solvers of the versions most suitable for use
+with [What4](https://github.com/GaloisInc/what4), as well as tools built on top
+of What4, such as [Cryptol](https://cryptol.net/),
+[Crux](https://crux.galois.com/), and [SAW](https://saw.galois.com/).
+
+Binary distributions can be found at the
+[releases page](https://github.com/GaloisInc/what4-solvers/releases).
+Currently, `what4-solvers` offers the following solver versions:
+
+* ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674)
+* Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3)
+* CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379)
+* CVC5 - [1.0.2](https://github.com/cvc5/cvc5/tree/ef35c1131976e5a3d981dace510d90aed2d11cef)
+* Yices - [2.6.2](https://github.com/SRI-CSL/yices2/tree/8509cfb5c294df3c0ac3a4814483f39c58879606)
+* Z3 - [4.8.10](https://github.com/Z3Prover/z3/tree/517d907567f4283ad8b48ff9c2a3f6dce838569e) and
+       [4.8.14](https://github.com/Z3Prover/z3/tree/df8f9d7dcb8b9f9b3de1072017b7c2b7f63f0af8)
+
+Built for the following operating systems:
+
+* macOS Monterey 12
+* Ubuntu 20.04
+* Ubuntu 22.04
+* Windows Server 2019
+
+## FAQ
+
+### Why build for multiple 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).
+
+### Why offer multiple Z3 versions?
+
+We use Z3 as the default SMT solver in many different projects' CI, including
+the CI for Cryptol and SAW. Unfortunately, certain Z3 versions have been known
+to non-deterministically fail or time out on certain SMT queries. See, for
+example, [this Cryptol issue](https://github.com/GaloisInc/cryptol/issues/1107)
+regarding Z3 4.8.10 and
+[this SAW issue](https://github.com/GaloisInc/saw-script/issues/1772) regarding
+Z3 4.8.14. As a consequence, it is very difficult to find a single Z3 version
+that works reliably across all of our tools' CI.
+
+As a compromise, we offer multiple Z3 versions so that tools can pick one that
+is known to work well for their particular needs. If we successfully identify a
+later version of Z3 that is known to work reliably across all CI
+configurations, we may reconsider this choice.