diff --git a/.github/ci.sh b/.github/ci.sh
index dbfc529..b565c98 100755
--- a/.github/ci.sh
+++ b/.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
 }
 
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b274e40..c7567d4 100644
--- a/.github/workflows/ci.yml
+++ b/.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:
@@ -95,6 +96,12 @@ jobs:
       matrix:
         os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019]
     steps:
+      - name: Setup MSYS2 (Windows)
+        uses: msys2/setup-msys2@v2
+        with:
+          update: true
+          msystem: MINGW64
+        if: runner.os == 'Windows'
 
       - uses: actions/download-artifact@v2
         with:
@@ -123,9 +130,26 @@ jobs:
 
       - uses: actions/download-artifact@v2
         with:
-          name: "${{ matrix.os }}-z3-bin"
+          name: "${{ matrix.os }}-z3-4.8.10-bin"
           path: bin
 
+      - uses: actions/download-artifact@v2
+        with:
+          name: "${{ matrix.os }}-z3-4.8.14-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
diff --git a/.gitmodules b/.gitmodules
index d9db92d..ddcefb7 100644
--- a/.gitmodules
+++ b/.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
diff --git a/README.md b/README.md
index f643452..59d6937 100644
--- a/README.md
+++ b/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.
diff --git a/repos/z3-4.8.10 b/repos/z3-4.8.10
new file mode 160000
index 0000000..517d907
--- /dev/null
+++ b/repos/z3-4.8.10
@@ -0,0 +1 @@
+Subproject commit 517d907567f4283ad8b48ff9c2a3f6dce838569e
diff --git a/repos/z3 b/repos/z3-4.8.14
similarity index 100%
rename from repos/z3
rename to repos/z3-4.8.14