diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 21e6f60037087fe70025dc22e78128b9040885f2..5780a467c29ee00228a8ab8d53e6b447a6a648be 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -19,6 +19,9 @@
 #   configure	configure
 ###############################################################################
 
+-* 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.
 -  E-ACSL       [2018/09/18] Support for ranges in memory builtins
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 99a5c9360d647dc13f05eebf515b6ff6fa296016..bbcf78dedebb7f60052f788e1606d485795cd53e 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -119,6 +119,8 @@ in \lstinline|\\at|}
 \subsection*{Version \eacslversion}
 
 \begin{itemize}
+\item \changeinsection{at}{support of \lstinline|\\at| on purely
+logic variables}
 \item \changeinsection{locations}{support of ranges in memory built-ins
   (e.g. \lstinline|\\valid| or \lstinline|\\initialized|)}
 \end{itemize}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 2b4fa7dec498ee36d6c79fa6a84e1a43bfe71fd0..b7213239b47d9445cfd9141e2f97724260d3b74e 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -512,6 +512,30 @@ only the first one is accepted and valid in \eacsl since evaluating the term
 
 \end{example}
 
+For the time being, \verb|\at| can be applied to any term or predicate that uses
+quantified variables, let-binded variables and C variables.
+
+\begin{example}
+The \verb|\at| construct of the following example is supported.
+\cinput{at_on-purely-logic-variables.c}
+
+\end{example}
+
+
+\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.
+
+\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.
+\cinput{at_on-purely-logic-variables_not-yet.c}
+
+\end{example}
+\end{notimplementedenv}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Statement contracts}
diff --git a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
index ef6ee47e37790f87a10e6c58561c0369039b78fe..a289de1d5a1c02e97bd12f1f5205a24c93639039 100644
--- a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
@@ -42,7 +42,7 @@ int main(void) {
   /*@ assert
       \exists integer u; 9 <= u < 21 &&
       \forall integer v; -5 < v <= (u < 15 ? u + 6 : 3) ==>
-        \at(n +  u + n > 0, K); */ ;
+        \at(n + u + v > 0, K); */ ;
 
   // Function calls:
   int t[5] = {9, 12, 12, 12, -4};
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
index e60a352da3bcb1f38ff9c2f0f9c3203a6c819bae..c6f65b06f7c80ea452bdd467b56a65ec502f71f2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
@@ -182,7 +182,7 @@ int main(void)
             if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
           }
           *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) = 
-          (n + (long)__gen_e_acsl_u_4) + n > 0L;
+          (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
           __gen_e_acsl_v_4 ++;
         }
         __gen_e_acsl_u_4 ++;
@@ -405,7 +405,7 @@ int main(void)
   /*@ assert
       ∃ ℤ u;
         9 ≤ u < 21 ∧
-        (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + n > 0,K));
+        (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
   */
   {
     int __gen_e_acsl_exists_4;
@@ -468,7 +468,7 @@ int main(void)
     }
     e_acsl_end_loop7: ;
     __e_acsl_assert(__gen_e_acsl_exists_4,(char *)"Assertion",(char *)"main",
-                    (char *)"\\exists integer u;\n  9 <= u < 21 &&\n  (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + n > 0,K))",
+                    (char *)"\\exists integer u;\n  9 <= u < 21 &&\n  (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
                     43);
   }
   int t[5] = {9, 12, 12, 12, -4};
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
index 771df194b253c0d7957ca44da637d78f143b5201..2c6d212d7a8b887c51dd0afd90d6b03a8fe215c7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
@@ -57,7 +57,7 @@ int main(void)
   assert
   ∃ ℤ u;
     9 ≤ u < 21 ∧
-    (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + n > 0,K));
+    (∀ ℤ v; -5 < v ≤ (u < 15? u + 6: 3) ⇒ \at((n + u) + v > 0,K));
    */
   ;
   int t[5] = {9, 12, 12, 12, -4};