diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 5353425ece9574d6254226e58d28c89d5044383a..462f26204da38d60cf995e0d89212a15124db7c5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -845,10 +845,10 @@ struct __anonstruct___mpz_struct_1 {
 };
 typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(x,Old));
+/*@ ensures \valid(\old(x));
     assigns *x;  */
 extern void mpz_init(__mpz_struct * /*[1]*/  x ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void mpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
 /*@ requires \valid(x);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index b54bf42b8c7c4a90a1928f5a0e130febcd911508..668d1cda588f9a41aa81c31847968d34ee249834 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -272,7 +272,7 @@ struct __anonstruct___mpz_struct_1 {
 };
 typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void mpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
 /*@ requires \valid(x);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 5873fe9fa5fd46952260980d0a995c8de4923424..add013d268826cf38f3f055d501b1adc65692351 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -62,10 +62,10 @@ __pure__)) ;
 __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
                                           mp_size_t __gmp_n )  __attribute__((
 __pure__)) ;
-/*@ ensures \valid(\at(x,Old));
+/*@ ensures \valid(\old(x));
     assigns *x;  */
 extern void __gmpz_init(__mpz_struct * /*[1]*/  x ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
 /*@ requires \valid(z1);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 67cc8ed29d4399053476a717f4110e70dd24f14e..4d40b16e6a009bcfab1c9485c8214119ba1c5966 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -45,7 +45,7 @@ __pure__)) ;
 __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
                                           mp_size_t __gmp_n )  __attribute__((
 __pure__)) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
 __inline static void __gmpz_neg(__mpz_struct * /*[1]*/  z1 ,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 88b4e2f8fd4cac9769a8c37683ee7859be1866a6..20a0d8a44809e868434a19c3c17c5914ad9cda5a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -45,10 +45,10 @@ __pure__)) ;
 __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z ,
                                           mp_size_t __gmp_n )  __attribute__((
 __pure__)) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/  z ,
                                char const   *str , int base ) ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index 504adf43ccc1a6cfc0d143f183f2064648100a19..d9645140f4cd9fa938d6943834eaf3321fb7ed07 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -123,10 +123,10 @@ struct __anonstruct___mpz_struct_1 {
 };
 typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern void mpz_init_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
-/*@ ensures \valid(\at(z,Old));
+/*@ ensures \valid(\old(z));
     assigns *z;  */
 extern int mpz_init_set_str(__mpz_struct * /*[1]*/  z , char const   *str ,
                             int base ) ;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 03c5f2bfb2fb19e48dd2340ceeb4e1bcfe06e19e..04c863bb48c898dfce16371e7bcc85670b535b79 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -298,7 +298,6 @@ let rec term_to_exp t = match t.term_node with
   | Tlambda _ -> not_yet "functional"
   | TDataCons _ -> not_yet "constructor"
   | Tif _ -> not_yet "conditional"
-  | Told _ -> not_yet "\\old"
   | Tat _ -> not_yet "\\at"
   | Tbase_addr _ -> not_yet "\\base_addr"
   | Tblock_length _ -> not_yet "\\block_length"
@@ -350,7 +349,6 @@ let rec named_predicate_to_revexp p = match p.content with
   | Plet _ -> not_yet "let _ = _ in _"
   | Pforall _ -> not_yet "\\forall"
   | Pexists _ -> not_yet "\\exists"
-  | Pold _ -> not_yet "\\old"
   | Pat _ -> not_yet "\\at"
   | Pvalid _ -> type_error "\\valid"
   | Pvalid_index _ -> type_error "\\valid_index"