diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 2652369061c2fa5e3363456d7454a7b849bf3f65..27b9451be0c0ce019141e58aa1eab2d32493c2ae 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -10,6 +10,8 @@
 - [Guillaume] ajouter les annotations de RTE dans la table des annotations
   	      (avec une option)
 - [David Mentré] tset
+- [Guillaume] voir les valeurs quand la spec échoue, voir Boogaloo@RV'13 à ce 
+  sujet
 
 #####################
 # E-ACSL CONSTRUCTS #
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 67423ac21da34824d10536b7f32fe2e0792cdcfb..2a29c1cd0354dd569bcb1a9da578856913c60b74 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -27,6 +27,11 @@ tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value:
                   assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2400..2848],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2880..3328],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3360..3808],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3840..4288],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [4320..4768],0%32.
 tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
index fe99e93ad604a53a1dc253d87d71877cdb508b34..c71a59ea7788d2dcb76b301df94d55460ad474fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
@@ -42,7 +42,16 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_l_2 < 15;
 tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value:
                   assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
-tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [0..4768],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [0..448],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [480..928],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [960..1408],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [1440..1888],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [1920..2368],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2400..2848],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [2880..3328],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3360..3808],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [3840..4288],0%32.
+tests/e-acsl-runtime/loop.i:21:[kernel] warning: completely indeterminate value in t with offsets [4320..4768],0%32.
 tests/e-acsl-runtime/loop.i:21:[value] all evaluations are invalid for function call argument
         (long)t[__e_acsl_k_2][__e_acsl_l_2]
 [value] using specification for function __gmpz_add