diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5780a467c29ee00228a8ab8d53e6b447a6a648be..4adf3772d04bbd70aff6198441d842f4e4728849 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -20,7 +20,6 @@
 ###############################################################################
 
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.
-                Fix bug #2354 about undeclared variables when using \at.
                 Fix bug #1762 about out-of-scope variables when using \old.
 *  E-ACSL       [2018/10/02] Fix bug #2305 about taking the address of a
                 bitfield.
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
new file mode 100644
index 0000000000000000000000000000000000000000..88bbc974a191e189a3fdaa7e88047b65abf6387f
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables.c
@@ -0,0 +1,12 @@
+main(void) {
+  int m = 2;
+  int n = 7;;
+  K: ;
+  n = 875;
+  /*@ assert
+      \let k = 3;
+      \exists integer u; 9 <= u < 21 &&
+      \forall integer v; -5 < v <= (u < 15 ? u + 6 : k) ==>
+        \at(n + u + v > 0, K); */ ;
+  return 0;
+}
diff --git a/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
new file mode 100644
index 0000000000000000000000000000000000000000..dff4da97bd3e5b3fa986023c89a94a7307563cd5
--- /dev/null
+++ b/src/plugins/e-acsl/doc/refman/at_on-purely-logic-variables_not-yet.c
@@ -0,0 +1,2 @@
+/*@ ensures \forall int i; 0 <= i < n-1 ==> \old(t[i]) == t[i+1]; */
+void reverse(int *t, int n) { }
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index b7213239b47d9445cfd9141e2f97724260d3b74e..3adb89eb13dd0ba7731bb2be8fd24caf64fc863e 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -523,14 +523,14 @@ The \verb|\at| construct of the following example is supported.
 
 
 \begin{notimplementedenv}
-However, quantified variables and let-binded variables that use C variables in
-their definition are not yet supported. Also, uses of formal variables of
-logic functions and global logic variables are not yet supported.
+However, quantified variables that use C variables in their bounds and
+let-binded variables that use C variables in their definition
+are not yet supported.
 
 \begin{example}
 The \verb|\at| construct of the following example is \emph{not yet} supported
-since the let-binded variable \verb|w| uses C variables, namely \verb|m| and
-\verb|n|, in its definition.
+since the quantified variable \verb|i| uses the C variable \verb|n| in the
+definition of its upper bound.
 \cinput{at_on-purely-logic-variables_not-yet.c}
 
 \end{example}