diff --git a/tests/misc/oracle/eva_annot.res.oracle b/tests/misc/oracle/eva_annot.res.oracle
index 30a1431306a486f23147309b7473fef7f9fb0806..a5f95b25d77c4d1e78b538490b0ba7715ad51f9d 100644
--- a/tests/misc/oracle/eva_annot.res.oracle
+++ b/tests/misc/oracle/eva_annot.res.oracle
@@ -17,13 +17,32 @@
 [eva:initial-state] Values of globals at initialization
   world ∈ {0}
   a[0..19] ∈ {0}
-[eva:loop-unroll:auto] eva_annot.c:21: Automatic loop unrolling.
+[eva:loop-unroll:auto] eva_annot.c:22: Automatic loop unrolling.
 [eva] using specification for function value
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   world ∈ [--..--]
-  a[0..19] ∈ [0..100]
-  s ∈ [0..2000]
+  a[0] ∈ [0..100]
+   [1] ∈ [1..101]
+   [2] ∈ [2..102]
+   [3] ∈ [3..103]
+   [4] ∈ [4..104]
+   [5] ∈ [5..105]
+   [6] ∈ [6..106]
+   [7] ∈ [7..107]
+   [8] ∈ [8..108]
+   [9] ∈ [9..109]
+   [10] ∈ [10..110]
+   [11] ∈ [11..111]
+   [12] ∈ [12..112]
+   [13] ∈ [13..113]
+   [14] ∈ [14..114]
+   [15] ∈ [15..115]
+   [16] ∈ [16..116]
+   [17] ∈ [17..117]
+   [18] ∈ [18..118]
+   [19] ∈ [19..119]
+  s ∈ [0. .. 2000.]
 [eva:summary] ====== ANALYSIS SUMMARY ======
   ----------------------------------------------------------------------------
   1 function analyzed (out of 1): 100% coverage.
@@ -41,33 +60,34 @@
 int a[20];
 /*@ ensures 0 ≤ \result ≤ 100;
     assigns \result, world;
-    assigns \result \from world;
-    assigns world \from world;
+    assigns \result \from world, root;
+    assigns world \from world, root;
  */
-int value(void);
+int value(int root);
 
-int main(void)
+float main(void)
 {
-  int s = 0;
+  float s = (float)0;
   {
     int i = 0;
     while (1) {
       /*@ assert Eva_domain: 0 ≤ i ≤ 20; */
       if (! (i < 20)) break;
       {
-        int v = value();
+        /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
+        int v = value(i + 1);
         /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
         /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
-        a[i] = v;
-        /*@ assert Eva_domain: 0 ≤ s ≤ 1900; */
+        a[i] = i + v;
+        /*@ assert Eva_domain: 0.00000000e+00f ≤ s ≤ 1.90000000e+03f; */
         /*@ assert Eva_domain: 0 ≤ v ≤ 100; */
-        s += v;
+        s += (float)v;
       }
       /*@ assert Eva_domain: 0 ≤ i ≤ 19; */
       i ++;
     }
   }
-  /*@ assert Eva_domain: 0 ≤ s ≤ 2000; */
+  /*@ assert Eva_domain: 0.00000000e+00f ≤ s ≤ 2.00000000e+03f; */
   return s;
 }