From 2d7002d7dab4d2693880395258f37971332e310b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 23 Apr 2024 15:12:34 -0400 Subject: [PATCH] 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. --- SAW/scripts/aarch64/docker_install.sh | 2 +- SAW/scripts/x86_64/docker_install.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/SAW/scripts/aarch64/docker_install.sh b/SAW/scripts/aarch64/docker_install.sh index 668747eb..bb69629a 100755 --- 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 index 41328a81..b6a2018e 100755 --- 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