diff --git a/opam b/opam
index 4be72acca11ea644bba0ee3c17f04133422cf46f..ea9769f87fc2d9ba5227dbbc358cffa1930efc43 100644
--- a/opam
+++ b/opam
@@ -132,7 +132,7 @@ depends: [
   "ocamlgraph" { with-test & >= "2.1.0" }
   "odoc" { with-doc }
   "unionFind" { >= "20220107" }
-  "why3" { >= "1.6.0" & < "1.7.0" }
+  "why3" { >= "1.6.0" & ( < "1.7.0" | !with-test ) }
   "yaml" { >= "3.0.0" }
   "yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)}
   "zarith" { >= "1.5" }
diff --git a/src/plugins/alias/README.md b/src/plugins/alias/README.md
index 2af708989b3b8d1df8f2eee3b61ddb4a0f7e73e9..8bf5f633dca549786a11c93c42913da563bf58f6 100644
--- a/src/plugins/alias/README.md
+++ b/src/plugins/alias/README.md
@@ -16,6 +16,8 @@ The plugin implements a variant of « Steensgaard's algorithm ».
 Note that the Eva plugin also implements a points-to analysis, which is much
 more precise but also much less efficient than this plugin.
 
+This plugin is currently at an experimental stage.
+
 ## Usage
 
 To run the may-alias analysis either:
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index a44b0e55677d65978a2285ef9087128ea08ed910..67f698182412223e3aa480d0380c5b2c81f368f1 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,11 @@
 
 % Next version
 \subsection*{Version \version}
+\begin{itemize}
+  \item No changes: changes in \acsl 1.20 do not impact \eacsl.
+\end{itemize}
+
+\subsection*{Version 1.19}
 \begin{itemize}
   \item Update according to \acsl 1.19
     \begin{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index ac7c25222d034de00b21620cb21e6279c2bb7c7e..c927ccde843f89b6c12efcde5f0045979fa252a2 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -24,7 +24,7 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\eacsllangversion}{1.19\xspace}
+\newcommand{\eacsllangversion}{1.20\xspace}
 \newcommand{\version}{\eacsllangversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 88c13081e12f211e6d0add8ebd1a0d0b1bd3a460..c16ff02fa861910b652cb905e9b218f2da7d25c9 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -28,6 +28,7 @@ Plugin WP <next-release>
 Plugin WP 28.0 (Nickel)
 ###############################################################################
 
+- WP          [2023-11-24] Ensure compatibility with Why3 1.7.0
 - WP          [2023-10-19] WP generates exits and terminates specification
                            on all functions, using the mechanism provided by
                            the Frama-C kernel