diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 405600b3263fe6ba89283519d2f9b81372e9c413..844b5b50097f8f55d30a604eb2ec14cd13cf1498 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
 #   <Prover>: prover
 ###############################################################################
 
+-  Wp         [2019/01/28] New floating-point model
+
 ######################
 Plugin WP 18.0 (Argon)
 ######################
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index da74357a7b980d3af92104006171c1c51d367aa9..1e3c5e076a67cc3e3d8a823eceda35a8c64bcd7d 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -340,12 +340,15 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
   or \texttt{-wp-rte} will generate a warning if some annotation might be not
   generated.
 
-\item[Float Model:] floating-point operations are \emph{defined} to be
-  the mathematical ones \emph{with} a rounding operation. This is fully
-  consistent with the \textsf{IEEE} semantics. Most automated provers
-  are not able to discharge the generated proof obligations. Special
-  support for the \textsf{Gappa} theorem prover is available through
-  \textsf{Why3}.
+\item[Float Model:] floating-point values are represent in a special
+  theory with dedicated operations over \texttt{float} and \texttt{double}
+  values and conversion from and to their \texttt{real} representation \emph{via}
+  rounding, as defined by the \textsc{C/ACSL} semantics.
+
+  Although correct with respect to the \textsc{IEEE} specifications, this
+  model still provides very little support for proving properties with automated
+  provers. You may add additional properties using \emph{drivers}
+  as explained later.
 
 \item[Real Model:] floating-point operations are \emph{transformed} on
   reals, with \emph{no} rounding. This is completely unsound with