From 5f27329490c68b0b40903b05c6eac427b4323392 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Tue, 10 Nov 2026 09:57:05 +0000
Subject: [PATCH] [docker] bump z3 minor and alt-ergo patch

z3 5.4.1
alt-ergo 2.6.4 -> 2.6.5

evict alt-ergo 2.6.4
---
 scripts/docker/Dockerfile | 11 +++++++++--
 src/ecProvers.ml          |  6 ++++++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile
index 62ec85658..f86dc6bb6 100644
--- a/scripts/docker/Dockerfile
+++ b/scripts/docker/Dockerfile
@@ -31,7 +31,7 @@ WORKDIR /home/$user
 
 ENV OPAMYES=true OPAMVERBOSE=0 OPAMJOBS=4
 
-ARG OCAML_VERSION=5.4.0
+ARG OCAML_VERSION=5.4.1
 
 RUN \
 	opam init --disable-sandboxing --compiler=ocaml-base-compiler.${OCAML_VERSION}
@@ -53,7 +53,7 @@ ENV PATH="/home/charlie/bin:$PATH"
 FROM ${BASE_BUILD_LAYER} AS build
 
 RUN \
-	version=2.6.4 && \
+	version=2.6.5 && \
   wget -O alt-ergo https://github.com/OCamlPro/alt-ergo/releases/download/v${version}/alt-ergo-v${version}-x86_64-linux-musl && \
   sudo install -m 0755 alt-ergo /usr/local/bin/alt-ergo-${version} && \
   rm -f alt-ergo
@@ -104,6 +104,13 @@ RUN \
 	sudo install -m 0755 cvc5 /usr/local/bin/cvc5-${version} && \
 	rm -f cvc5
 
+RUN \
+	version=5.4.0 && glibc=2.39 && \
+	wget -O z3.zip https://github.com/Z3Prover/z3/releases/download/z3-${version}/z3-${version}-x64-glibc-${glibc}.zip && \
+	unzip -j z3.zip z3-${version}-x64-glibc-${glibc}/bin/z3 && \
+	sudo install -m 0755 z3 /usr/local/bin/z3-${version} && \
+	rm -f z3 z3.zip
+
 RUN \
 	version=5.3.3 && glibc=2.39 && \
 	wget -O z3.zip https://github.com/Z3Prover/z3/releases/download/z3-${version}/z3-${version}-x64-glibc-${glibc}.zip && \
diff --git a/src/ecProvers.ml b/src/ecProvers.ml
index 41dd1b7e2..b31b976c5 100644
--- a/src/ecProvers.ml
+++ b/src/ecProvers.ml
@@ -103,10 +103,16 @@ module Evictions = struct
     pe_cause = `Inconsistent;
     pe_test  = `ByVersion ("Alt-Ergo", (`Le, VP.of_tuple (2, 3, 0)));
   }
+
+  let alt_ergo_2_6_4 = {
+    pe_cause = `Inconsistent;
+    pe_test  = `ByVersion ("Alt-Ergo", (`Eq, VP.of_tuple (2, 6, 4)));
+  }
 end
 
 let evictions : prover_eviction_test list = [
   Evictions.alt_ergo_le_0_99_1;
+  Evictions.alt_ergo_2_6_4;
 ]
 
 (* -------------------------------------------------------------------- *)