CI: Use more recent version of Z3

Z3's Constrained Horn Clause (CHC) solving is buggy on Z3-4.8.8 and will return incorrect answers, which affects the AES-GCM proof. This patch upgrades to a newer version of Z3 which is not affected by the bug.
RyanGlScott · Apr 23, 2024 · 2d7002d · 2d7002d
1 parent 3cdc32f
commit 2d7002d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SAW/scripts/aarch64/docker_install.sh b/SAW/scripts/aarch64/docker_install.sh
@@ -5,7 +5,7 @@
 
 set -ex
 
-Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip'
+Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.14/z3-4.8.14-x64-glibc-2.31.zip'
 YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz'
 
 mkdir -p /bin /deps

diff --git a/SAW/scripts/x86_64/docker_install.sh b/SAW/scripts/x86_64/docker_install.sh
@@ -5,7 +5,7 @@
 
 set -ex
 
-Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip'
+Z3_URL='https://github.com/Z3Prover/z3/releases/download/z3-4.8.14/z3-4.8.14-x64-glibc-2.31.zip'
 YICES_URL='https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz'
 
 mkdir -p /bin /deps