From 52f7e232dd786a62a4d834b79528ee115cfbf45b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 12 Apr 2024 08:52:42 +0200
Subject: [PATCH] [wp/doc] update prover fallback documentation

---
 src/plugins/wp/doc/manual/wp_plugin.tex | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 173961c6dc0..75d6ddea26e 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1450,8 +1450,11 @@ Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use
 Finally, since \textsf{Why-3} also provides the alias
 \verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.
 
-If you require a specific version of a prover which is not installed,
-\textsf{WP} will fallback to the default version available to \textsf{Why-3} for this prover, if any.
+If you require on command line a specific version of a prover which is not
+installed, \textsf{WP} will emit an error. When a script contains a couple
+prover/version that is not installed, \textsf{WP} will try to find another
+version of the same prover and fallback on this solver (emitting a warning) if
+it finds one. In this case, one should update the scripts.
 
 Notice that \textsf{Why-3} provers benefit from a cache management when used in combination
 with a \textsf{WP}-session, see Section~\ref{wp-cache} for more details.
-- 
GitLab