diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0c48b6c985e328b88a009121a6e0431a102a7db0..e11f7bd73d436ea620c24e3de5ffc4dafda95064 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-19.0
\ No newline at end of file
+19.0+dev
diff --git a/src/plugins/e-acsl/doc/refman/binders.tex b/src/plugins/e-acsl/doc/refman/binders.tex
index 53a46c97cc32b0eda572c5d911617e9fb082d93b..023fec69d0788b02b3768d5aaf530618422d7802 100644
--- a/src/plugins/e-acsl/doc/refman/binders.tex
+++ b/src/plugins/e-acsl/doc/refman/binders.tex
@@ -9,7 +9,7 @@
   logic-type-expr ::= built-in-logic-type ;
   | id ; type identifier
   \
-  built-in-logic-type ::= "boolean" | "integer" | { "real" }
+  built-in-logic-type ::= "boolean" | "integer" | "real"
   \
   variable-ident ::= id
   | "*" variable-ident ;
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index b610ebad7eac345d7633c19e90931f94282837bf..ee30a79f7e0de4a4d9ae5f160c63fc98200dc495 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -125,6 +125,13 @@ in \lstinline|\\at|}
 \section{Changes in \eacsl Implementation}
 
 \subsection*{Version \eacslversion}
+
+\begin{itemize}
+\item \changeinsection{reals}{support of rational numbers and operations}
+\end{itemize}
+
+\subsection*{Version Potassium-19}
+
 \begin{itemize}
 \item \changeinsection{logicspec}{support of logic functions and predicates}
 \end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/libraries_modern.tex b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
index 862e5a22fe8f7cc66e9e777cf84754daf29ee711..4e828cdd1d396e51eba8b9c9a1e7d7a603a0a4d7 100644
--- a/src/plugins/e-acsl/doc/refman/libraries_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/libraries_modern.tex
@@ -1,6 +1,5 @@
 \chapter{Libraries}
 \label{chap:lib}
 
-\emph{Disclaimer:} this chapter is yet empty. It is left here to give an idea of
-what the final document will look and to be consistent with the \acsl reference
-manual~\cite{acsl}.
+\emph{Disclaimer:} this chapter is empty on purpose. It is left here to be
+consistent with the \acsl reference manual~\cite{acsl}.
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index baafd9b8bb8a943adcc50e0727d7de9063bdb3a0..c1482c0d65cbb0df19eccf95a887d310ac7a5f22 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -45,12 +45,6 @@ only difference between \eacsl and \acsl predicates are quantifications.
 \label{fig:gram:binders}
 \end{figure}
 
-\begin{notimplementedenv}
-  Reals are not correctly supported by the \eacsl plug-in right now. Only
-  floating point numbers are supported: real constants and operations are seen as
-  \C floating point constants and operations.
-\end{notimplementedenv}
-
 \subsection*{Quantification}
 \eacsl quantification must be computable. They are limited to two limited forms.
 
@@ -260,10 +254,17 @@ It is not possible to define logic types introduced by the specification writer
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Real numbers} and floating point numbers}
+\subsection{Real numbers and floating point numbers}
+\label{sec:reals}
 \nodiff
 
-\difficults{\notimplemented{Exact real numbers} and even floating point numbers}
+\difficults{Exact real numbers and even floating point numbers}
+
+\begin{notimplementedenv}
+  Real numbers beyond rationals are currently not supported by the \eacsl
+  plug-in. Only rationals (in $\mathbb{Q}$) and floating point numbers are
+  supported.
+\end{notimplementedenv}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%