diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 076eace285b9bf83dc7e85b28d57d76dbec1bf8b..78c3791c9d46018488b903a2f32fbcbd97332c00 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-Chlorine-20180501-beta
+Chlorine-20180501+dev
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3f9ccc57028564cad8ea4cba24eb817a87d2f129..3a70cdfe5a9d5994c6106887b1ed4a8f3109199b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,7 +19,8 @@
 #   configure	configure
 ###############################################################################
 
--  E-ACSL       [2018/18/09] Support for ranges in a few builtins.
+-  E-ACSL       [2018/18/09] Support for ranges in memory builtins
+	        (\valid, \initialized, etc).
 
 ###############################
 Plugin E-ACSL Chlorine-20180501
diff --git a/src/plugins/e-acsl/doc/refman/.gitignore b/src/plugins/e-acsl/doc/refman/.gitignore
index b7b857f4e7925cce8eecab9571078c72bb404444..2c2b06ea7119f0233f24735f396c4f9bf3f4bd1c 100644
--- a/src/plugins/e-acsl/doc/refman/.gitignore
+++ b/src/plugins/e-acsl/doc/refman/.gitignore
@@ -1,2 +1,3 @@
 e-acsl.pdf
 e-acsl-implementation.pdf
+eacslversion.tex
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 8adaf7b00663fe25e6ec30db003c899f204fc781..99a5c9360d647dc13f05eebf515b6ff6fa296016 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.13:
+  \begin{itemize}
+  \item \changeinsection{locations}{add syntax for set membership}
+  \end{itemize}
+\end{itemize}
+
+\subsection*{Version 1.12}
+\begin{itemize}
 \item Update according to \acsl 1.12:
   \begin{itemize}
   \item \changeinsection{locations}{add subsections for build-in lists}
@@ -110,6 +118,13 @@ in \lstinline|\\at|}
 
 \subsection*{Version \eacslversion}
 
+\begin{itemize}
+\item \changeinsection{locations}{support of ranges in memory built-ins
+  (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
+\end{itemize}
+
+\subsection*{Version Chlorine-20180501}
+
 \begin{itemize}
 \item \changeinsection{expressions}{support of \lstinline|\\let| binding}
 \end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/loc.tex b/src/plugins/e-acsl/doc/refman/loc.tex
index f998e26dc08ca39989904fb0beae5a8ef8f9743a..37cdb3a22a20114794fe130e719b86daf86e6222 100644
--- a/src/plugins/e-acsl/doc/refman/loc.tex
+++ b/src/plugins/e-acsl/doc/refman/loc.tex
@@ -5,7 +5,7 @@
        | "*" tset ;
        | "&" tset ;
        | tset "[" tset "]" ;
-       | [ { term ".." term } ] ; range
+       | [ term ".." term ] ; range
        | { "\union" "(" tset ("," tset)* ")" } ; union of locations
        | { "\inter" "(" tset ("," tset)* ")" }; intersection
        | tset "+" tset ;
@@ -17,4 +17,5 @@
        | term ; implicit singleton
        \
   pred ::= { "\subset" "(" tset "," tset ")" } ; set inclusion
+       | { term "\in" tset } ; set membership
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 3294e626298e73ab219550810f0fd87c6963ee72..5d1fa33003cbcc7674420f0e8f2231c7e12ca625 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -21,8 +21,8 @@
   { loop-assigns } ::= { "loop" "assigns" locations ";" } ;
   \
   { loop-behavior } ::= { "for" id ("," id)* ":" } ;
-  { loop-clause* } ; annotation for behavior $id$
+  { loop-clause* } ; \hspace{-30mm} annotation for behavior $id$
   \
   { loop-variant } ::= { "loop" "variant" term ";" } ;
-  | { "loop" "variant" term "for" id ";" } ; variant for relation $id$
+  | { "loop" "variant" term "for" id ";" } ;  \hspace{-30mm} variant for relation $id$
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 8914df96cd7111492bcde2ab4da2a38c7ba7d771..fb3dabe02dc215ccbebbb9e8b97cfaefc0c207aa 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.12\xspace}
+\newcommand{\acslversion}{1.13\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 c2ee3338b80e1bb7a640c07e5bc2aa019b7579ba..2b4fa7dec498ee36d6c79fa6a84e1a43bfe71fd0 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -374,6 +374,17 @@ set of all integers between 0 and 9 and between 20 and 29.
 \end{example}
 \end{notimplementedenv}
 
+\begin{notimplementedenv}
+  Ranges are currently only supported in memory built-ins described in
+  Section~\ref{subsec:memory} and~\ref{sec:dangling}.
+
+\begin{example}
+The predicate \lstinline|\valid(&t[0 .. 9])| is supported and denotes that
+the ten first cells of the array \lstinline|t| are valid. Writing the term
+\lstinline|&t[0 .. 9]| alone, outside any memory built-in, is not yet supported.
+\end{example}
+\end{notimplementedenv}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Default contracts, multiple contracts}
@@ -665,7 +676,8 @@ predicates which are related to memory location.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Memory blocks and pointer dereferencing}
-\label{subsec:memory}\label{sec:memory}
+\label{subsec:memory}
+\label{sec:memory} % for correctness of \changeinsection in Changes
 \nodiff
 
 \difficultswhy{\lstinline|\\base\_addr|,