diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index 0671104df075c2dd60049795472441e5e0776620..cb6a92931a6f11881d2ebff24922c092a30b9a95 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -2,6 +2,7 @@
   C-compound-statement ::= "{" declaration* statement* assertion+ "}"
         \
   C-statement ::= assertion statement \
-  assertion ::= "/*@" "assert" pred ";" "*/" ;
-  | { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
+  assertion-kind ::= "assert" | "check" \
+  assertion ::= "/*@" assertion-kind pred ";" "*/" ;
+  | { "/*@" "for" id ("," id)* ":" assertion-kind pred ";" "*/" } ;
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index b482e45965e933015939a0b2f318fa8ac4b1e1af..b610ebad7eac345d7633c19e90931f94282837bf 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,14 @@
 
 \subsection*{Version \version}
 \begin{itemize}
+\item Update according to \acsl 1.14:
+  \begin{itemize}
+  \item \changeinsection{assertions}{add the keyword \texttt{check}}
+  \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.13}
+\begin{itemize}
 \item Update according to \acsl 1.13:
   \begin{itemize}
   \item \changeinsection{locations}{add syntax for set membership}
@@ -117,6 +125,11 @@ in \lstinline|\\at|}
 \section{Changes in \eacsl Implementation}
 
 \subsection*{Version \eacslversion}
+\begin{itemize}
+\item \changeinsection{logicspec}{support of logic functions and predicates}
+\end{itemize}
+
+\subsection*{Version Argon-18}
 
 \begin{itemize}
 \item \changeinsection{at}{support of \lstinline|\\at| on purely
diff --git a/src/plugins/e-acsl/doc/refman/logic.tex b/src/plugins/e-acsl/doc/refman/logic.tex
index 6dd160eada7218be33c171109ae76dea571e45ea..53b4a3aacc2270e356c6c57ebba15f2d170c648b 100644
--- a/src/plugins/e-acsl/doc/refman/logic.tex
+++ b/src/plugins/e-acsl/doc/refman/logic.tex
@@ -1,19 +1,19 @@
 \begin{syntax}
-  C-global-decl ::= { "/*@" logic-def+ "*/" }
+  C-global-decl ::= "/*@" logic-def+ "*/"
   \
-  [ { logic-def } ] ::= { logic-const-def } ;
-          | { logic-function-def } ;
-          | { logic-predicate-def } ;
+  logic-def ::= { logic-const-def } ;
+          | logic-function-def ;
+          | logic-predicate-def ;
   \
-  [ { type-expr } ] ::= { id };
+  type-expr ::= id;
   \
-  [ { logic-const-def } ] ::= { "logic" type-expr id "=" term ";" }
+  { logic-const-def } ::= { "logic" type-expr id "=" term ";" }
   \
-  [ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
+  logic-function-def ::= "logic" type-expr id parameters "=" term ";"
   \
-  [ { logic-predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
+  logic-predicate-def ::= "predicate" id parameters? "=" pred ";"
   \
-  { parameters } ::= { "(" parameter (, parameter)* ")" }
+  parameters ::= "(" parameter (, parameter)* ")"
   \
-  { parameter } ::= { type-expr id }
+  parameter ::= type-expr id
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index e5704ebffeed9b32e2583f4df27ddfa69066f672..88c2665b3138eb4593be41a543f86a070172ef12 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{\acslversion}{1.13\xspace}
+\newcommand{\acslversion}{1.14\xspace}
 \newcommand{\version}{\acslversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 3adb89eb13dd0ba7731bb2be8fd24caf64fc863e..baafd9b8bb8a943adcc50e0727d7de9063bdb3a0 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -612,7 +612,7 @@ axiomatics.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Predicate and function definitions}}
+\subsection{Predicate and function definitions}
 \nodiff
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -642,7 +642,7 @@ axiomatics.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{\notimplemented{Recursive logic definitions}}
+\subsection{Recursive logic definitions}
 \index{recursion}
 \nodiff