diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 85aad27349fe2d9e0b4851f2ecae6f151b94da39..fe66b29db23d30b6bfe5480ae673fc037920ed9a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -13,7 +13,8 @@ int f(int x)
 }
 
 int Y = 1;
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ \old(x);
+    ensures \result ≡ Y; */
 int __gen_e_acsl_g(int x);
 
 int g(int x)
@@ -48,17 +49,22 @@ int __gen_e_acsl_h(void)
   int __retres;
   __retres = h();
   __e_acsl_assert(__retres == 0,(char *)"Postcondition",(char *)"h",
-                  (char *)"\\result == 0",21);
+                  (char *)"\\result == 0",18);
   return __retres;
 }
 
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ \old(x);
+    ensures \result ≡ Y; */
 int __gen_e_acsl_g(int x)
 {
+  int __gen_e_acsl_at;
   int __retres;
+  __gen_e_acsl_at = x;
   __retres = g(x);
+  __e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
+                  (char *)"g",(char *)"\\result == \\old(x)",12);
   __e_acsl_assert(__retres == Y,(char *)"Postcondition",(char *)"g",
-                  (char *)"\\result == Y",16);
+                  (char *)"\\result == Y",13);
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/runtime/result.i b/src/plugins/e-acsl/tests/runtime/result.i
index 2391f60ce1497aabecd05a8bcf851db361ac671f..bae320b69ff040d389d0a712c98ad690f109ccc0 100644
--- a/src/plugins/e-acsl/tests/runtime/result.i
+++ b/src/plugins/e-acsl/tests/runtime/result.i
@@ -9,11 +9,8 @@ int f(int x) {
 
 int Y = 1;
 
-// does not work since it is converted into \result == \old(x) and, 
-// in this particular case, the pre-state and the post-state are the same and 
-// it does not work yet (related to issue in at.i).
-// /*@ ensures \result == x; */ 
-/*@ ensures \result == Y; */
+/*@ ensures \result == x;
+  @ ensures \result == Y; */
 int g(int x) { 
   return x; 
 }