Fall back to Z3 4.8.8 on AWSLC/BLST proofs

This updates the `what4-solvers` snapshot to one that includes both Z3 4.8.8
and 4.8.14. While we continue to use 4.8.14 for most CI purposes, we fall back
to 4.8.8 specifically when running the AWSLC or BLST proofs, which have been
known to nondeterministically time out with those versions. Hopefully, this
should resolve our CI woes.

This avoids the main issue in #1772, although the underlying cause still has yet
to be investigated.

Author: RyanGlScott

.github/ci.sh

@@ -129,7 +129,13 @@ zip_dist_with_solvers() {
   cp "$BIN/cvc4"       dist/bin/
   cp "$BIN/yices"      dist/bin/
   cp "$BIN/yices-smt2" dist/bin/
+  # Z3 4.8.14 has been known to nondeterministically time out with the AWSLC
+  # and BLST proofs, so we include both 4.8.8 and 4.8.14 so that we can fall
+  # back to 4.8.8 (a version known to work with the AWSLC and BLST proofs)
+  # where necessary. See #1772.
   cp "$BIN/z3"         dist/bin/
+  cp "$BIN/z3-4.8.8"   dist/bin/
+  cp "$BIN/z3-4.8.14"  dist/bin/
   cp -r dist "$sname"
   tar -cvzf "$sname".tar.gz "$sname"
 }

.github/workflows/ci.yml

@@ -24,7 +24,7 @@ env:
   # ./saw-remote-api/Dockerfile
   # ./s2nTests/scripts/blst-entrypoint.sh
   # ./s2nTests/docker/saw.dockerfile
-  SOLVER_PKG_VERSION: "snapshot-20220902"
+  SOLVER_PKG_VERSION: "snapshot-20221212"
 
   OCAML_VERSION: 4.09.x
 

s2nTests/scripts/awslc-entrypoint.sh

@@ -6,6 +6,10 @@ cd /saw-script/aws-lc-verification/SAW
 rm bin/saw
 cp /saw-bin/saw bin/saw
 cp /saw-bin/abc bin/abc
+cp /saw-bin/yices bin/yices
+# Z3 4.8.14 has been known to nondeterministically time out with the BLST
+# proofs, so fall back to 4.8.8 instead. See #1772.
+cp /saw-bin/z3-4.8.8 bin/z3
 
 export PATH=/saw-script/aws-lc-verification/SAW/bin:$PATH
 export CRYPTOLPATH=/saw-script/aws-lc-verification/cryptol-specs

s2nTests/scripts/blst-entrypoint.sh

@@ -3,11 +3,13 @@ set -xe
 
 cd /workdir
 ./scripts/install.sh
+cp /saw-bin/cryptol bin/cryptol
 cp /saw-bin/saw bin/saw
-
-wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
-(cd bin && unzip -o ../solvers.zip)
-chmod +x bin/*
+cp /saw-bin/abc bin/abc
+cp /saw-bin/yices bin/yices
+# Z3 4.8.14 has been known to nondeterministically time out with the BLST
+# proofs, so fall back to 4.8.8 instead. See #1772.
+cp /saw-bin/z3-4.8.8 bin/z3
 
 export PATH=/workdir/bin:$PATH
 export CRYPTOLPATH=/workdir/cryptol-specs:/workdir/spec

saw-remote-api/Dockerfile

@@ -28,7 +28,7 @@ RUN cabal v2-update && cabal v2-build -j exe:saw-remote-api
 RUN mkdir -p /home/saw/rootfs/usr/local/bin
 RUN cp $(cabal v2-exec which saw-remote-api) /home/saw/rootfs/usr/local/bin/saw-remote-api
 WORKDIR /home/saw//rootfs/usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /home/saw/rootfs

saw/Dockerfile

@@ -29,7 +29,7 @@ RUN cabal v2-build
 RUN mkdir -p /home/saw/rootfs/usr/local/bin
 RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw
 WORKDIR /home/saw//rootfs/usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /home/saw/rootfs