diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 74f06206e0516484554cd4fafa16ffb76988a0fe..44868a143cbab14096a30bce28994cacadf9aa44 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -34,8 +34,8 @@ Plugin WP <next-release>
 - WP          [2020-09-21] Added support for Why3 Coq interactive prover
 - WP          [2020-09-21] New option -wp-interactive <mode>
 - WP          [2020-09-21] New option -wp-interactive-timeout <seconds>
-- WP          [2020-09-17] New experimental option: -wp-check-model-hypotheses
-                           Generates requires in contracts for model hypotheses
+- WP          [2020-09-17] New experimental option: -wp-check-memory-model
+                           Insert function contracts for model hypotheses
 - WP          [2020-09-17] Hypotheses: assigned memory locations
 - WP          [2020-09-11] Support for generalized @check ACSL annotations
 - WP          [2020-07-06] Removed debug keys "no-xxx-info" (subsumed by "shell")
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 9223f9d67dfc742606487b15eeb708de80f8c8d7..6e7afa77c066bb52273da98252d093d08b6980f3 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -34,5 +34,5 @@ the user \emph{must} check by manual code review that no aliases are
 introduced \emph{via} pointers passed to formal parameters at call sites.
 
 However, \textsf{WP} warns about the implicit separation hypotheses required by
-the memory model \textit{via} the \texttt{-wp-warn-separation} option, set
+the memory model \textit{via} the \texttt{-wp-warn-memory-model} option, set
 by default.
diff --git a/src/plugins/wp/doc/manual/wp_logic.tex b/src/plugins/wp/doc/manual/wp_logic.tex
index fb06118205256554f6819989501e20158840cbff..b51bb2e77899aa61c06c94bb48c1b7540c01467b 100644
--- a/src/plugins/wp/doc/manual/wp_logic.tex
+++ b/src/plugins/wp/doc/manual/wp_logic.tex
@@ -178,3 +178,48 @@ detected variables are then assigned to the Hoare memory model.
 
 This optimization is not activated by default, since the non-aliasing
 assumptions at call sites are sometimes irrelevant.
+
+\section{Mixed models hypotheses}
+
+For the previously presented \textsf{Ref} model, but also for the
+\textsf{Typed}, and \textsf{Caveat} models presented later, WP lists
+the separation and validity hypotheses associated to the choice that
+it make of dispatching each pointer and variable either to the
+\lstinline{Hoare} or to the model $\cal{M}$ used for the heap.
+
+Thus, in addition to user-defined function \lstinline{requires}, WP
+also states as \lstinline{requires} that:
+
+\begin{itemize}
+\item \lstinline{Hoare} variables are separated from each other,
+\item \lstinline{Hoare} variables are separated from the locations in $\cal{M}$,
+\item references are valid memory locations,
+\item locations assigned via a pointer are separated from \lstinline{Hoare}
+  variables whose address is not taken by the function (including via
+  its contract).
+\end{itemize}
+
+Furthermore, the function must ensure that:
+
+\begin{itemize}
+\item locations assigned via a pointer (including returned value when
+  it is a pointer) are separated from \lstinline{Hoare} variables whose address
+  is not taken by the function (including via its contract),
+\item pointers assigned by the function (including returned value when
+  it is a pointer) are separated from function parameters and \lstinline{Hoare}
+  variables whose address is not taken by the function (including via
+  its contract).
+\end{itemize}
+
+In order to precisely generate these hypotheses, WP needs precise
+\lstinline{assigns} specification. In particular each function under
+verification and all its callees needs an \lstinline{assigns} specification.
+Furthermore, if the function assigns or returns a pointer, WP needs
+a correct \lstinline{\from} specification. If the specification is
+incomplete, a warning \lstinline{wp:pedantic-assigns} is triggered.
+Note that WP does not verify that the \lstinline{\from} is correct.
+
+The hypotheses are displayed when the option
+\lstinline{-wp-warn-memory-model} is enable (it is enabled by default).
+They can be verified by WP using the experimental option
+\lstinline{-wp-check-memory-model}.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index baabcb0c126a097e691c2abfbb2b0f1457321b4e..8398488c91938420fc5a5799b8970270c5355087 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -827,6 +827,9 @@ The available \textsf{WP} command-line options related to model selection are:
   an \textsf{ACSL} specification is printed on output.
   Currently, only the \texttt{Caveat}, \texttt{Typed} and \texttt{Ref} memory models support
   this feature.
+\item[\tt -wp-(no)-check-memory-model] this \emph{experimental} option generates
+  the hypotheses listed by the option \texttt{-wp-warn-memory-model} as ACSL contracts and
+  asks WP to verify them. Disabled by default.
 \end{description}
 
 \subsection{Computation Strategy}