diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index 4e9b6c018300dfb4671f31e5fc5e00eff79be5ef..739a9a16e25a69a2f76d718b93c3c3e6a2baa0c9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -48,7 +48,7 @@ int main(void)
     e_acsl_end_loop1: ;
     __e_acsl_assert(__gen_e_acsl_forall,1,"Assertion","main",
                     "\\forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1",
-                    "tests/arith/quantif.i",15);
+                    "tests/arith/quantif.i",16);
   }
   /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */ ;
   {
@@ -68,7 +68,7 @@ int main(void)
     e_acsl_end_loop2: ;
     __e_acsl_assert(__gen_e_acsl_forall_2,1,"Assertion","main",
                     "\\forall integer x; 0 < x <= 1 ==> x == 1",
-                    "tests/arith/quantif.i",16);
+                    "tests/arith/quantif.i",17);
   }
   /*@ assert ∀ ℤ x; 0 < x ≤ 1 ⇒ x ≡ 1; */ ;
   {
@@ -88,7 +88,7 @@ int main(void)
     e_acsl_end_loop3: ;
     __e_acsl_assert(__gen_e_acsl_forall_3,1,"Assertion","main",
                     "\\forall integer x; 0 <= x < 1 ==> x == 0",
-                    "tests/arith/quantif.i",17);
+                    "tests/arith/quantif.i",18);
   }
   /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */ ;
   {
@@ -121,7 +121,7 @@ int main(void)
     e_acsl_end_loop4: ;
     __e_acsl_assert(__gen_e_acsl_forall_4,1,"Assertion","main",
                     "\\forall integer x, integer y, integer z;\n  0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1",
-                    "tests/arith/quantif.i",21);
+                    "tests/arith/quantif.i",22);
   }
   /*@
   assert
@@ -146,7 +146,7 @@ int main(void)
     e_acsl_end_loop5: ;
     __e_acsl_assert(__gen_e_acsl_exists,1,"Assertion","main",
                     "\\exists int x; 0 <= x < 10 && x == 5",
-                    "tests/arith/quantif.i",26);
+                    "tests/arith/quantif.i",27);
   }
   /*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */ ;
   {
@@ -187,7 +187,7 @@ int main(void)
     e_acsl_end_loop7: ;
     __e_acsl_assert(__gen_e_acsl_forall_5,1,"Assertion","main",
                     "\\forall int x;\n  0 <= x < 10 ==>\n  x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)",
-                    "tests/arith/quantif.i",30);
+                    "tests/arith/quantif.i",31);
   }
   /*@
   assert
@@ -223,7 +223,7 @@ int main(void)
       e_acsl_end_loop8: ;
       __e_acsl_assert(__gen_e_acsl_forall_6,1,"Assertion","main",
                       "\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
-                      "tests/arith/quantif.i",36);
+                      "tests/arith/quantif.i",37);
     }
     /*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ ;
     {
@@ -249,7 +249,7 @@ int main(void)
       e_acsl_end_loop9: ;
       __e_acsl_assert(__gen_e_acsl_forall_7,1,"Assertion","main",
                       "\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
-                      "tests/arith/quantif.i",37);
+                      "tests/arith/quantif.i",38);
     }
     /*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ ;
     {
@@ -275,7 +275,7 @@ int main(void)
       e_acsl_end_loop10: ;
       __e_acsl_assert(__gen_e_acsl_forall_8,1,"Assertion","main",
                       "\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
-                      "tests/arith/quantif.i",38);
+                      "tests/arith/quantif.i",39);
     }
     /*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */ ;
     {
@@ -330,7 +330,7 @@ int main(void)
       e_acsl_end_loop11: ;
       __e_acsl_assert(__gen_e_acsl_forall_9,1,"Assertion","main",
                       "\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
-                      "tests/arith/quantif.i",39);
+                      "tests/arith/quantif.i",40);
       __gmpz_clear(__gen_e_acsl_i_4);
     }
     /*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */ ;
@@ -338,18 +338,18 @@ int main(void)
   }
   __e_acsl_assert(1,1,"Assertion","main",
                   "\\forall integer x; 0 < x < 1 ==> \\false",
-                  "tests/arith/quantif.i",43);
+                  "tests/arith/quantif.i",44);
   /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */ ;
   __e_acsl_assert(! 0,1,"Assertion","main",
                   "!(\\exists char c; 10 <= c < 10 && c == 10)",
-                  "tests/arith/quantif.i",44);
+                  "tests/arith/quantif.i",45);
   /*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */ ;
   {
     int __gen_e_acsl_u;
     __gen_e_acsl_u = 5;
     __e_acsl_assert(1,1,"Assertion","main",
                     "\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
-                    "tests/arith/quantif.i",46);
+                    "tests/arith/quantif.i",47);
   }
   /*@
   assert \let u = 5; ∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
@@ -390,7 +390,7 @@ int main(void)
     e_acsl_end_loop12: ;
     __e_acsl_assert(__gen_e_acsl_forall_10,1,"Assertion","main",
                     "forall_multiple_binders_1:\n  \\forall integer i, integer j, integer k;\n    0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 ==> p1(i, j, k)",
-                    "tests/arith/quantif.i",51);
+                    "tests/arith/quantif.i",52);
   }
   /*@
   assert
@@ -434,7 +434,7 @@ int main(void)
     e_acsl_end_loop13: ;
     __e_acsl_assert(__gen_e_acsl_forall_11,1,"Assertion","main",
                     "forall_multiple_binders_2:\n  \\forall integer i, integer j, integer k;\n    0 <= i <= j < k <= 10 ==> p2(i, j, k)",
-                    "tests/arith/quantif.i",54);
+                    "tests/arith/quantif.i",55);
   }
   /*@
   assert
@@ -477,7 +477,7 @@ int main(void)
     e_acsl_end_loop14: ;
     __e_acsl_assert(__gen_e_acsl_forall_12,1,"Assertion","main",
                     "forall_multiple_binders_3:\n  \\forall integer i, integer j, integer k;\n    0 <= i < j <= 10 && 1 < k < 11 ==> p3(i, j, k)",
-                    "tests/arith/quantif.i",57);
+                    "tests/arith/quantif.i",58);
   }
   /*@
   assert
@@ -521,7 +521,7 @@ int main(void)
     e_acsl_end_loop15: ;
     __e_acsl_assert(__gen_e_acsl_forall_13,1,"Assertion","main",
                     "forall_multiple_binders_4:\n  \\forall integer i, integer j, integer k;\n    0 <= i < 10 ==> 1 < j <= 11 ==> 2 <= k <= 12 ==> p1(i, j, k)",
-                    "tests/arith/quantif.i",60);
+                    "tests/arith/quantif.i",61);
   }
   /*@
   assert
@@ -565,7 +565,7 @@ int main(void)
     e_acsl_end_loop16: ;
     __e_acsl_assert(__gen_e_acsl_forall_14,1,"Assertion","main",
                     "forall_unordered_binders:\n  \\forall integer i, integer j, integer k;\n    0 <= i <= k <= 10 && 1 <= j < k ==> p4(i, j, k)",
-                    "tests/arith/quantif.i",63);
+                    "tests/arith/quantif.i",64);
   }
   /*@
   assert
@@ -609,7 +609,7 @@ int main(void)
     e_acsl_end_loop17: ;
     __e_acsl_assert(__gen_e_acsl_exists_3,1,"Assertion","main",
                     "exists_multiple_binders_1:\n  \\exists integer i, integer j, integer k;\n    0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 && p1(i, j, k)",
-                    "tests/arith/quantif.i",66);
+                    "tests/arith/quantif.i",67);
   }
   /*@
   assert
@@ -653,7 +653,7 @@ int main(void)
     e_acsl_end_loop18: ;
     __e_acsl_assert(__gen_e_acsl_exists_4,1,"Assertion","main",
                     "exists_multiple_binders_2:\n  \\exists integer i, integer j, integer k;\n    0 <= i <= j < k <= 10 && p2(i, j, k)",
-                    "tests/arith/quantif.i",69);
+                    "tests/arith/quantif.i",70);
   }
   /*@
   assert
@@ -696,7 +696,7 @@ int main(void)
     e_acsl_end_loop19: ;
     __e_acsl_assert(__gen_e_acsl_exists_5,1,"Assertion","main",
                     "exists_multiple_binders_3:\n  \\exists integer i, integer j, integer k;\n    0 <= i < j <= 10 && 1 < k < 11 && p3(i, j, k)",
-                    "tests/arith/quantif.i",72);
+                    "tests/arith/quantif.i",73);
   }
   /*@
   assert
@@ -740,7 +740,7 @@ int main(void)
     e_acsl_end_loop20: ;
     __e_acsl_assert(__gen_e_acsl_exists_6,1,"Assertion","main",
                     "exists_unordered_binders:\n  \\exists integer i, integer j, integer k;\n    0 <= i <= k <= 10 && 1 <= j < k && p4(i, j, k)",
-                    "tests/arith/quantif.i",75);
+                    "tests/arith/quantif.i",76);
   }
   /*@
   assert
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
index 5e70777069f3e532c1c5d602600e2824a295e93b..362a4d3b1798252f52ecebda63c5101c8bfe6c56 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
@@ -30,7 +30,7 @@ int main(void)
     }
     __e_acsl_assert(__gen_e_acsl_sum == 108,1,"Assertion","main",
                     "\\sum(2, 10, \\lambda integer k; 2 * k) == 108",
-                    "tests/arith/sum.i",9);
+                    "tests/arith/sum.i",10);
   }
   /*@ assert \sum(2, 10, \lambda ℤ k; 2 * k) ≡ 108; */ ;
   {
@@ -60,10 +60,6 @@ int main(void)
         __gmpz_add(__gen_e_acsl_sum_2,
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_sum_2),
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_2));
-        /*@ assert
-            Eva: signed_overflow:
-              __gen_e_acsl_k_2 + __gen_e_acsl_one_2 ≤ 2147483647;
-        */
         __gen_e_acsl_k_2 += __gen_e_acsl_one_2;
       }
     }
@@ -72,7 +68,7 @@ int main(void)
                                  (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
     __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","main",
                     "\\sum(2, 35, \\lambda integer k; 18446744073709551615) != 0",
-                    "tests/arith/sum.i",11);
+                    "tests/arith/sum.i",12);
     __gmpz_clear(__gen_e_acsl_lambda_2);
     __gmpz_clear(__gen_e_acsl_sum_2);
     __gmpz_clear(__gen_e_acsl__2);
@@ -100,7 +96,7 @@ int main(void)
     }
     __e_acsl_assert(__gen_e_acsl_sum_3 == 0,1,"Assertion","main",
                     "\\sum(10, 2, \\lambda integer k; k) == 0",
-                    "tests/arith/sum.i",13);
+                    "tests/arith/sum.i",14);
   }
   /*@ assert \sum(10, 2, \lambda ℤ k; k) ≡ 0; */ ;
   {
@@ -146,7 +142,7 @@ int main(void)
                                  (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
     __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
                     "\\sum(x * x, 2, \\lambda integer k; k) == 0",
-                    "tests/arith/sum.i",15);
+                    "tests/arith/sum.i",16);
     __gmpz_clear(__gen_e_acsl_x);
     __gmpz_clear(__gen_e_acsl_mul);
     __gmpz_clear(__gen_e_acsl__3);
@@ -191,7 +187,7 @@ int main(void)
     }
     __e_acsl_assert(__gen_e_acsl_sum_5 == 6,1,"Assertion","main",
                     "\\sum(18446744073709551610, 18446744073709551615, \\lambda integer k; 1) == 6",
-                    "tests/arith/sum.i",17);
+                    "tests/arith/sum.i",18);
     __gmpz_clear(__gen_e_acsl__5);
     __gmpz_clear(__gen_e_acsl__6);
     __gmpz_clear(__gen_e_acsl_k_5);
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
index bcc5b8e29950cffd37a8b4638ffdc90428a57dc9..f19157d05414752406e69daa907e176bc421acb4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
@@ -1,67 +1,67 @@
 [e-acsl] beginning translation.
-[e-acsl] tests/arith/quantif.i:80: Warning: 
+[e-acsl] tests/arith/quantif.i:81: Warning: 
   invalid E-ACSL construct
   `invalid guard 10 > i in quantification
   failed_invalid_guards: ∀ ℤ i; 10 > i ≥ 0 ⇒ p1(i, 2, 2).
   Missing guard for i. Only < and ≤ are allowed to guard quantifier variables'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:82: Warning: 
+[e-acsl] tests/arith/quantif.i:83: Warning: 
   invalid E-ACSL construct
   `invalid guard p1(i, j, k) in quantification
   failed_unguarded_k:
     ∀ ℤ i, ℤ j, ℤ k; 0 ≤ i < 10 ∧ 1 < j ≤ 11 ⇒ p1(i, j, k).
   Missing guard for k. '.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:84: Warning: 
+[e-acsl] tests/arith/quantif.i:85: Warning: 
   E-ACSL construct
   `non integer variable i in quantification
   failed_non_integer: ∀ ℝ i; 0 ≤ i < 10 ⇒ p1(\truncate(i), 2, 2)'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:86: Warning: 
+[e-acsl] tests/arith/quantif.i:87: Warning: 
   invalid E-ACSL construct
   `missing lower bound for i in quantification
   failed_missing_lower_bound: ∀ ℤ i; i < 10 ⇒ p1(i, 2, 2)'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:88: Warning: 
+[e-acsl] tests/arith/quantif.i:89: Warning: 
   invalid E-ACSL construct
   `invalid guard p1(i, 2, 2) in quantification
   failded_missing_upper_bound: ∀ ℤ i; 0 ≤ i ⇒ p1(i, 2, 2). 
   Missing upper bound for i. '.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:90: Warning: 
+[e-acsl] tests/arith/quantif.i:91: Warning: 
   invalid E-ACSL construct
   `invalid guard p1(i, j, 2) in quantification
   failed_invalid_upper_bound_1: ∀ ℤ i, ℤ j; 0 ≤ i < j ⇒ p1(i, j, 2). 
   Missing upper bound for j. '.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:92: Warning: 
+[e-acsl] tests/arith/quantif.i:93: Warning: 
   invalid E-ACSL construct
   `missing lower bound for i when processing the linked upper bound i < j
   in quantification
   failed_invalid_upper_bound_2:
     ∀ ℤ i, ℤ j; i < j ∧ 0 ≤ i ⇒ p1(i, 2, 2)'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:94: Warning: 
+[e-acsl] tests/arith/quantif.i:95: Warning: 
   invalid E-ACSL construct
   `found existing lower bound i < j when processing 3 ≤ j in quantification
   failed_extra_constraint:
     ∀ ℤ i, ℤ j; 0 ≤ i < j ∧ i < 10 ∧ 3 ≤ j < 5 ⇒ p1(i, j, 2)'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:96: Warning: 
+[e-acsl] tests/arith/quantif.i:97: Warning: 
   invalid E-ACSL construct
   `found existing lower bound 0 ≤ i when processing j < i in quantification
   failed_multiple_upper_bounds:
     ∀ ℤ i, ℤ j; 0 ≤ i < j < i ∧ j ≤ 10 ⇒ p1(i, j, 2)'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:98: Warning: 
+[e-acsl] tests/arith/quantif.i:99: Warning: 
   invalid E-ACSL construct
   `found existing lower bound i < k when processing j < k in quantification
   multiple_linked_upper:
     ∀ ℤ i, ℤ j, ℤ k;
       0 ≤ i < k ∧ 1 ≤ j < k ∧ 2 ≤ k < 10 ⇒ p1(i, j, k)'.
   Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:100: Warning: 
+[e-acsl] tests/arith/quantif.i:101: Warning: 
   invalid E-ACSL construct
   `invalid constraint 2 ≤ i, both operands are constants or already bounded in quantification
   multiple_guard:
@@ -69,44 +69,36 @@
       0 ≤ i < 10 ∧ 2 ≤ i < 8 ∧ 4 ≤ j < 6 ⇒ p1(i, j, 2)'.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/quantif.i:21: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/arith/quantif.i:21: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:30: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:39: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/arith/quantif.i:46: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:54: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/arith/quantif.i:54: Warning: 
+[eva:alarm] tests/arith/quantif.i:22: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:31: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:40: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:47: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:55: Warning: 
   assertion 'forall_multiple_binders_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:57: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/arith/quantif.i:57: Warning: 
+[eva:alarm] tests/arith/quantif.i:58: Warning: 
   assertion 'forall_multiple_binders_3' got status unknown.
-[eva:alarm] tests/arith/quantif.i:63: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/arith/quantif.i:63: Warning: 
+[eva:alarm] tests/arith/quantif.i:64: Warning: 
   assertion 'forall_unordered_binders' got status unknown.
-[eva:alarm] tests/arith/quantif.i:69: Warning: 
+[eva:alarm] tests/arith/quantif.i:70: Warning: 
   assertion 'exists_multiple_binders_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:72: Warning: 
+[eva:alarm] tests/arith/quantif.i:73: Warning: 
   assertion 'exists_multiple_binders_3' got status unknown.
-[eva:alarm] tests/arith/quantif.i:75: Warning: 
+[eva:alarm] tests/arith/quantif.i:76: Warning: 
   assertion 'exists_unordered_binders' got status unknown.
-[eva:alarm] tests/arith/quantif.i:82: Warning: 
+[eva:alarm] tests/arith/quantif.i:83: Warning: 
   assertion 'failed_unguarded_k' got status unknown.
-[eva:alarm] tests/arith/quantif.i:84: Warning: 
+[eva:alarm] tests/arith/quantif.i:85: Warning: 
   assertion 'failed_non_integer' got status unknown.
-[eva:alarm] tests/arith/quantif.i:86: Warning: 
+[eva:alarm] tests/arith/quantif.i:87: Warning: 
   assertion 'failed_missing_lower_bound' got status unknown.
-[eva:alarm] tests/arith/quantif.i:88: Warning: 
+[eva:alarm] tests/arith/quantif.i:89: Warning: 
   assertion 'failded_missing_upper_bound' got status unknown.
-[eva:alarm] tests/arith/quantif.i:90: Warning: 
+[eva:alarm] tests/arith/quantif.i:91: Warning: 
   assertion 'failed_invalid_upper_bound_1' got status unknown.
-[eva:alarm] tests/arith/quantif.i:92: Warning: 
+[eva:alarm] tests/arith/quantif.i:93: Warning: 
   assertion 'failed_invalid_upper_bound_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:96: Warning: 
+[eva:alarm] tests/arith/quantif.i:97: Warning: 
   assertion 'failed_multiple_upper_bounds' got status unknown.
-[eva:alarm] tests/arith/quantif.i:98: Warning: 
+[eva:alarm] tests/arith/quantif.i:99: Warning: 
   assertion 'multiple_linked_upper' got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
index 5755a0ac2816326556bbb7426f204961831d3b06..9a451aa3e6bba03daa79b4d27ab73a7b92c0fcc8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
@@ -39,8 +39,6 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/rationals.c:4: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:4: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] tests/arith/rationals.c:4: Warning: 
   function __gen_e_acsl_avg: postcondition got status unknown.
 [eva:alarm] tests/arith/rationals.c:29: Warning: 
diff --git a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
index bc11e73b17fdafc6c275f527f316f74da69ad6ab..df0b0c5c271fba45ac9f080c494664c60e65f105 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
@@ -1,18 +1,16 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/sum.i:9: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:11: Warning: 
-  signed overflow. assert __gen_e_acsl_k_2 + __gen_e_acsl_one_2 ≤ 2147483647;
-[eva:alarm] tests/arith/sum.i:11: Warning: 
+[eva:alarm] tests/arith/sum.i:10: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.i:12: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:11: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:13: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:15: Warning: 
+[eva:alarm] tests/arith/sum.i:12: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.i:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.i:16: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:15: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/sum.i:17: Warning: 
+[eva:alarm] tests/arith/sum.i:16: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.i:18: Warning: 
   signed overflow.
   assert __gen_e_acsl_sum_5 + __gen_e_acsl_lambda_5 ≤ 2147483647;
-[eva:alarm] tests/arith/sum.i:17: Warning: 
+[eva:alarm] tests/arith/sum.i:18: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/sum.i:17: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.i:18: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index ef6ec87ac427333fcee748159cf6993c89461ecf..81e8acd74d625e25004b04543d8a9d3024ce016d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -46,7 +46,7 @@ int main(void)
                                                     sizeof(union msg));
     __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
                     "\\initialized((union msg *)((unsigned char *)buf))",
-                    "tests/bts/bts1304.i",23);
+                    "tests/bts/bts1304.i",24);
   }
   /*@ assert \initialized((union msg *)((unsigned char *)buf)); */ ;
   __retres = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index e79ccbae463cd4ea3afee5dd6424896e73a369b2..98da9b92aa86932c8548f21c13d7f5b071e1ccb9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -21,7 +21,7 @@ int f(void)
     __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)S,sizeof(char),
                                                   (void *)S,(void *)(& S));
     __e_acsl_assert(__gen_e_acsl_valid_read,1,"Assertion","f",
-                    "\\valid_read(S)","tests/bts/bts1837.i",10);
+                    "\\valid_read(S)","tests/bts/bts1837.i",11);
   }
   /*@ assert \valid_read(S); */ ;
   {
@@ -39,7 +39,7 @@ int f(void)
     }
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","f","\\valid_read(s1)",
-                    "tests/bts/bts1837.i",11);
+                    "tests/bts/bts1837.i",12);
   }
   /*@ assert \valid_read(s1); */ ;
   {
@@ -57,7 +57,7 @@ int f(void)
     }
     else __gen_e_acsl_and_2 = 0;
     __e_acsl_assert(__gen_e_acsl_and_2,1,"Assertion","f","\\valid_read(s2)",
-                    "tests/bts/bts1837.i",12);
+                    "tests/bts/bts1837.i",13);
   }
   /*@ assert \valid_read(s2); */ ;
   __retres = 0;
@@ -127,7 +127,7 @@ int main(void)
         }
         else __gen_e_acsl_and = 0;
         __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","main",
-                        "\\valid_read(s)","tests/bts/bts1837.i",20);
+                        "\\valid_read(s)","tests/bts/bts1837.i",21);
       }
       /*@ assert \valid_read(s); */ ;
       {
@@ -143,7 +143,7 @@ int main(void)
         }
         else __gen_e_acsl_and_2 = 0;
         __e_acsl_assert(! __gen_e_acsl_and_2,1,"Assertion","main",
-                        "!\\valid(s)","tests/bts/bts1837.i",21);
+                        "!\\valid(s)","tests/bts/bts1837.i",22);
       }
       /*@ assert ¬\valid(s); */ ;
       __e_acsl_delete_block((void *)(& s));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
index e6e4eb7768ce069596adadbef5a2e82b3996dcb0..206e0f2af8778fd0860ed99a149a6d8c837113c8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
@@ -33,17 +33,15 @@
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
   function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
 [eva:alarm] tests/bts/issue-eacsl-40.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/bts/issue-eacsl-40.c:15: Warning: 
+  assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index b26e3c1f7a70d37418abb8b9327c88cff7b6a8c8..d61abbeb6de23fdca5d7251c280f2b0edb11f85c 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -9,7 +9,6 @@
 #include "sys/types.h"
 #include "sys/wait.h"
 #include "unistd.h"
-char *__gen_e_acsl_literal_string_29;
 char *__gen_e_acsl_literal_string_28;
 char *__gen_e_acsl_literal_string_27;
 char *__gen_e_acsl_literal_string_26;
@@ -31,6 +30,7 @@ char *__gen_e_acsl_literal_string_11;
 char *__gen_e_acsl_literal_string_10;
 char *__gen_e_acsl_literal_string_9;
 char *__gen_e_acsl_literal_string_30;
+char *__gen_e_acsl_literal_string_29;
 char *__gen_e_acsl_literal_string_7;
 char *__gen_e_acsl_literal_string_6;
 char *__gen_e_acsl_literal_string;
@@ -96,7 +96,7 @@ void test_memory_tracking(void)
                                                       (size_t)__gen_e_acsl_if);
       __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion",
                       "test_memory_tracking","\\initialized(&dest[0 .. 1])",
-                      "tests/builtin/strcat.c",14);
+                      "tests/builtin/strcat.c",15);
     }
     /*@ assert \initialized(&dest[0 .. 1]); */ ;
     {
@@ -110,7 +110,7 @@ void test_memory_tracking(void)
                                                         (size_t)__gen_e_acsl_if_2);
       __e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion",
                       "test_memory_tracking","!\\initialized(&dest[2 .. 3])",
-                      "tests/builtin/strcat.c",15);
+                      "tests/builtin/strcat.c",16);
     }
     /*@ assert ¬\initialized(&dest[2 .. 3]); */ ;
     {
@@ -124,7 +124,7 @@ void test_memory_tracking(void)
                                                         (size_t)__gen_e_acsl_if_3);
       __e_acsl_assert(__gen_e_acsl_initialized_3,1,"Assertion",
                       "test_memory_tracking","\\initialized(&src[0 .. 1])",
-                      "tests/builtin/strcat.c",16);
+                      "tests/builtin/strcat.c",17);
     }
     /*@ assert \initialized(&src[0 .. 1]); */ ;
     __e_acsl_builtin_strcat(dest,(char const *)(src));
@@ -139,7 +139,7 @@ void test_memory_tracking(void)
                                                         (size_t)__gen_e_acsl_if_4);
       __e_acsl_assert(__gen_e_acsl_initialized_4,1,"Assertion",
                       "test_memory_tracking","\\initialized(&dest[0 .. 2])",
-                      "tests/builtin/strcat.c",19);
+                      "tests/builtin/strcat.c",20);
     }
     /*@ assert \initialized(&dest[0 .. 2]); */ ;
     {
@@ -148,7 +148,7 @@ void test_memory_tracking(void)
                                                         sizeof(char));
       __e_acsl_assert(! __gen_e_acsl_initialized_5,1,"Assertion",
                       "test_memory_tracking","!\\initialized(&dest[3])",
-                      "tests/builtin/strcat.c",20);
+                      "tests/builtin/strcat.c",21);
     }
     /*@ assert ¬\initialized(&dest[3]); */ ;
     __e_acsl_delete_block((void *)(src));
@@ -174,7 +174,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(__gen_e_acsl_initialized_6,1,"Assertion",
                       "test_memory_tracking",
                       "\\initialized(&dest_0[0 .. 1])",
-                      "tests/builtin/strcat.c",26);
+                      "tests/builtin/strcat.c",27);
     }
     /*@ assert \initialized(&dest_0[0 .. 1]); */ ;
     {
@@ -190,7 +190,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(! __gen_e_acsl_initialized_7,1,"Assertion",
                       "test_memory_tracking",
                       "!\\initialized(&dest_0[2 .. 3])",
-                      "tests/builtin/strcat.c",27);
+                      "tests/builtin/strcat.c",28);
     }
     /*@ assert ¬\initialized(&dest_0[2 .. 3]); */ ;
     {
@@ -205,7 +205,7 @@ void test_memory_tracking(void)
                                                         (size_t)__gen_e_acsl_if_7);
       __e_acsl_assert(__gen_e_acsl_initialized_8,1,"Assertion",
                       "test_memory_tracking","\\initialized(&src_0[0 .. 2])",
-                      "tests/builtin/strcat.c",28);
+                      "tests/builtin/strcat.c",29);
     }
     /*@ assert \initialized(&src_0[0 .. 2]); */ ;
     __e_acsl_builtin_strncat(dest_0,(char const *)(src_0),(unsigned long)1);
@@ -222,7 +222,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(__gen_e_acsl_initialized_9,1,"Assertion",
                       "test_memory_tracking",
                       "\\initialized(&dest_0[0 .. 2])",
-                      "tests/builtin/strcat.c",31);
+                      "tests/builtin/strcat.c",32);
     }
     /*@ assert \initialized(&dest_0[0 .. 2]); */ ;
     {
@@ -231,7 +231,7 @@ void test_memory_tracking(void)
                                                          sizeof(char));
       __e_acsl_assert(! __gen_e_acsl_initialized_10,1,"Assertion",
                       "test_memory_tracking","!\\initialized(&dest_0[3])",
-                      "tests/builtin/strcat.c",32);
+                      "tests/builtin/strcat.c",33);
     }
     /*@ assert ¬\initialized(&dest_0[3]); */ ;
     __e_acsl_delete_block((void *)(src_0));
@@ -257,7 +257,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(__gen_e_acsl_initialized_11,1,"Assertion",
                       "test_memory_tracking",
                       "\\initialized(&dest_1[0 .. 1])",
-                      "tests/builtin/strcat.c",38);
+                      "tests/builtin/strcat.c",39);
     }
     /*@ assert \initialized(&dest_1[0 .. 1]); */ ;
     {
@@ -273,7 +273,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(! __gen_e_acsl_initialized_12,1,"Assertion",
                       "test_memory_tracking",
                       "!\\initialized(&dest_1[2 .. 3])",
-                      "tests/builtin/strcat.c",39);
+                      "tests/builtin/strcat.c",40);
     }
     /*@ assert ¬\initialized(&dest_1[2 .. 3]); */ ;
     {
@@ -288,7 +288,7 @@ void test_memory_tracking(void)
                                                          (size_t)__gen_e_acsl_if_11);
       __e_acsl_assert(__gen_e_acsl_initialized_13,1,"Assertion",
                       "test_memory_tracking","\\initialized(&src_1[0 .. 1])",
-                      "tests/builtin/strcat.c",40);
+                      "tests/builtin/strcat.c",41);
     }
     /*@ assert \initialized(&src_1[0 .. 1]); */ ;
     __e_acsl_builtin_strncat(dest_1,(char const *)(src_1),(unsigned long)2);
@@ -305,7 +305,7 @@ void test_memory_tracking(void)
       __e_acsl_assert(__gen_e_acsl_initialized_14,1,"Assertion",
                       "test_memory_tracking",
                       "\\initialized(&dest_1[0 .. 2])",
-                      "tests/builtin/strcat.c",43);
+                      "tests/builtin/strcat.c",44);
     }
     /*@ assert \initialized(&dest_1[0 .. 2]); */ ;
     {
@@ -314,7 +314,7 @@ void test_memory_tracking(void)
                                                          sizeof(char));
       __e_acsl_assert(! __gen_e_acsl_initialized_15,1,"Assertion",
                       "test_memory_tracking","!\\initialized(&dest_1[3])",
-                      "tests/builtin/strcat.c",44);
+                      "tests/builtin/strcat.c",45);
     }
     /*@ assert ¬\initialized(&dest_1[3]); */ ;
     __e_acsl_delete_block((void *)(src_1));
@@ -439,116 +439,116 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __gen_e_acsl_literal_string_29 = "tests/builtin/strcat.c:99";
-    __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
-                         sizeof("tests/builtin/strcat.c:99"));
-    __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
-    __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
-    __gen_e_acsl_literal_string_28 = "tests/builtin/strcat.c:98";
+    __gen_e_acsl_literal_string_28 = "tests/builtin/strcat.c:99";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
-                         sizeof("tests/builtin/strcat.c:98"));
+                         sizeof("tests/builtin/strcat.c:99"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
-    __gen_e_acsl_literal_string_27 = "tests/builtin/strcat.c:96";
+    __gen_e_acsl_literal_string_27 = "tests/builtin/strcat.c:97";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
-                         sizeof("tests/builtin/strcat.c:96"));
+                         sizeof("tests/builtin/strcat.c:97"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
-    __gen_e_acsl_literal_string_26 = "tests/builtin/strcat.c:95";
+    __gen_e_acsl_literal_string_26 = "tests/builtin/strcat.c:96";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
-                         sizeof("tests/builtin/strcat.c:95"));
+                         sizeof("tests/builtin/strcat.c:96"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
-    __gen_e_acsl_literal_string_25 = "tests/builtin/strcat.c:94";
+    __gen_e_acsl_literal_string_25 = "tests/builtin/strcat.c:95";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
-                         sizeof("tests/builtin/strcat.c:94"));
+                         sizeof("tests/builtin/strcat.c:95"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
-    __gen_e_acsl_literal_string_24 = "tests/builtin/strcat.c:93";
+    __gen_e_acsl_literal_string_24 = "tests/builtin/strcat.c:94";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
-                         sizeof("tests/builtin/strcat.c:93"));
+                         sizeof("tests/builtin/strcat.c:94"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
-    __gen_e_acsl_literal_string_23 = "tests/builtin/strcat.c:92";
+    __gen_e_acsl_literal_string_23 = "tests/builtin/strcat.c:93";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
-                         sizeof("tests/builtin/strcat.c:92"));
+                         sizeof("tests/builtin/strcat.c:93"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
-    __gen_e_acsl_literal_string_22 = "tests/builtin/strcat.c:91";
+    __gen_e_acsl_literal_string_22 = "tests/builtin/strcat.c:92";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
-                         sizeof("tests/builtin/strcat.c:91"));
+                         sizeof("tests/builtin/strcat.c:92"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
-    __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:90";
+    __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:91";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
-                         sizeof("tests/builtin/strcat.c:90"));
+                         sizeof("tests/builtin/strcat.c:91"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
-    __gen_e_acsl_literal_string_20 = "tests/builtin/strcat.c:77";
+    __gen_e_acsl_literal_string_20 = "tests/builtin/strcat.c:78";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
-                         sizeof("tests/builtin/strcat.c:77"));
+                         sizeof("tests/builtin/strcat.c:78"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
-    __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:76";
+    __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:77";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
-                         sizeof("tests/builtin/strcat.c:76"));
+                         sizeof("tests/builtin/strcat.c:77"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
-    __gen_e_acsl_literal_string_18 = "tests/builtin/strcat.c:75";
+    __gen_e_acsl_literal_string_18 = "tests/builtin/strcat.c:76";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
-                         sizeof("tests/builtin/strcat.c:75"));
+                         sizeof("tests/builtin/strcat.c:76"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
-    __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:74";
+    __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:75";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
-                         sizeof("tests/builtin/strcat.c:74"));
+                         sizeof("tests/builtin/strcat.c:75"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
-    __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:73";
+    __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:74";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
-                         sizeof("tests/builtin/strcat.c:73"));
+                         sizeof("tests/builtin/strcat.c:74"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
-    __gen_e_acsl_literal_string_15 = "tests/builtin/strcat.c:72";
+    __gen_e_acsl_literal_string_15 = "tests/builtin/strcat.c:73";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
-                         sizeof("tests/builtin/strcat.c:72"));
+                         sizeof("tests/builtin/strcat.c:73"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
-    __gen_e_acsl_literal_string_14 = "tests/builtin/strcat.c:71";
+    __gen_e_acsl_literal_string_14 = "tests/builtin/strcat.c:72";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
-                         sizeof("tests/builtin/strcat.c:71"));
+                         sizeof("tests/builtin/strcat.c:72"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __gen_e_acsl_literal_string_13 = "tests/builtin/strcat.c:70";
+    __gen_e_acsl_literal_string_13 = "tests/builtin/strcat.c:71";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
-                         sizeof("tests/builtin/strcat.c:70"));
+                         sizeof("tests/builtin/strcat.c:71"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
-    __gen_e_acsl_literal_string_12 = "tests/builtin/strcat.c:69";
+    __gen_e_acsl_literal_string_12 = "tests/builtin/strcat.c:70";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
-                         sizeof("tests/builtin/strcat.c:69"));
+                         sizeof("tests/builtin/strcat.c:70"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
-    __gen_e_acsl_literal_string_11 = "tests/builtin/strcat.c:68";
+    __gen_e_acsl_literal_string_11 = "tests/builtin/strcat.c:69";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
-                         sizeof("tests/builtin/strcat.c:68"));
+                         sizeof("tests/builtin/strcat.c:69"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
-    __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:67";
+    __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:68";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
-                         sizeof("tests/builtin/strcat.c:67"));
+                         sizeof("tests/builtin/strcat.c:68"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
-    __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:66";
+    __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:67";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
-                         sizeof("tests/builtin/strcat.c:66"));
+                         sizeof("tests/builtin/strcat.c:67"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
-    __gen_e_acsl_literal_string_30 = "tests/builtin/strcat.c:100";
+    __gen_e_acsl_literal_string_30 = "tests/builtin/strcat.c:101";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
-                         sizeof("tests/builtin/strcat.c:100"));
+                         sizeof("tests/builtin/strcat.c:101"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
+    __gen_e_acsl_literal_string_29 = "tests/builtin/strcat.c:100";
+    __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
+                         sizeof("tests/builtin/strcat.c:100"));
+    __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
+    __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
     __gen_e_acsl_literal_string_7 = "abcd";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
                          sizeof("abcd"));
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
index 3e0326a3b6030646f8ead6e203483521643d43c5..c9aba380e55deebb69faeacf037889e18c20a47d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
@@ -1,40 +1,40 @@
-TEST 1: OK: Expected execution at tests/builtin/strcat.c:66
-TEST 2: OK: Expected execution at tests/builtin/strcat.c:67
+TEST 1: OK: Expected execution at tests/builtin/strcat.c:67
+TEST 2: OK: Expected execution at tests/builtin/strcat.c:68
 strcat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 3: OK: Expected signal at tests/builtin/strcat.c:68
+TEST 3: OK: Expected signal at tests/builtin/strcat.c:69
 strcat: destination string string unallocated
-TEST 4: OK: Expected signal at tests/builtin/strcat.c:69
+TEST 4: OK: Expected signal at tests/builtin/strcat.c:70
 strcat: source string string unallocated
-TEST 5: OK: Expected signal at tests/builtin/strcat.c:70
+TEST 5: OK: Expected signal at tests/builtin/strcat.c:71
 strcat: destination string string unallocated
-TEST 6: OK: Expected signal at tests/builtin/strcat.c:71
+TEST 6: OK: Expected signal at tests/builtin/strcat.c:72
 strcat: source string string unallocated
-TEST 7: OK: Expected signal at tests/builtin/strcat.c:72
+TEST 7: OK: Expected signal at tests/builtin/strcat.c:73
 strcat: destination string string is not writable
-TEST 8: OK: Expected signal at tests/builtin/strcat.c:73
+TEST 8: OK: Expected signal at tests/builtin/strcat.c:74
 strcat: overlapping memory areas
-TEST 9: OK: Expected signal at tests/builtin/strcat.c:74
+TEST 9: OK: Expected signal at tests/builtin/strcat.c:75
 strcat: overlapping memory areas
-TEST 10: OK: Expected signal at tests/builtin/strcat.c:75
+TEST 10: OK: Expected signal at tests/builtin/strcat.c:76
 strcat: overlapping memory areas
-TEST 11: OK: Expected signal at tests/builtin/strcat.c:76
-TEST 12: OK: Expected execution at tests/builtin/strcat.c:77
-TEST 13: OK: Expected execution at tests/builtin/strcat.c:90
+TEST 11: OK: Expected signal at tests/builtin/strcat.c:77
+TEST 12: OK: Expected execution at tests/builtin/strcat.c:78
+TEST 13: OK: Expected execution at tests/builtin/strcat.c:91
 strncat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 14: OK: Expected signal at tests/builtin/strcat.c:91
+TEST 14: OK: Expected signal at tests/builtin/strcat.c:92
 strcat: destination string string unallocated
-TEST 15: OK: Expected signal at tests/builtin/strcat.c:92
+TEST 15: OK: Expected signal at tests/builtin/strcat.c:93
 strncat: source string string unallocated
-TEST 16: OK: Expected signal at tests/builtin/strcat.c:93
+TEST 16: OK: Expected signal at tests/builtin/strcat.c:94
 strcat: destination string string unallocated
-TEST 17: OK: Expected signal at tests/builtin/strcat.c:94
+TEST 17: OK: Expected signal at tests/builtin/strcat.c:95
 strncat: source string string unallocated
-TEST 18: OK: Expected signal at tests/builtin/strcat.c:95
+TEST 18: OK: Expected signal at tests/builtin/strcat.c:96
 strcat: destination string string is not writable
-TEST 19: OK: Expected signal at tests/builtin/strcat.c:96
+TEST 19: OK: Expected signal at tests/builtin/strcat.c:97
 strcat: overlapping memory areas
-TEST 20: OK: Expected signal at tests/builtin/strcat.c:98
+TEST 20: OK: Expected signal at tests/builtin/strcat.c:99
 strncat: insufficient space in destination string, available: 6 bytes, requires at least 7 bytes
-TEST 21: OK: Expected signal at tests/builtin/strcat.c:99
+TEST 21: OK: Expected signal at tests/builtin/strcat.c:100
 strcat: overlapping memory areas
-TEST 22: OK: Expected signal at tests/builtin/strcat.c:100
+TEST 22: OK: Expected signal at tests/builtin/strcat.c:101
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
index a0ee038cc74acef95d0700b3fd7f0302ba180afe..2644fbaf96fa398d23a58dc7ae336b019cd6283e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
@@ -32,16 +32,16 @@ void simple_loop(void)
 
 void nested_loops(void)
 {
-  int t[10][15];
+  int t[4][8];
   int i = 0;
   {
     int __gen_e_acsl_and;
-    if (0 <= i) __gen_e_acsl_and = i <= 10; else __gen_e_acsl_and = 0;
+    if (0 <= i) __gen_e_acsl_and = i <= 4; else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,1,"Invariant","nested_loops",
-                    "0 <= i <= 10","tests/constructs/loop.i",15);
+                    "0 <= i <= 4","tests/constructs/loop.i",15);
   }
-  /*@ loop invariant 0 ≤ i ≤ 10; */
-  while (i < 10) {
+  /*@ loop invariant 0 ≤ i ≤ 4; */
+  while (i < 4) {
     {
       int j = 0;
       {
@@ -56,14 +56,14 @@ void nested_loops(void)
           __gen_e_acsl_l = 0;
           while (1) {
             if (__gen_e_acsl_l < j) ; else break;
-            __e_acsl_assert(__gen_e_acsl_l < 15,1,"RTE","nested_loops",
-                            "index_bound: __gen_e_acsl_l < 15",
+            __e_acsl_assert(__gen_e_acsl_l < 8,1,"RTE","nested_loops",
+                            "index_bound: __gen_e_acsl_l < 8",
                             "tests/constructs/loop.i",19);
             __e_acsl_assert(0 <= __gen_e_acsl_l,1,"RTE","nested_loops",
                             "index_bound: 0 <= __gen_e_acsl_l",
                             "tests/constructs/loop.i",19);
-            __e_acsl_assert(__gen_e_acsl_k < 10,1,"RTE","nested_loops",
-                            "index_bound: __gen_e_acsl_k < 10",
+            __e_acsl_assert(__gen_e_acsl_k < 4,1,"RTE","nested_loops",
+                            "index_bound: __gen_e_acsl_k < 4",
                             "tests/constructs/loop.i",19);
             __e_acsl_assert(0 <= __gen_e_acsl_k,1,"RTE","nested_loops",
                             "index_bound: 0 <= __gen_e_acsl_k",
@@ -82,17 +82,16 @@ void nested_loops(void)
         __e_acsl_assert(__gen_e_acsl_forall,1,"Invariant","nested_loops",
                         "\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k * l",
                         "tests/constructs/loop.i",19);
-        if (0 <= j) __gen_e_acsl_and_2 = j <= 15;
-        else __gen_e_acsl_and_2 = 0;
+        if (0 <= j) __gen_e_acsl_and_2 = j <= 8; else __gen_e_acsl_and_2 = 0;
         __e_acsl_assert(__gen_e_acsl_and_2,1,"Invariant","nested_loops",
-                        "0 <= j <= 15","tests/constructs/loop.i",17);
+                        "0 <= j <= 8","tests/constructs/loop.i",17);
       }
-      /*@ loop invariant 0 ≤ j ≤ 15;
+      /*@ loop invariant 0 ≤ j ≤ 8;
           loop invariant
             ∀ ℤ k, ℤ l;
               0 ≤ k < i ∧ 0 ≤ l < j ⇒ t[k][l] ≡ k * l;
       */
-      while (j < 15) {
+      while (j < 8) {
         t[i][j] = i * j;
         {
           int __gen_e_acsl_and_3;
@@ -100,10 +99,10 @@ void nested_loops(void)
           int __gen_e_acsl_k_2;
           int __gen_e_acsl_l_2;
           j ++;
-          if (0 <= j) __gen_e_acsl_and_3 = j <= 15;
+          if (0 <= j) __gen_e_acsl_and_3 = j <= 8;
           else __gen_e_acsl_and_3 = 0;
           __e_acsl_assert(__gen_e_acsl_and_3,1,"Invariant","nested_loops",
-                          "0 <= j <= 15","tests/constructs/loop.i",17);
+                          "0 <= j <= 8","tests/constructs/loop.i",17);
           __gen_e_acsl_forall_2 = 1;
           __gen_e_acsl_k_2 = 0;
           while (1) {
@@ -111,22 +110,18 @@ void nested_loops(void)
             __gen_e_acsl_l_2 = 0;
             while (1) {
               if (__gen_e_acsl_l_2 < j) ; else break;
-              __e_acsl_assert(__gen_e_acsl_l_2 < 15,1,"RTE","nested_loops",
-                              "index_bound: __gen_e_acsl_l_2 < 15",
+              __e_acsl_assert(__gen_e_acsl_l_2 < 8,1,"RTE","nested_loops",
+                              "index_bound: __gen_e_acsl_l_2 < 8",
                               "tests/constructs/loop.i",19);
               __e_acsl_assert(0 <= __gen_e_acsl_l_2,1,"RTE","nested_loops",
                               "index_bound: 0 <= __gen_e_acsl_l_2",
                               "tests/constructs/loop.i",19);
-              __e_acsl_assert(__gen_e_acsl_k_2 < 10,1,"RTE","nested_loops",
-                              "index_bound: __gen_e_acsl_k_2 < 10",
+              __e_acsl_assert(__gen_e_acsl_k_2 < 4,1,"RTE","nested_loops",
+                              "index_bound: __gen_e_acsl_k_2 < 4",
                               "tests/constructs/loop.i",19);
               __e_acsl_assert(0 <= __gen_e_acsl_k_2,1,"RTE","nested_loops",
                               "index_bound: 0 <= __gen_e_acsl_k_2",
                               "tests/constructs/loop.i",19);
-              /*@ assert
-                  Eva: initialization:
-                    \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
-              */
               if ((long)t[__gen_e_acsl_k_2][__gen_e_acsl_l_2] == __gen_e_acsl_k_2 * (long)__gen_e_acsl_l_2) 
                 ;
               else {
@@ -147,9 +142,9 @@ void nested_loops(void)
     {
       int __gen_e_acsl_and_4;
       i ++;
-      if (0 <= i) __gen_e_acsl_and_4 = i <= 10; else __gen_e_acsl_and_4 = 0;
+      if (0 <= i) __gen_e_acsl_and_4 = i <= 4; else __gen_e_acsl_and_4 = 0;
       __e_acsl_assert(__gen_e_acsl_and_4,1,"Invariant","nested_loops",
-                      "0 <= i <= 10","tests/constructs/loop.i",15);
+                      "0 <= i <= 4","tests/constructs/loop.i",15);
     }
   }
   return;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle
index 05abf9e3c2d8b16e05b88e4c79b4069ba0cfe457..86e58d678ea4f7f60b6d4fbc258872a440f47434 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle
@@ -2,8 +2,3 @@
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/constructs/loop.i:19: Warning: 
   loop invariant got status unknown.
-[eva:alarm] tests/constructs/loop.i:19: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/constructs/loop.i:19: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 322f2dc640cdd63ce58f1024bd92056d773102b4..73f57f2afcf7ecd04bba5d39ff6cae5150d6db5a 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -47,5 +47,5 @@
   is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning: 
+[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning: 
   Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 63106e3cbddbc2d928f20e06174ca8c03cc217b7..276ea7da617cea6b2dc54d539f1fd1bb84d094d5 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -252,94 +252,94 @@ void __e_acsl_globals_init(void)
   static char __e_acsl_already_run = 0;
   if (! __e_acsl_already_run) {
     __e_acsl_already_run = 1;
-    __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:46";
+    __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:47";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
-                         sizeof("tests/format/fprintf.c:46"));
+                         sizeof("tests/format/fprintf.c:47"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
-    __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:45";
+    __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:46";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
-                         sizeof("tests/format/fprintf.c:45"));
+                         sizeof("tests/format/fprintf.c:46"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
-    __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:44";
+    __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:45";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
-                         sizeof("tests/format/fprintf.c:44"));
+                         sizeof("tests/format/fprintf.c:45"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
-    __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:43";
+    __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:44";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
-                         sizeof("tests/format/fprintf.c:43"));
+                         sizeof("tests/format/fprintf.c:44"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
-    __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:42";
+    __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:43";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
-                         sizeof("tests/format/fprintf.c:42"));
+                         sizeof("tests/format/fprintf.c:43"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
-    __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:41";
+    __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:42";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
-                         sizeof("tests/format/fprintf.c:41"));
+                         sizeof("tests/format/fprintf.c:42"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
-    __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:38";
+    __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:39";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
-                         sizeof("tests/format/fprintf.c:38"));
+                         sizeof("tests/format/fprintf.c:39"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
-    __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:37";
+    __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:38";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
-                         sizeof("tests/format/fprintf.c:37"));
+                         sizeof("tests/format/fprintf.c:38"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
-    __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:36";
+    __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:37";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
-                         sizeof("tests/format/fprintf.c:36"));
+                         sizeof("tests/format/fprintf.c:37"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
-    __gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:35";
+    __gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:36";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
-                         sizeof("tests/format/fprintf.c:35"));
+                         sizeof("tests/format/fprintf.c:36"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
-    __gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:34";
+    __gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:35";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
-                         sizeof("tests/format/fprintf.c:34"));
+                         sizeof("tests/format/fprintf.c:35"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
-    __gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:28";
+    __gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:29";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
-                         sizeof("tests/format/fprintf.c:28"));
+                         sizeof("tests/format/fprintf.c:29"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
-    __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:27";
+    __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:28";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
-                         sizeof("tests/format/fprintf.c:27"));
+                         sizeof("tests/format/fprintf.c:28"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
-    __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:22";
+    __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:23";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
-                         sizeof("tests/format/fprintf.c:22"));
+                         sizeof("tests/format/fprintf.c:23"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:21";
+    __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:22";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
-                         sizeof("tests/format/fprintf.c:21"));
+                         sizeof("tests/format/fprintf.c:22"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
-    __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:19";
+    __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:20";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
-                         sizeof("tests/format/fprintf.c:19"));
+                         sizeof("tests/format/fprintf.c:20"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
-    __gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:16";
+    __gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:17";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
-                         sizeof("tests/format/fprintf.c:16"));
+                         sizeof("tests/format/fprintf.c:17"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
-    __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:15";
+    __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:16";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
-                         sizeof("tests/format/fprintf.c:15"));
+                         sizeof("tests/format/fprintf.c:16"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
     __gen_e_acsl_literal_string_11 = "foobar %s\n";
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index b5d7a91b2f184f5660294c13d4ac52d3266a371f..6d0f66bf9b26d38f4c81f716ad0438eda4050acf 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -515,7 +515,7 @@ void test_specifier_application(char const *allowed, char const *fmt,
     __e_acsl_assert(__gen_e_acsl_and,1,"Assertion",
                     "test_specifier_application",
                     "alloca_bounds: 0 < sizeof(char) * (int)(len + 1) <= 18446744073709551615",
-                    "tests/format/printf.c",51);
+                    "tests/format/printf.c",54);
   }
   /*@
   assert
@@ -899,784 +899,784 @@ void __e_acsl_globals_init(void)
                          sizeof("uoxX"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
-    __gen_e_acsl_literal_string_337 = "tests/format/printf.c:476";
+    __gen_e_acsl_literal_string_337 = "tests/format/printf.c:479";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_337,
-                         sizeof("tests/format/printf.c:476"));
+                         sizeof("tests/format/printf.c:479"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_337);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_337);
-    __gen_e_acsl_literal_string_335 = "tests/format/printf.c:473";
+    __gen_e_acsl_literal_string_335 = "tests/format/printf.c:476";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_335,
-                         sizeof("tests/format/printf.c:473"));
+                         sizeof("tests/format/printf.c:476"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_335);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_335);
-    __gen_e_acsl_literal_string_333 = "tests/format/printf.c:472";
+    __gen_e_acsl_literal_string_333 = "tests/format/printf.c:475";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_333,
-                         sizeof("tests/format/printf.c:472"));
+                         sizeof("tests/format/printf.c:475"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_333);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_333);
-    __gen_e_acsl_literal_string_332 = "tests/format/printf.c:471";
+    __gen_e_acsl_literal_string_332 = "tests/format/printf.c:474";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_332,
-                         sizeof("tests/format/printf.c:471"));
+                         sizeof("tests/format/printf.c:474"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_332);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_332);
-    __gen_e_acsl_literal_string_330 = "tests/format/printf.c:470";
+    __gen_e_acsl_literal_string_330 = "tests/format/printf.c:473";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_330,
-                         sizeof("tests/format/printf.c:470"));
+                         sizeof("tests/format/printf.c:473"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_330);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_330);
-    __gen_e_acsl_literal_string_328 = "tests/format/printf.c:469";
+    __gen_e_acsl_literal_string_328 = "tests/format/printf.c:472";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_328,
-                         sizeof("tests/format/printf.c:469"));
+                         sizeof("tests/format/printf.c:472"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_328);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_328);
-    __gen_e_acsl_literal_string_326 = "tests/format/printf.c:468";
+    __gen_e_acsl_literal_string_326 = "tests/format/printf.c:471";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_326,
-                         sizeof("tests/format/printf.c:468"));
+                         sizeof("tests/format/printf.c:471"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_326);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_326);
-    __gen_e_acsl_literal_string_324 = "tests/format/printf.c:467";
+    __gen_e_acsl_literal_string_324 = "tests/format/printf.c:470";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_324,
-                         sizeof("tests/format/printf.c:467"));
+                         sizeof("tests/format/printf.c:470"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_324);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_324);
-    __gen_e_acsl_literal_string_322 = "tests/format/printf.c:466";
+    __gen_e_acsl_literal_string_322 = "tests/format/printf.c:469";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_322,
-                         sizeof("tests/format/printf.c:466"));
+                         sizeof("tests/format/printf.c:469"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_322);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_322);
-    __gen_e_acsl_literal_string_320 = "tests/format/printf.c:465";
+    __gen_e_acsl_literal_string_320 = "tests/format/printf.c:468";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_320,
-                         sizeof("tests/format/printf.c:465"));
+                         sizeof("tests/format/printf.c:468"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_320);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_320);
-    __gen_e_acsl_literal_string_318 = "tests/format/printf.c:464";
+    __gen_e_acsl_literal_string_318 = "tests/format/printf.c:467";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_318,
-                         sizeof("tests/format/printf.c:464"));
+                         sizeof("tests/format/printf.c:467"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_318);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_318);
-    __gen_e_acsl_literal_string_316 = "tests/format/printf.c:461";
+    __gen_e_acsl_literal_string_316 = "tests/format/printf.c:464";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_316,
-                         sizeof("tests/format/printf.c:461"));
+                         sizeof("tests/format/printf.c:464"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_316);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_316);
-    __gen_e_acsl_literal_string_315 = "tests/format/printf.c:460";
+    __gen_e_acsl_literal_string_315 = "tests/format/printf.c:463";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_315,
-                         sizeof("tests/format/printf.c:460"));
+                         sizeof("tests/format/printf.c:463"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_315);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_315);
-    __gen_e_acsl_literal_string_314 = "tests/format/printf.c:459";
+    __gen_e_acsl_literal_string_314 = "tests/format/printf.c:462";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_314,
-                         sizeof("tests/format/printf.c:459"));
+                         sizeof("tests/format/printf.c:462"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_314);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_314);
-    __gen_e_acsl_literal_string_313 = "tests/format/printf.c:458";
+    __gen_e_acsl_literal_string_313 = "tests/format/printf.c:461";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_313,
-                         sizeof("tests/format/printf.c:458"));
+                         sizeof("tests/format/printf.c:461"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_313);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_313);
-    __gen_e_acsl_literal_string_311 = "tests/format/printf.c:455";
+    __gen_e_acsl_literal_string_311 = "tests/format/printf.c:458";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_311,
-                         sizeof("tests/format/printf.c:455"));
+                         sizeof("tests/format/printf.c:458"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_311);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_311);
-    __gen_e_acsl_literal_string_310 = "tests/format/printf.c:454";
+    __gen_e_acsl_literal_string_310 = "tests/format/printf.c:457";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_310,
-                         sizeof("tests/format/printf.c:454"));
+                         sizeof("tests/format/printf.c:457"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_310);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_310);
-    __gen_e_acsl_literal_string_309 = "tests/format/printf.c:453";
+    __gen_e_acsl_literal_string_309 = "tests/format/printf.c:456";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_309,
-                         sizeof("tests/format/printf.c:453"));
+                         sizeof("tests/format/printf.c:456"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_309);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_309);
-    __gen_e_acsl_literal_string_307 = "tests/format/printf.c:428";
+    __gen_e_acsl_literal_string_307 = "tests/format/printf.c:431";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_307,
-                         sizeof("tests/format/printf.c:428"));
+                         sizeof("tests/format/printf.c:431"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_307);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_307);
-    __gen_e_acsl_literal_string_305 = "tests/format/printf.c:427";
+    __gen_e_acsl_literal_string_305 = "tests/format/printf.c:430";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_305,
-                         sizeof("tests/format/printf.c:427"));
+                         sizeof("tests/format/printf.c:430"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_305);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_305);
-    __gen_e_acsl_literal_string_303 = "tests/format/printf.c:426";
+    __gen_e_acsl_literal_string_303 = "tests/format/printf.c:429";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_303,
-                         sizeof("tests/format/printf.c:426"));
+                         sizeof("tests/format/printf.c:429"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_303);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_303);
-    __gen_e_acsl_literal_string_301 = "tests/format/printf.c:425";
+    __gen_e_acsl_literal_string_301 = "tests/format/printf.c:428";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_301,
-                         sizeof("tests/format/printf.c:425"));
+                         sizeof("tests/format/printf.c:428"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_301);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_301);
-    __gen_e_acsl_literal_string_299 = "tests/format/printf.c:424";
+    __gen_e_acsl_literal_string_299 = "tests/format/printf.c:427";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_299,
-                         sizeof("tests/format/printf.c:424"));
+                         sizeof("tests/format/printf.c:427"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_299);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_299);
-    __gen_e_acsl_literal_string_297 = "tests/format/printf.c:421";
+    __gen_e_acsl_literal_string_297 = "tests/format/printf.c:424";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_297,
-                         sizeof("tests/format/printf.c:421"));
+                         sizeof("tests/format/printf.c:424"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_297);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_297);
-    __gen_e_acsl_literal_string_296 = "tests/format/printf.c:419";
+    __gen_e_acsl_literal_string_296 = "tests/format/printf.c:422";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_296,
-                         sizeof("tests/format/printf.c:419"));
+                         sizeof("tests/format/printf.c:422"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_296);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_296);
-    __gen_e_acsl_literal_string_295 = "tests/format/printf.c:416";
+    __gen_e_acsl_literal_string_295 = "tests/format/printf.c:419";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_295,
-                         sizeof("tests/format/printf.c:416"));
+                         sizeof("tests/format/printf.c:419"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_295);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_295);
-    __gen_e_acsl_literal_string_294 = "tests/format/printf.c:415";
+    __gen_e_acsl_literal_string_294 = "tests/format/printf.c:418";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_294,
-                         sizeof("tests/format/printf.c:415"));
+                         sizeof("tests/format/printf.c:418"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_294);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_294);
-    __gen_e_acsl_literal_string_293 = "tests/format/printf.c:410";
+    __gen_e_acsl_literal_string_293 = "tests/format/printf.c:413";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_293,
-                         sizeof("tests/format/printf.c:410"));
+                         sizeof("tests/format/printf.c:413"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_293);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_293);
-    __gen_e_acsl_literal_string_292 = "tests/format/printf.c:409";
+    __gen_e_acsl_literal_string_292 = "tests/format/printf.c:412";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_292,
-                         sizeof("tests/format/printf.c:409"));
+                         sizeof("tests/format/printf.c:412"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_292);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_292);
-    __gen_e_acsl_literal_string_291 = "tests/format/printf.c:408";
+    __gen_e_acsl_literal_string_291 = "tests/format/printf.c:411";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_291,
-                         sizeof("tests/format/printf.c:408"));
+                         sizeof("tests/format/printf.c:411"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_291);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_291);
-    __gen_e_acsl_literal_string_290 = "tests/format/printf.c:407";
+    __gen_e_acsl_literal_string_290 = "tests/format/printf.c:410";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_290,
-                         sizeof("tests/format/printf.c:407"));
+                         sizeof("tests/format/printf.c:410"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_290);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_290);
-    __gen_e_acsl_literal_string_288 = "tests/format/printf.c:400";
+    __gen_e_acsl_literal_string_288 = "tests/format/printf.c:403";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_288,
-                         sizeof("tests/format/printf.c:400"));
+                         sizeof("tests/format/printf.c:403"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_288);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_288);
-    __gen_e_acsl_literal_string_287 = "tests/format/printf.c:399";
+    __gen_e_acsl_literal_string_287 = "tests/format/printf.c:402";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_287,
-                         sizeof("tests/format/printf.c:399"));
+                         sizeof("tests/format/printf.c:402"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_287);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_287);
-    __gen_e_acsl_literal_string_285 = "tests/format/printf.c:396";
+    __gen_e_acsl_literal_string_285 = "tests/format/printf.c:399";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_285,
-                         sizeof("tests/format/printf.c:396"));
+                         sizeof("tests/format/printf.c:399"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_285);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_285);
-    __gen_e_acsl_literal_string_284 = "tests/format/printf.c:395";
+    __gen_e_acsl_literal_string_284 = "tests/format/printf.c:398";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_284,
-                         sizeof("tests/format/printf.c:395"));
+                         sizeof("tests/format/printf.c:398"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_284);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_284);
-    __gen_e_acsl_literal_string_283 = "tests/format/printf.c:394";
+    __gen_e_acsl_literal_string_283 = "tests/format/printf.c:397";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_283,
-                         sizeof("tests/format/printf.c:394"));
+                         sizeof("tests/format/printf.c:397"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_283);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_283);
-    __gen_e_acsl_literal_string_282 = "tests/format/printf.c:393";
+    __gen_e_acsl_literal_string_282 = "tests/format/printf.c:396";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_282,
-                         sizeof("tests/format/printf.c:393"));
+                         sizeof("tests/format/printf.c:396"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_282);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_282);
-    __gen_e_acsl_literal_string_281 = "tests/format/printf.c:392";
+    __gen_e_acsl_literal_string_281 = "tests/format/printf.c:395";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_281,
-                         sizeof("tests/format/printf.c:392"));
+                         sizeof("tests/format/printf.c:395"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_281);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_281);
-    __gen_e_acsl_literal_string_280 = "tests/format/printf.c:391";
+    __gen_e_acsl_literal_string_280 = "tests/format/printf.c:394";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_280,
-                         sizeof("tests/format/printf.c:391"));
+                         sizeof("tests/format/printf.c:394"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_280);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_280);
-    __gen_e_acsl_literal_string_279 = "tests/format/printf.c:390";
+    __gen_e_acsl_literal_string_279 = "tests/format/printf.c:393";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_279,
-                         sizeof("tests/format/printf.c:390"));
+                         sizeof("tests/format/printf.c:393"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_279);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_279);
-    __gen_e_acsl_literal_string_277 = "tests/format/printf.c:387";
+    __gen_e_acsl_literal_string_277 = "tests/format/printf.c:390";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_277,
-                         sizeof("tests/format/printf.c:387"));
+                         sizeof("tests/format/printf.c:390"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_277);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_277);
-    __gen_e_acsl_literal_string_276 = "tests/format/printf.c:386";
+    __gen_e_acsl_literal_string_276 = "tests/format/printf.c:389";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_276,
-                         sizeof("tests/format/printf.c:386"));
+                         sizeof("tests/format/printf.c:389"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_276);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_276);
-    __gen_e_acsl_literal_string_275 = "tests/format/printf.c:385";
+    __gen_e_acsl_literal_string_275 = "tests/format/printf.c:388";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_275,
-                         sizeof("tests/format/printf.c:385"));
+                         sizeof("tests/format/printf.c:388"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_275);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_275);
-    __gen_e_acsl_literal_string_273 = "tests/format/printf.c:384";
+    __gen_e_acsl_literal_string_273 = "tests/format/printf.c:387";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_273,
-                         sizeof("tests/format/printf.c:384"));
+                         sizeof("tests/format/printf.c:387"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_273);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_273);
-    __gen_e_acsl_literal_string_271 = "tests/format/printf.c:383";
+    __gen_e_acsl_literal_string_271 = "tests/format/printf.c:386";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_271,
-                         sizeof("tests/format/printf.c:383"));
+                         sizeof("tests/format/printf.c:386"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_271);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_271);
-    __gen_e_acsl_literal_string_270 = "tests/format/printf.c:382";
+    __gen_e_acsl_literal_string_270 = "tests/format/printf.c:385";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_270,
-                         sizeof("tests/format/printf.c:382"));
+                         sizeof("tests/format/printf.c:385"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_270);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_270);
-    __gen_e_acsl_literal_string_269 = "tests/format/printf.c:381";
+    __gen_e_acsl_literal_string_269 = "tests/format/printf.c:384";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_269,
-                         sizeof("tests/format/printf.c:381"));
+                         sizeof("tests/format/printf.c:384"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_269);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_269);
-    __gen_e_acsl_literal_string_267 = "tests/format/printf.c:380";
+    __gen_e_acsl_literal_string_267 = "tests/format/printf.c:383";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_267,
-                         sizeof("tests/format/printf.c:380"));
+                         sizeof("tests/format/printf.c:383"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_267);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_267);
-    __gen_e_acsl_literal_string_265 = "tests/format/printf.c:379";
+    __gen_e_acsl_literal_string_265 = "tests/format/printf.c:382";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_265,
-                         sizeof("tests/format/printf.c:379"));
+                         sizeof("tests/format/printf.c:382"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_265);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_265);
-    __gen_e_acsl_literal_string_264 = "tests/format/printf.c:378";
+    __gen_e_acsl_literal_string_264 = "tests/format/printf.c:381";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_264,
-                         sizeof("tests/format/printf.c:378"));
+                         sizeof("tests/format/printf.c:381"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_264);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_264);
-    __gen_e_acsl_literal_string_263 = "tests/format/printf.c:377";
+    __gen_e_acsl_literal_string_263 = "tests/format/printf.c:380";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_263,
-                         sizeof("tests/format/printf.c:377"));
+                         sizeof("tests/format/printf.c:380"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_263);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_263);
-    __gen_e_acsl_literal_string_261 = "tests/format/printf.c:376";
+    __gen_e_acsl_literal_string_261 = "tests/format/printf.c:379";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_261,
-                         sizeof("tests/format/printf.c:376"));
+                         sizeof("tests/format/printf.c:379"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_261);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_261);
-    __gen_e_acsl_literal_string_259 = "tests/format/printf.c:375";
+    __gen_e_acsl_literal_string_259 = "tests/format/printf.c:378";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_259,
-                         sizeof("tests/format/printf.c:375"));
+                         sizeof("tests/format/printf.c:378"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_259);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_259);
-    __gen_e_acsl_literal_string_258 = "tests/format/printf.c:374";
+    __gen_e_acsl_literal_string_258 = "tests/format/printf.c:377";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_258,
-                         sizeof("tests/format/printf.c:374"));
+                         sizeof("tests/format/printf.c:377"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_258);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_258);
-    __gen_e_acsl_literal_string_257 = "tests/format/printf.c:373";
+    __gen_e_acsl_literal_string_257 = "tests/format/printf.c:376";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_257,
-                         sizeof("tests/format/printf.c:373"));
+                         sizeof("tests/format/printf.c:376"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_257);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_257);
-    __gen_e_acsl_literal_string_255 = "tests/format/printf.c:372";
+    __gen_e_acsl_literal_string_255 = "tests/format/printf.c:375";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_255,
-                         sizeof("tests/format/printf.c:372"));
+                         sizeof("tests/format/printf.c:375"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_255);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_255);
-    __gen_e_acsl_literal_string_253 = "tests/format/printf.c:369";
+    __gen_e_acsl_literal_string_253 = "tests/format/printf.c:372";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_253,
-                         sizeof("tests/format/printf.c:369"));
+                         sizeof("tests/format/printf.c:372"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_253);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_253);
-    __gen_e_acsl_literal_string_252 = "tests/format/printf.c:368";
+    __gen_e_acsl_literal_string_252 = "tests/format/printf.c:371";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_252,
-                         sizeof("tests/format/printf.c:368"));
+                         sizeof("tests/format/printf.c:371"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_252);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_252);
-    __gen_e_acsl_literal_string_251 = "tests/format/printf.c:367";
+    __gen_e_acsl_literal_string_251 = "tests/format/printf.c:370";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_251,
-                         sizeof("tests/format/printf.c:367"));
+                         sizeof("tests/format/printf.c:370"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_251);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_251);
-    __gen_e_acsl_literal_string_249 = "tests/format/printf.c:366";
+    __gen_e_acsl_literal_string_249 = "tests/format/printf.c:369";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_249,
-                         sizeof("tests/format/printf.c:366"));
+                         sizeof("tests/format/printf.c:369"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_249);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_249);
-    __gen_e_acsl_literal_string_247 = "tests/format/printf.c:365";
+    __gen_e_acsl_literal_string_247 = "tests/format/printf.c:368";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_247,
-                         sizeof("tests/format/printf.c:365"));
+                         sizeof("tests/format/printf.c:368"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_247);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_247);
-    __gen_e_acsl_literal_string_246 = "tests/format/printf.c:364";
+    __gen_e_acsl_literal_string_246 = "tests/format/printf.c:367";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_246,
-                         sizeof("tests/format/printf.c:364"));
+                         sizeof("tests/format/printf.c:367"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_246);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_246);
-    __gen_e_acsl_literal_string_245 = "tests/format/printf.c:363";
+    __gen_e_acsl_literal_string_245 = "tests/format/printf.c:366";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_245,
-                         sizeof("tests/format/printf.c:363"));
+                         sizeof("tests/format/printf.c:366"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_245);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_245);
-    __gen_e_acsl_literal_string_243 = "tests/format/printf.c:362";
+    __gen_e_acsl_literal_string_243 = "tests/format/printf.c:365";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_243,
-                         sizeof("tests/format/printf.c:362"));
+                         sizeof("tests/format/printf.c:365"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_243);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_243);
-    __gen_e_acsl_literal_string_241 = "tests/format/printf.c:361";
+    __gen_e_acsl_literal_string_241 = "tests/format/printf.c:364";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_241,
-                         sizeof("tests/format/printf.c:361"));
+                         sizeof("tests/format/printf.c:364"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_241);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_241);
-    __gen_e_acsl_literal_string_240 = "tests/format/printf.c:360";
+    __gen_e_acsl_literal_string_240 = "tests/format/printf.c:363";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_240,
-                         sizeof("tests/format/printf.c:360"));
+                         sizeof("tests/format/printf.c:363"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_240);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_240);
-    __gen_e_acsl_literal_string_239 = "tests/format/printf.c:359";
+    __gen_e_acsl_literal_string_239 = "tests/format/printf.c:362";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_239,
-                         sizeof("tests/format/printf.c:359"));
+                         sizeof("tests/format/printf.c:362"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_239);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_239);
-    __gen_e_acsl_literal_string_237 = "tests/format/printf.c:358";
+    __gen_e_acsl_literal_string_237 = "tests/format/printf.c:361";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_237,
-                         sizeof("tests/format/printf.c:358"));
+                         sizeof("tests/format/printf.c:361"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_237);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_237);
-    __gen_e_acsl_literal_string_235 = "tests/format/printf.c:357";
+    __gen_e_acsl_literal_string_235 = "tests/format/printf.c:360";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_235,
-                         sizeof("tests/format/printf.c:357"));
+                         sizeof("tests/format/printf.c:360"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_235);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_235);
-    __gen_e_acsl_literal_string_234 = "tests/format/printf.c:356";
+    __gen_e_acsl_literal_string_234 = "tests/format/printf.c:359";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_234,
-                         sizeof("tests/format/printf.c:356"));
+                         sizeof("tests/format/printf.c:359"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_234);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_234);
-    __gen_e_acsl_literal_string_233 = "tests/format/printf.c:355";
+    __gen_e_acsl_literal_string_233 = "tests/format/printf.c:358";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_233,
-                         sizeof("tests/format/printf.c:355"));
+                         sizeof("tests/format/printf.c:358"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_233);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_233);
-    __gen_e_acsl_literal_string_231 = "tests/format/printf.c:354";
+    __gen_e_acsl_literal_string_231 = "tests/format/printf.c:357";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_231,
-                         sizeof("tests/format/printf.c:354"));
+                         sizeof("tests/format/printf.c:357"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_231);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_231);
-    __gen_e_acsl_literal_string_226 = "tests/format/printf.c:350";
+    __gen_e_acsl_literal_string_226 = "tests/format/printf.c:353";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_226,
-                         sizeof("tests/format/printf.c:350"));
+                         sizeof("tests/format/printf.c:353"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_226);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_226);
-    __gen_e_acsl_literal_string_221 = "tests/format/printf.c:348";
+    __gen_e_acsl_literal_string_221 = "tests/format/printf.c:351";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_221,
-                         sizeof("tests/format/printf.c:348"));
+                         sizeof("tests/format/printf.c:351"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_221);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_221);
-    __gen_e_acsl_literal_string_216 = "tests/format/printf.c:347";
+    __gen_e_acsl_literal_string_216 = "tests/format/printf.c:350";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_216,
-                         sizeof("tests/format/printf.c:347"));
+                         sizeof("tests/format/printf.c:350"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_216);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_216);
-    __gen_e_acsl_literal_string_211 = "tests/format/printf.c:346";
+    __gen_e_acsl_literal_string_211 = "tests/format/printf.c:349";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_211,
-                         sizeof("tests/format/printf.c:346"));
+                         sizeof("tests/format/printf.c:349"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_211);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_211);
-    __gen_e_acsl_literal_string_206 = "tests/format/printf.c:344";
+    __gen_e_acsl_literal_string_206 = "tests/format/printf.c:347";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_206,
-                         sizeof("tests/format/printf.c:344"));
+                         sizeof("tests/format/printf.c:347"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_206);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_206);
-    __gen_e_acsl_literal_string_201 = "tests/format/printf.c:342";
+    __gen_e_acsl_literal_string_201 = "tests/format/printf.c:345";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_201,
-                         sizeof("tests/format/printf.c:342"));
+                         sizeof("tests/format/printf.c:345"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_201);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_201);
-    __gen_e_acsl_literal_string_196 = "tests/format/printf.c:341";
+    __gen_e_acsl_literal_string_196 = "tests/format/printf.c:344";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_196,
-                         sizeof("tests/format/printf.c:341"));
+                         sizeof("tests/format/printf.c:344"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_196);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_196);
-    __gen_e_acsl_literal_string_194 = "tests/format/printf.c:338";
+    __gen_e_acsl_literal_string_194 = "tests/format/printf.c:341";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_194,
-                         sizeof("tests/format/printf.c:338"));
+                         sizeof("tests/format/printf.c:341"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_194);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_194);
-    __gen_e_acsl_literal_string_193 = "tests/format/printf.c:337";
+    __gen_e_acsl_literal_string_193 = "tests/format/printf.c:340";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_193,
-                         sizeof("tests/format/printf.c:337"));
+                         sizeof("tests/format/printf.c:340"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_193);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_193);
-    __gen_e_acsl_literal_string_192 = "tests/format/printf.c:336";
+    __gen_e_acsl_literal_string_192 = "tests/format/printf.c:339";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_192,
-                         sizeof("tests/format/printf.c:336"));
+                         sizeof("tests/format/printf.c:339"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_192);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_192);
-    __gen_e_acsl_literal_string_191 = "tests/format/printf.c:335";
+    __gen_e_acsl_literal_string_191 = "tests/format/printf.c:338";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_191,
-                         sizeof("tests/format/printf.c:335"));
+                         sizeof("tests/format/printf.c:338"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_191);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_191);
-    __gen_e_acsl_literal_string_190 = "tests/format/printf.c:334";
+    __gen_e_acsl_literal_string_190 = "tests/format/printf.c:337";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_190,
-                         sizeof("tests/format/printf.c:334"));
+                         sizeof("tests/format/printf.c:337"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_190);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_190);
-    __gen_e_acsl_literal_string_186 = "tests/format/printf.c:333";
+    __gen_e_acsl_literal_string_186 = "tests/format/printf.c:336";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_186,
-                         sizeof("tests/format/printf.c:333"));
+                         sizeof("tests/format/printf.c:336"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_186);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_186);
-    __gen_e_acsl_literal_string_183 = "tests/format/printf.c:330";
+    __gen_e_acsl_literal_string_183 = "tests/format/printf.c:333";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_183,
-                         sizeof("tests/format/printf.c:330"));
+                         sizeof("tests/format/printf.c:333"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_183);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_183);
-    __gen_e_acsl_literal_string_180 = "tests/format/printf.c:326";
+    __gen_e_acsl_literal_string_180 = "tests/format/printf.c:329";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_180,
-                         sizeof("tests/format/printf.c:326"));
+                         sizeof("tests/format/printf.c:329"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_180);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_180);
-    __gen_e_acsl_literal_string_177 = "tests/format/printf.c:324";
+    __gen_e_acsl_literal_string_177 = "tests/format/printf.c:327";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_177,
-                         sizeof("tests/format/printf.c:324"));
+                         sizeof("tests/format/printf.c:327"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_177);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_177);
-    __gen_e_acsl_literal_string_174 = "tests/format/printf.c:323";
+    __gen_e_acsl_literal_string_174 = "tests/format/printf.c:326";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_174,
-                         sizeof("tests/format/printf.c:323"));
+                         sizeof("tests/format/printf.c:326"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_174);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_174);
-    __gen_e_acsl_literal_string_172 = "tests/format/printf.c:322";
+    __gen_e_acsl_literal_string_172 = "tests/format/printf.c:325";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_172,
-                         sizeof("tests/format/printf.c:322"));
+                         sizeof("tests/format/printf.c:325"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_172);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_172);
-    __gen_e_acsl_literal_string_170 = "tests/format/printf.c:321";
+    __gen_e_acsl_literal_string_170 = "tests/format/printf.c:324";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_170,
-                         sizeof("tests/format/printf.c:321"));
+                         sizeof("tests/format/printf.c:324"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_170);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_170);
-    __gen_e_acsl_literal_string_168 = "tests/format/printf.c:318";
+    __gen_e_acsl_literal_string_168 = "tests/format/printf.c:321";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_168,
-                         sizeof("tests/format/printf.c:318"));
+                         sizeof("tests/format/printf.c:321"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_168);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_168);
-    __gen_e_acsl_literal_string_167 = "tests/format/printf.c:317";
+    __gen_e_acsl_literal_string_167 = "tests/format/printf.c:320";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_167,
-                         sizeof("tests/format/printf.c:317"));
+                         sizeof("tests/format/printf.c:320"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_167);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_167);
-    __gen_e_acsl_literal_string_166 = "tests/format/printf.c:316";
+    __gen_e_acsl_literal_string_166 = "tests/format/printf.c:319";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_166,
-                         sizeof("tests/format/printf.c:316"));
+                         sizeof("tests/format/printf.c:319"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_166);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_166);
-    __gen_e_acsl_literal_string_165 = "tests/format/printf.c:315";
+    __gen_e_acsl_literal_string_165 = "tests/format/printf.c:318";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_165,
-                         sizeof("tests/format/printf.c:315"));
+                         sizeof("tests/format/printf.c:318"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_165);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_165);
-    __gen_e_acsl_literal_string_164 = "tests/format/printf.c:314";
+    __gen_e_acsl_literal_string_164 = "tests/format/printf.c:317";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_164,
-                         sizeof("tests/format/printf.c:314"));
+                         sizeof("tests/format/printf.c:317"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_164);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_164);
-    __gen_e_acsl_literal_string_163 = "tests/format/printf.c:313";
+    __gen_e_acsl_literal_string_163 = "tests/format/printf.c:316";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_163,
-                         sizeof("tests/format/printf.c:313"));
+                         sizeof("tests/format/printf.c:316"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_163);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_163);
-    __gen_e_acsl_literal_string_161 = "tests/format/printf.c:312";
+    __gen_e_acsl_literal_string_161 = "tests/format/printf.c:315";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_161,
-                         sizeof("tests/format/printf.c:312"));
+                         sizeof("tests/format/printf.c:315"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_161);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_161);
-    __gen_e_acsl_literal_string_159 = "tests/format/printf.c:309";
+    __gen_e_acsl_literal_string_159 = "tests/format/printf.c:312";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_159,
-                         sizeof("tests/format/printf.c:309"));
+                         sizeof("tests/format/printf.c:312"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_159);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_159);
-    __gen_e_acsl_literal_string_157 = "tests/format/printf.c:308";
+    __gen_e_acsl_literal_string_157 = "tests/format/printf.c:311";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_157,
-                         sizeof("tests/format/printf.c:308"));
+                         sizeof("tests/format/printf.c:311"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_157);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_157);
-    __gen_e_acsl_literal_string_155 = "tests/format/printf.c:307";
+    __gen_e_acsl_literal_string_155 = "tests/format/printf.c:310";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_155,
-                         sizeof("tests/format/printf.c:307"));
+                         sizeof("tests/format/printf.c:310"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_155);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_155);
-    __gen_e_acsl_literal_string_152 = "tests/format/printf.c:303";
+    __gen_e_acsl_literal_string_152 = "tests/format/printf.c:306";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_152,
-                         sizeof("tests/format/printf.c:303"));
+                         sizeof("tests/format/printf.c:306"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_152);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_152);
-    __gen_e_acsl_literal_string_149 = "tests/format/printf.c:302";
+    __gen_e_acsl_literal_string_149 = "tests/format/printf.c:305";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_149,
-                         sizeof("tests/format/printf.c:302"));
+                         sizeof("tests/format/printf.c:305"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_149);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_149);
-    __gen_e_acsl_literal_string_146 = "tests/format/printf.c:301";
+    __gen_e_acsl_literal_string_146 = "tests/format/printf.c:304";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_146,
-                         sizeof("tests/format/printf.c:301"));
+                         sizeof("tests/format/printf.c:304"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_146);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_146);
-    __gen_e_acsl_literal_string_143 = "tests/format/printf.c:300";
+    __gen_e_acsl_literal_string_143 = "tests/format/printf.c:303";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_143,
-                         sizeof("tests/format/printf.c:300"));
+                         sizeof("tests/format/printf.c:303"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_143);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_143);
-    __gen_e_acsl_literal_string_139 = "tests/format/printf.c:299";
+    __gen_e_acsl_literal_string_139 = "tests/format/printf.c:302";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_139,
-                         sizeof("tests/format/printf.c:299"));
+                         sizeof("tests/format/printf.c:302"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_139);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_139);
-    __gen_e_acsl_literal_string_138 = "tests/format/printf.c:296";
+    __gen_e_acsl_literal_string_138 = "tests/format/printf.c:299";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_138,
-                         sizeof("tests/format/printf.c:296"));
+                         sizeof("tests/format/printf.c:299"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_138);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_138);
-    __gen_e_acsl_literal_string_135 = "tests/format/printf.c:295";
+    __gen_e_acsl_literal_string_135 = "tests/format/printf.c:298";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_135,
-                         sizeof("tests/format/printf.c:295"));
+                         sizeof("tests/format/printf.c:298"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_135);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_135);
-    __gen_e_acsl_literal_string_133 = "tests/format/printf.c:290";
+    __gen_e_acsl_literal_string_133 = "tests/format/printf.c:293";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_133,
-                         sizeof("tests/format/printf.c:290"));
+                         sizeof("tests/format/printf.c:293"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_133);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_133);
-    __gen_e_acsl_literal_string_130 = "tests/format/printf.c:289";
+    __gen_e_acsl_literal_string_130 = "tests/format/printf.c:292";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_130,
-                         sizeof("tests/format/printf.c:289"));
+                         sizeof("tests/format/printf.c:292"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_130);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_130);
-    __gen_e_acsl_literal_string_127 = "tests/format/printf.c:287";
+    __gen_e_acsl_literal_string_127 = "tests/format/printf.c:290";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_127,
-                         sizeof("tests/format/printf.c:287"));
+                         sizeof("tests/format/printf.c:290"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_127);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_127);
-    __gen_e_acsl_literal_string_125 = "tests/format/printf.c:282";
+    __gen_e_acsl_literal_string_125 = "tests/format/printf.c:285";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_125,
-                         sizeof("tests/format/printf.c:282"));
+                         sizeof("tests/format/printf.c:285"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_125);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_125);
-    __gen_e_acsl_literal_string_122 = "tests/format/printf.c:281";
+    __gen_e_acsl_literal_string_122 = "tests/format/printf.c:284";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_122,
-                         sizeof("tests/format/printf.c:281"));
+                         sizeof("tests/format/printf.c:284"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_122);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_122);
-    __gen_e_acsl_literal_string_119 = "tests/format/printf.c:277";
+    __gen_e_acsl_literal_string_119 = "tests/format/printf.c:280";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_119,
-                         sizeof("tests/format/printf.c:277"));
+                         sizeof("tests/format/printf.c:280"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_119);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_119);
-    __gen_e_acsl_literal_string_116 = "tests/format/printf.c:272";
+    __gen_e_acsl_literal_string_116 = "tests/format/printf.c:275";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_116,
-                         sizeof("tests/format/printf.c:272"));
+                         sizeof("tests/format/printf.c:275"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_116);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_116);
-    __gen_e_acsl_literal_string_114 = "tests/format/printf.c:269";
+    __gen_e_acsl_literal_string_114 = "tests/format/printf.c:272";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_114,
-                         sizeof("tests/format/printf.c:269"));
+                         sizeof("tests/format/printf.c:272"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_114);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_114);
-    __gen_e_acsl_literal_string_111 = "tests/format/printf.c:268";
+    __gen_e_acsl_literal_string_111 = "tests/format/printf.c:271";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_111,
-                         sizeof("tests/format/printf.c:268"));
+                         sizeof("tests/format/printf.c:271"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_111);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_111);
-    __gen_e_acsl_literal_string_108 = "tests/format/printf.c:267";
+    __gen_e_acsl_literal_string_108 = "tests/format/printf.c:270";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_108,
-                         sizeof("tests/format/printf.c:267"));
+                         sizeof("tests/format/printf.c:270"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_108);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_108);
-    __gen_e_acsl_literal_string_105 = "tests/format/printf.c:266";
+    __gen_e_acsl_literal_string_105 = "tests/format/printf.c:269";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_105,
-                         sizeof("tests/format/printf.c:266"));
+                         sizeof("tests/format/printf.c:269"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_105);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_105);
-    __gen_e_acsl_literal_string_102 = "tests/format/printf.c:263";
+    __gen_e_acsl_literal_string_102 = "tests/format/printf.c:266";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_102,
-                         sizeof("tests/format/printf.c:263"));
+                         sizeof("tests/format/printf.c:266"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_102);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_102);
-    __gen_e_acsl_literal_string_99 = "tests/format/printf.c:262";
+    __gen_e_acsl_literal_string_99 = "tests/format/printf.c:265";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_99,
-                         sizeof("tests/format/printf.c:262"));
+                         sizeof("tests/format/printf.c:265"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_99);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_99);
-    __gen_e_acsl_literal_string_96 = "tests/format/printf.c:261";
+    __gen_e_acsl_literal_string_96 = "tests/format/printf.c:264";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_96,
-                         sizeof("tests/format/printf.c:261"));
+                         sizeof("tests/format/printf.c:264"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_96);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_96);
-    __gen_e_acsl_literal_string_94 = "tests/format/printf.c:257";
+    __gen_e_acsl_literal_string_94 = "tests/format/printf.c:260";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_94,
-                         sizeof("tests/format/printf.c:257"));
+                         sizeof("tests/format/printf.c:260"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_94);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_94);
-    __gen_e_acsl_literal_string_92 = "tests/format/printf.c:254";
+    __gen_e_acsl_literal_string_92 = "tests/format/printf.c:257";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_92,
-                         sizeof("tests/format/printf.c:254"));
+                         sizeof("tests/format/printf.c:257"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_92);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_92);
-    __gen_e_acsl_literal_string_89 = "tests/format/printf.c:252";
+    __gen_e_acsl_literal_string_89 = "tests/format/printf.c:255";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_89,
-                         sizeof("tests/format/printf.c:252"));
+                         sizeof("tests/format/printf.c:255"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_89);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_89);
-    __gen_e_acsl_literal_string_86 = "tests/format/printf.c:251";
+    __gen_e_acsl_literal_string_86 = "tests/format/printf.c:254";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_86,
-                         sizeof("tests/format/printf.c:251"));
+                         sizeof("tests/format/printf.c:254"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_86);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_86);
-    __gen_e_acsl_literal_string_83 = "tests/format/printf.c:250";
+    __gen_e_acsl_literal_string_83 = "tests/format/printf.c:253";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_83,
-                         sizeof("tests/format/printf.c:250"));
+                         sizeof("tests/format/printf.c:253"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_83);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_83);
-    __gen_e_acsl_literal_string_80 = "tests/format/printf.c:249";
+    __gen_e_acsl_literal_string_80 = "tests/format/printf.c:252";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_80,
-                         sizeof("tests/format/printf.c:249"));
+                         sizeof("tests/format/printf.c:252"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_80);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_80);
-    __gen_e_acsl_literal_string_78 = "tests/format/printf.c:247";
+    __gen_e_acsl_literal_string_78 = "tests/format/printf.c:250";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_78,
-                         sizeof("tests/format/printf.c:247"));
+                         sizeof("tests/format/printf.c:250"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_78);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_78);
-    __gen_e_acsl_literal_string_75 = "tests/format/printf.c:246";
+    __gen_e_acsl_literal_string_75 = "tests/format/printf.c:249";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_75,
-                         sizeof("tests/format/printf.c:246"));
+                         sizeof("tests/format/printf.c:249"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_75);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_75);
-    __gen_e_acsl_literal_string_72 = "tests/format/printf.c:245";
+    __gen_e_acsl_literal_string_72 = "tests/format/printf.c:248";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_72,
-                         sizeof("tests/format/printf.c:245"));
+                         sizeof("tests/format/printf.c:248"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_72);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_72);
-    __gen_e_acsl_literal_string_68 = "tests/format/printf.c:244";
+    __gen_e_acsl_literal_string_68 = "tests/format/printf.c:247";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_68,
-                         sizeof("tests/format/printf.c:244"));
+                         sizeof("tests/format/printf.c:247"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_68);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_68);
-    __gen_e_acsl_literal_string_66 = "tests/format/printf.c:241";
+    __gen_e_acsl_literal_string_66 = "tests/format/printf.c:244";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_66,
-                         sizeof("tests/format/printf.c:241"));
+                         sizeof("tests/format/printf.c:244"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_66);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_66);
-    __gen_e_acsl_literal_string_63 = "tests/format/printf.c:240";
+    __gen_e_acsl_literal_string_63 = "tests/format/printf.c:243";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_63,
-                         sizeof("tests/format/printf.c:240"));
+                         sizeof("tests/format/printf.c:243"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_63);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_63);
-    __gen_e_acsl_literal_string_60 = "tests/format/printf.c:239";
+    __gen_e_acsl_literal_string_60 = "tests/format/printf.c:242";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_60,
-                         sizeof("tests/format/printf.c:239"));
+                         sizeof("tests/format/printf.c:242"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_60);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_60);
-    __gen_e_acsl_literal_string_57 = "tests/format/printf.c:238";
+    __gen_e_acsl_literal_string_57 = "tests/format/printf.c:241";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_57,
-                         sizeof("tests/format/printf.c:238"));
+                         sizeof("tests/format/printf.c:241"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_57);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_57);
-    __gen_e_acsl_literal_string_55 = "tests/format/printf.c:235";
+    __gen_e_acsl_literal_string_55 = "tests/format/printf.c:238";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_55,
-                         sizeof("tests/format/printf.c:235"));
+                         sizeof("tests/format/printf.c:238"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_55);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_55);
-    __gen_e_acsl_literal_string_52 = "tests/format/printf.c:234";
+    __gen_e_acsl_literal_string_52 = "tests/format/printf.c:237";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_52,
-                         sizeof("tests/format/printf.c:234"));
+                         sizeof("tests/format/printf.c:237"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_52);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_52);
-    __gen_e_acsl_literal_string_49 = "tests/format/printf.c:233";
+    __gen_e_acsl_literal_string_49 = "tests/format/printf.c:236";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_49,
-                         sizeof("tests/format/printf.c:233"));
+                         sizeof("tests/format/printf.c:236"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_49);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_49);
-    __gen_e_acsl_literal_string_45 = "tests/format/printf.c:232";
+    __gen_e_acsl_literal_string_45 = "tests/format/printf.c:235";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_45,
-                         sizeof("tests/format/printf.c:232"));
+                         sizeof("tests/format/printf.c:235"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_45);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_45);
-    __gen_e_acsl_literal_string_44 = "tests/format/printf.c:226";
+    __gen_e_acsl_literal_string_44 = "tests/format/printf.c:229";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_44,
-                         sizeof("tests/format/printf.c:226"));
+                         sizeof("tests/format/printf.c:229"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_44);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_44);
-    __gen_e_acsl_literal_string_42 = "tests/format/printf.c:225";
+    __gen_e_acsl_literal_string_42 = "tests/format/printf.c:228";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_42,
-                         sizeof("tests/format/printf.c:225"));
+                         sizeof("tests/format/printf.c:228"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_42);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_42);
-    __gen_e_acsl_literal_string_40 = "tests/format/printf.c:224";
+    __gen_e_acsl_literal_string_40 = "tests/format/printf.c:227";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_40,
-                         sizeof("tests/format/printf.c:224"));
+                         sizeof("tests/format/printf.c:227"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_40);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_40);
-    __gen_e_acsl_literal_string_36 = "tests/format/printf.c:218";
+    __gen_e_acsl_literal_string_36 = "tests/format/printf.c:221";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_36,
-                         sizeof("tests/format/printf.c:218"));
+                         sizeof("tests/format/printf.c:221"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_36);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_36);
-    __gen_e_acsl_literal_string_33 = "tests/format/printf.c:215";
+    __gen_e_acsl_literal_string_33 = "tests/format/printf.c:218";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_33,
-                         sizeof("tests/format/printf.c:215"));
+                         sizeof("tests/format/printf.c:218"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_33);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_33);
-    __gen_e_acsl_literal_string_30 = "tests/format/printf.c:209";
+    __gen_e_acsl_literal_string_30 = "tests/format/printf.c:212";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
-                         sizeof("tests/format/printf.c:209"));
+                         sizeof("tests/format/printf.c:212"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
-    __gen_e_acsl_literal_string_29 = "tests/format/printf.c:206";
+    __gen_e_acsl_literal_string_29 = "tests/format/printf.c:209";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
-                         sizeof("tests/format/printf.c:206"));
+                         sizeof("tests/format/printf.c:209"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
-    __gen_e_acsl_literal_string_27 = "tests/format/printf.c:204";
+    __gen_e_acsl_literal_string_27 = "tests/format/printf.c:207";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
-                         sizeof("tests/format/printf.c:204"));
+                         sizeof("tests/format/printf.c:207"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
-    __gen_e_acsl_literal_string_25 = "tests/format/printf.c:201";
+    __gen_e_acsl_literal_string_25 = "tests/format/printf.c:204";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
-                         sizeof("tests/format/printf.c:201"));
+                         sizeof("tests/format/printf.c:204"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
-    __gen_e_acsl_literal_string_23 = "tests/format/printf.c:199";
+    __gen_e_acsl_literal_string_23 = "tests/format/printf.c:202";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
-                         sizeof("tests/format/printf.c:199"));
+                         sizeof("tests/format/printf.c:202"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
-    __gen_e_acsl_literal_string_21 = "tests/format/printf.c:197";
+    __gen_e_acsl_literal_string_21 = "tests/format/printf.c:200";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
-                         sizeof("tests/format/printf.c:197"));
+                         sizeof("tests/format/printf.c:200"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
-    __gen_e_acsl_literal_string_19 = "tests/format/printf.c:194";
+    __gen_e_acsl_literal_string_19 = "tests/format/printf.c:197";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
-                         sizeof("tests/format/printf.c:194"));
+                         sizeof("tests/format/printf.c:197"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
-    __gen_e_acsl_literal_string_18 = "tests/format/printf.c:189";
+    __gen_e_acsl_literal_string_18 = "tests/format/printf.c:192";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
-                         sizeof("tests/format/printf.c:189"));
+                         sizeof("tests/format/printf.c:192"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
-    __gen_e_acsl_literal_string_16 = "tests/format/printf.c:186";
+    __gen_e_acsl_literal_string_16 = "tests/format/printf.c:189";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
-                         sizeof("tests/format/printf.c:186"));
+                         sizeof("tests/format/printf.c:189"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
-    __gen_e_acsl_literal_string_14 = "tests/format/printf.c:183";
+    __gen_e_acsl_literal_string_14 = "tests/format/printf.c:186";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
-                         sizeof("tests/format/printf.c:183"));
+                         sizeof("tests/format/printf.c:186"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
-    __gen_e_acsl_literal_string_12 = "tests/format/printf.c:180";
+    __gen_e_acsl_literal_string_12 = "tests/format/printf.c:183";
     __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
-                         sizeof("tests/format/printf.c:180"));
+                         sizeof("tests/format/printf.c:183"));
     __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
     __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
     __gen_e_acsl_literal_string_35 = "oxXaAeEfFgG";
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 8ac28fcd5d621500357d806e74bc8f559e6c244c..494c722d019b3dd212d80ffa2662693fd07d5244 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -1,4 +1,4 @@
-[kernel:parser:decimal-float] tests/format/printf.c:89: Warning: 
+[kernel:parser:decimal-float] tests/format/printf.c:92: Warning: 
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [e-acsl] beginning translation.
@@ -101,5 +101,5 @@
   is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/format/printf.c:180: Warning: 
+[kernel:annot:missing-spec] tests/format/printf.c:183: Warning: 
   Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
index fe875c9a1ac68e47475516ef0bff5790bebf077b..0c12cd746446f71822a636b6555149d9e02b32c3 100644
--- a/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/sprintf.res.oracle
@@ -3,18 +3,25 @@
 [kernel:annot:missing-spec] tests/format/sprintf.c:12: Warning: 
   Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
 [eva:alarm] tests/format/sprintf.c:13: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:13: Warning: assertion got status unknown.
 [eva:alarm] tests/format/sprintf.c:14: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:14: Warning: assertion got status unknown.
 [kernel:annot:missing-spec] tests/format/sprintf.c:20: Warning: 
   Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
 [eva:alarm] tests/format/sprintf.c:21: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:21: Warning: assertion got status unknown.
 [eva:alarm] tests/format/sprintf.c:22: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:22: Warning: assertion got status unknown.
 [eva:alarm] tests/format/sprintf.c:23: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:23: Warning: assertion got status unknown.
 [eva:alarm] tests/format/sprintf.c:30: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:30: Warning: assertion got status unknown.
 [eva:alarm] tests/format/sprintf.c:31: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/format/sprintf.c:31: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
index fe27812ca9504e05f3a4f63bb9275d24d734e2c8..0bbf23ea140d1b32644f3a7749bfb189bdf52cff 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
@@ -1,28 +1,28 @@
-TEST 1: OK: Expected execution at tests/format/fprintf.c:15
+TEST 1: OK: Expected execution at tests/format/fprintf.c:16
 fprintf: attempt to write to an invalid stream
-TEST 2: OK: Expected signal at tests/format/fprintf.c:16
-TEST 3: OK: Expected execution at tests/format/fprintf.c:19
+TEST 2: OK: Expected signal at tests/format/fprintf.c:17
+TEST 3: OK: Expected execution at tests/format/fprintf.c:20
 fprintf: attempt to write to an invalid stream
-TEST 4: OK: Expected signal at tests/format/fprintf.c:21
+TEST 4: OK: Expected signal at tests/format/fprintf.c:22
 fprintf: attempt to write to an invalid stream
-TEST 5: OK: Expected signal at tests/format/fprintf.c:22
-TEST 6: OK: Expected execution at tests/format/fprintf.c:27
+TEST 5: OK: Expected signal at tests/format/fprintf.c:23
+TEST 6: OK: Expected execution at tests/format/fprintf.c:28
 dprintf: attempt to write to a closed file descriptor 3
-TEST 7: OK: Expected signal at tests/format/fprintf.c:28
-TEST 8: OK: Expected execution at tests/format/fprintf.c:34
-TEST 9: OK: Expected execution at tests/format/fprintf.c:35
+TEST 7: OK: Expected signal at tests/format/fprintf.c:29
+TEST 8: OK: Expected execution at tests/format/fprintf.c:35
+TEST 9: OK: Expected execution at tests/format/fprintf.c:36
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 10: OK: Expected signal at tests/format/fprintf.c:36
+TEST 10: OK: Expected signal at tests/format/fprintf.c:37
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 11: OK: Expected signal at tests/format/fprintf.c:37
+TEST 11: OK: Expected signal at tests/format/fprintf.c:38
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 12: OK: Expected signal at tests/format/fprintf.c:38
-TEST 13: OK: Expected execution at tests/format/fprintf.c:41
-TEST 14: OK: Expected execution at tests/format/fprintf.c:42
+TEST 12: OK: Expected signal at tests/format/fprintf.c:39
+TEST 13: OK: Expected execution at tests/format/fprintf.c:42
+TEST 14: OK: Expected execution at tests/format/fprintf.c:43
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 15: OK: Expected signal at tests/format/fprintf.c:43
+TEST 15: OK: Expected signal at tests/format/fprintf.c:44
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 16: OK: Expected signal at tests/format/fprintf.c:44
+TEST 16: OK: Expected signal at tests/format/fprintf.c:45
 sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 17: OK: Expected signal at tests/format/fprintf.c:45
-TEST 18: OK: Expected execution at tests/format/fprintf.c:46
+TEST 17: OK: Expected signal at tests/format/fprintf.c:46
+TEST 18: OK: Expected execution at tests/format/fprintf.c:47
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
index 2fa4a16bc9bd2ca99c7b38bc5a7c93e8f09c2823..3335b94a93bd6dc5293f59cb402f50eae25adf44 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
@@ -1,575 +1,575 @@
-TEST 1: OK: Expected execution at tests/format/printf.c:180
-TEST 2: OK: Expected execution at tests/format/printf.c:183
+TEST 1: OK: Expected execution at tests/format/printf.c:184
+TEST 2: OK: Expected execution at tests/format/printf.c:187
 printf: directive 4 (%u) in format "%s - %s and say it %d or %u more times 
 " has no argument
-TEST 3: OK: Expected signal at tests/format/printf.c:186
-TEST 4: OK: Expected execution at tests/format/printf.c:189
+TEST 3: OK: Expected signal at tests/format/printf.c:190
+TEST 4: OK: Expected execution at tests/format/printf.c:193
 printf: invalid format string (unallocated or unterminated)
-TEST 5: OK: Expected signal at tests/format/printf.c:194
-TEST 6: OK: Expected execution at tests/format/printf.c:197
+TEST 5: OK: Expected signal at tests/format/printf.c:198
+TEST 6: OK: Expected execution at tests/format/printf.c:201
 printf: directive 4 (%4$s) in format "%4$s Say it %2$d or %1$u times 
 " has no argument
-TEST 7: OK: Expected signal at tests/format/printf.c:199
+TEST 7: OK: Expected signal at tests/format/printf.c:203
 Format error: illegal format specifier '$'
-TEST 8: OK: Expected signal at tests/format/printf.c:201
+TEST 8: OK: Expected signal at tests/format/printf.c:205
 Format error: "%s Say it %2$d or %3$u times 
 ":  numbered and non-numbered directives cannot be mixed
-TEST 9: OK: Expected signal at tests/format/printf.c:204
-TEST 10: OK: Expected execution at tests/format/printf.c:206
-TEST 11: OK: Expected execution at tests/format/printf.c:209
-TEST 12: OK: Expected execution at tests/format/printf.c:209
-TEST 13: OK: Expected execution at tests/format/printf.c:209
-TEST 14: OK: Expected execution at tests/format/printf.c:209
-TEST 15: OK: Expected execution at tests/format/printf.c:209
-TEST 16: OK: Expected execution at tests/format/printf.c:209
-TEST 17: OK: Expected execution at tests/format/printf.c:209
-TEST 18: OK: Expected execution at tests/format/printf.c:209
-TEST 19: OK: Expected execution at tests/format/printf.c:209
-TEST 20: OK: Expected execution at tests/format/printf.c:209
-TEST 21: OK: Expected execution at tests/format/printf.c:209
-TEST 22: OK: Expected execution at tests/format/printf.c:209
-TEST 23: OK: Expected execution at tests/format/printf.c:209
+TEST 9: OK: Expected signal at tests/format/printf.c:208
+TEST 10: OK: Expected execution at tests/format/printf.c:210
+TEST 11: OK: Expected execution at tests/format/printf.c:213
+TEST 12: OK: Expected execution at tests/format/printf.c:213
+TEST 13: OK: Expected execution at tests/format/printf.c:213
+TEST 14: OK: Expected execution at tests/format/printf.c:213
+TEST 15: OK: Expected execution at tests/format/printf.c:213
+TEST 16: OK: Expected execution at tests/format/printf.c:213
+TEST 17: OK: Expected execution at tests/format/printf.c:213
+TEST 18: OK: Expected execution at tests/format/printf.c:213
+TEST 19: OK: Expected execution at tests/format/printf.c:213
+TEST 20: OK: Expected execution at tests/format/printf.c:213
+TEST 21: OK: Expected execution at tests/format/printf.c:213
+TEST 22: OK: Expected execution at tests/format/printf.c:213
+TEST 23: OK: Expected execution at tests/format/printf.c:213
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [c]
-TEST 24: OK: Expected signal at tests/format/printf.c:209
-TEST 25: OK: Expected execution at tests/format/printf.c:209
+TEST 24: OK: Expected signal at tests/format/printf.c:213
+TEST 25: OK: Expected execution at tests/format/printf.c:213
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [p]
-TEST 26: OK: Expected signal at tests/format/printf.c:209
+TEST 26: OK: Expected signal at tests/format/printf.c:213
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
-TEST 27: OK: Expected signal at tests/format/printf.c:209
+TEST 27: OK: Expected signal at tests/format/printf.c:213
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [d]
-TEST 28: OK: Expected signal at tests/format/printf.c:215
+TEST 28: OK: Expected signal at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [i]
-TEST 29: OK: Expected signal at tests/format/printf.c:215
-TEST 30: OK: Expected execution at tests/format/printf.c:215
+TEST 29: OK: Expected signal at tests/format/printf.c:219
+TEST 30: OK: Expected execution at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [u]
-TEST 31: OK: Expected signal at tests/format/printf.c:215
-TEST 32: OK: Expected execution at tests/format/printf.c:215
-TEST 33: OK: Expected execution at tests/format/printf.c:215
-TEST 34: OK: Expected execution at tests/format/printf.c:215
-TEST 35: OK: Expected execution at tests/format/printf.c:215
-TEST 36: OK: Expected execution at tests/format/printf.c:215
-TEST 37: OK: Expected execution at tests/format/printf.c:215
-TEST 38: OK: Expected execution at tests/format/printf.c:215
-TEST 39: OK: Expected execution at tests/format/printf.c:215
-TEST 40: OK: Expected execution at tests/format/printf.c:215
+TEST 31: OK: Expected signal at tests/format/printf.c:219
+TEST 32: OK: Expected execution at tests/format/printf.c:219
+TEST 33: OK: Expected execution at tests/format/printf.c:219
+TEST 34: OK: Expected execution at tests/format/printf.c:219
+TEST 35: OK: Expected execution at tests/format/printf.c:219
+TEST 36: OK: Expected execution at tests/format/printf.c:219
+TEST 37: OK: Expected execution at tests/format/printf.c:219
+TEST 38: OK: Expected execution at tests/format/printf.c:219
+TEST 39: OK: Expected execution at tests/format/printf.c:219
+TEST 40: OK: Expected execution at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [c]
-TEST 41: OK: Expected signal at tests/format/printf.c:215
+TEST 41: OK: Expected signal at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [s]
-TEST 42: OK: Expected signal at tests/format/printf.c:215
+TEST 42: OK: Expected signal at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [p]
-TEST 43: OK: Expected signal at tests/format/printf.c:215
+TEST 43: OK: Expected signal at tests/format/printf.c:219
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [n]
-TEST 44: OK: Expected signal at tests/format/printf.c:215
-TEST 45: OK: Expected execution at tests/format/printf.c:218
-TEST 46: OK: Expected execution at tests/format/printf.c:218
-TEST 47: OK: Expected execution at tests/format/printf.c:218
-TEST 48: OK: Expected execution at tests/format/printf.c:218
-TEST 49: OK: Expected execution at tests/format/printf.c:218
-TEST 50: OK: Expected execution at tests/format/printf.c:218
-TEST 51: OK: Expected execution at tests/format/printf.c:218
-TEST 52: OK: Expected execution at tests/format/printf.c:218
-TEST 53: OK: Expected execution at tests/format/printf.c:218
-TEST 54: OK: Expected execution at tests/format/printf.c:218
-TEST 55: OK: Expected execution at tests/format/printf.c:218
-TEST 56: OK: Expected execution at tests/format/printf.c:218
-TEST 57: OK: Expected execution at tests/format/printf.c:218
+TEST 44: OK: Expected signal at tests/format/printf.c:219
+TEST 45: OK: Expected execution at tests/format/printf.c:222
+TEST 46: OK: Expected execution at tests/format/printf.c:222
+TEST 47: OK: Expected execution at tests/format/printf.c:222
+TEST 48: OK: Expected execution at tests/format/printf.c:222
+TEST 49: OK: Expected execution at tests/format/printf.c:222
+TEST 50: OK: Expected execution at tests/format/printf.c:222
+TEST 51: OK: Expected execution at tests/format/printf.c:222
+TEST 52: OK: Expected execution at tests/format/printf.c:222
+TEST 53: OK: Expected execution at tests/format/printf.c:222
+TEST 54: OK: Expected execution at tests/format/printf.c:222
+TEST 55: OK: Expected execution at tests/format/printf.c:222
+TEST 56: OK: Expected execution at tests/format/printf.c:222
+TEST 57: OK: Expected execution at tests/format/printf.c:222
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [c]
-TEST 58: OK: Expected signal at tests/format/printf.c:218
+TEST 58: OK: Expected signal at tests/format/printf.c:222
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [s]
-TEST 59: OK: Expected signal at tests/format/printf.c:218
+TEST 59: OK: Expected signal at tests/format/printf.c:222
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [p]
-TEST 60: OK: Expected signal at tests/format/printf.c:218
+TEST 60: OK: Expected signal at tests/format/printf.c:222
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [n]
-TEST 61: OK: Expected signal at tests/format/printf.c:218
-TEST 62: OK: Expected execution at tests/format/printf.c:224
-TEST 63: OK: Expected execution at tests/format/printf.c:225
+TEST 61: OK: Expected signal at tests/format/printf.c:222
+TEST 62: OK: Expected execution at tests/format/printf.c:228
+TEST 63: OK: Expected execution at tests/format/printf.c:229
 Format error: illegal format specifier 'l'
-TEST 64: OK: Expected signal at tests/format/printf.c:226
+TEST 64: OK: Expected signal at tests/format/printf.c:230
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [f]
-TEST 65: OK: Expected signal at tests/format/printf.c:232
+TEST 65: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [F]
-TEST 66: OK: Expected signal at tests/format/printf.c:232
+TEST 66: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [e]
-TEST 67: OK: Expected signal at tests/format/printf.c:232
+TEST 67: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [E]
-TEST 68: OK: Expected signal at tests/format/printf.c:232
+TEST 68: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [g]
-TEST 69: OK: Expected signal at tests/format/printf.c:232
+TEST 69: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [G]
-TEST 70: OK: Expected signal at tests/format/printf.c:232
+TEST 70: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [a]
-TEST 71: OK: Expected signal at tests/format/printf.c:232
+TEST 71: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [A]
-TEST 72: OK: Expected signal at tests/format/printf.c:232
+TEST 72: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [c]
-TEST 73: OK: Expected signal at tests/format/printf.c:232
+TEST 73: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [s]
-TEST 74: OK: Expected signal at tests/format/printf.c:232
+TEST 74: OK: Expected signal at tests/format/printf.c:236
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [hh] to format specifier [p]
-TEST 75: OK: Expected signal at tests/format/printf.c:232
-TEST 76: OK: Expected execution at tests/format/printf.c:233
-TEST 77: OK: Expected execution at tests/format/printf.c:233
-TEST 78: OK: Expected execution at tests/format/printf.c:234
-TEST 79: OK: Expected execution at tests/format/printf.c:234
-TEST 80: OK: Expected execution at tests/format/printf.c:235
-TEST 81: OK: Expected execution at tests/format/printf.c:235
-TEST 82: OK: Expected execution at tests/format/printf.c:235
+TEST 75: OK: Expected signal at tests/format/printf.c:236
+TEST 76: OK: Expected execution at tests/format/printf.c:237
+TEST 77: OK: Expected execution at tests/format/printf.c:237
+TEST 78: OK: Expected execution at tests/format/printf.c:238
+TEST 79: OK: Expected execution at tests/format/printf.c:238
+TEST 80: OK: Expected execution at tests/format/printf.c:239
+TEST 81: OK: Expected execution at tests/format/printf.c:239
+TEST 82: OK: Expected execution at tests/format/printf.c:239
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [f]
-TEST 83: OK: Expected signal at tests/format/printf.c:238
+TEST 83: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [F]
-TEST 84: OK: Expected signal at tests/format/printf.c:238
+TEST 84: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [e]
-TEST 85: OK: Expected signal at tests/format/printf.c:238
+TEST 85: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [E]
-TEST 86: OK: Expected signal at tests/format/printf.c:238
+TEST 86: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [g]
-TEST 87: OK: Expected signal at tests/format/printf.c:238
+TEST 87: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [G]
-TEST 88: OK: Expected signal at tests/format/printf.c:238
+TEST 88: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [a]
-TEST 89: OK: Expected signal at tests/format/printf.c:238
+TEST 89: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [A]
-TEST 90: OK: Expected signal at tests/format/printf.c:238
+TEST 90: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [c]
-TEST 91: OK: Expected signal at tests/format/printf.c:238
+TEST 91: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [s]
-TEST 92: OK: Expected signal at tests/format/printf.c:238
+TEST 92: OK: Expected signal at tests/format/printf.c:242
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [h] to format specifier [p]
-TEST 93: OK: Expected signal at tests/format/printf.c:238
-TEST 94: OK: Expected execution at tests/format/printf.c:239
-TEST 95: OK: Expected execution at tests/format/printf.c:239
-TEST 96: OK: Expected execution at tests/format/printf.c:240
-TEST 97: OK: Expected execution at tests/format/printf.c:240
-TEST 98: OK: Expected execution at tests/format/printf.c:241
-TEST 99: OK: Expected execution at tests/format/printf.c:241
-TEST 100: OK: Expected execution at tests/format/printf.c:241
+TEST 93: OK: Expected signal at tests/format/printf.c:242
+TEST 94: OK: Expected execution at tests/format/printf.c:243
+TEST 95: OK: Expected execution at tests/format/printf.c:243
+TEST 96: OK: Expected execution at tests/format/printf.c:244
+TEST 97: OK: Expected execution at tests/format/printf.c:244
+TEST 98: OK: Expected execution at tests/format/printf.c:245
+TEST 99: OK: Expected execution at tests/format/printf.c:245
+TEST 100: OK: Expected execution at tests/format/printf.c:245
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [l] to format specifier [p]
-TEST 101: OK: Expected signal at tests/format/printf.c:244
-TEST 102: OK: Expected execution at tests/format/printf.c:245
-TEST 103: OK: Expected execution at tests/format/printf.c:245
-TEST 104: OK: Expected execution at tests/format/printf.c:246
-TEST 105: OK: Expected execution at tests/format/printf.c:246
-TEST 106: OK: Expected execution at tests/format/printf.c:247
-TEST 107: OK: Expected execution at tests/format/printf.c:247
-TEST 108: OK: Expected execution at tests/format/printf.c:249
-TEST 109: OK: Expected execution at tests/format/printf.c:249
-TEST 110: OK: Expected execution at tests/format/printf.c:250
-TEST 111: OK: Expected execution at tests/format/printf.c:250
-TEST 112: OK: Expected execution at tests/format/printf.c:251
-TEST 113: OK: Expected execution at tests/format/printf.c:251
-TEST 114: OK: Expected execution at tests/format/printf.c:252
-TEST 115: OK: Expected execution at tests/format/printf.c:252
-TEST 116: OK: Expected execution at tests/format/printf.c:254
-TEST 117: OK: Expected execution at tests/format/printf.c:257
-TEST 118: OK: Expected execution at tests/format/printf.c:261
-TEST 119: OK: Expected execution at tests/format/printf.c:261
-TEST 120: OK: Expected execution at tests/format/printf.c:262
-TEST 121: OK: Expected execution at tests/format/printf.c:262
-TEST 122: OK: Expected execution at tests/format/printf.c:263
-TEST 123: OK: Expected execution at tests/format/printf.c:263
-TEST 124: OK: Expected execution at tests/format/printf.c:263
+TEST 101: OK: Expected signal at tests/format/printf.c:248
+TEST 102: OK: Expected execution at tests/format/printf.c:249
+TEST 103: OK: Expected execution at tests/format/printf.c:249
+TEST 104: OK: Expected execution at tests/format/printf.c:250
+TEST 105: OK: Expected execution at tests/format/printf.c:250
+TEST 106: OK: Expected execution at tests/format/printf.c:251
+TEST 107: OK: Expected execution at tests/format/printf.c:251
+TEST 108: OK: Expected execution at tests/format/printf.c:253
+TEST 109: OK: Expected execution at tests/format/printf.c:253
+TEST 110: OK: Expected execution at tests/format/printf.c:254
+TEST 111: OK: Expected execution at tests/format/printf.c:254
+TEST 112: OK: Expected execution at tests/format/printf.c:255
+TEST 113: OK: Expected execution at tests/format/printf.c:255
+TEST 114: OK: Expected execution at tests/format/printf.c:256
+TEST 115: OK: Expected execution at tests/format/printf.c:256
+TEST 116: OK: Expected execution at tests/format/printf.c:258
+TEST 117: OK: Expected execution at tests/format/printf.c:261
+TEST 118: OK: Expected execution at tests/format/printf.c:265
+TEST 119: OK: Expected execution at tests/format/printf.c:265
+TEST 120: OK: Expected execution at tests/format/printf.c:266
+TEST 121: OK: Expected execution at tests/format/printf.c:266
+TEST 122: OK: Expected execution at tests/format/printf.c:267
+TEST 123: OK: Expected execution at tests/format/printf.c:267
+TEST 124: OK: Expected execution at tests/format/printf.c:267
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [f]
-TEST 125: OK: Expected signal at tests/format/printf.c:266
+TEST 125: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [F]
-TEST 126: OK: Expected signal at tests/format/printf.c:266
+TEST 126: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [e]
-TEST 127: OK: Expected signal at tests/format/printf.c:266
+TEST 127: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [E]
-TEST 128: OK: Expected signal at tests/format/printf.c:266
+TEST 128: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [g]
-TEST 129: OK: Expected signal at tests/format/printf.c:266
+TEST 129: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [G]
-TEST 130: OK: Expected signal at tests/format/printf.c:266
+TEST 130: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [a]
-TEST 131: OK: Expected signal at tests/format/printf.c:266
+TEST 131: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [A]
-TEST 132: OK: Expected signal at tests/format/printf.c:266
+TEST 132: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [c]
-TEST 133: OK: Expected signal at tests/format/printf.c:266
+TEST 133: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [s]
-TEST 134: OK: Expected signal at tests/format/printf.c:266
+TEST 134: OK: Expected signal at tests/format/printf.c:270
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [j] to format specifier [p]
-TEST 135: OK: Expected signal at tests/format/printf.c:266
-TEST 136: OK: Expected execution at tests/format/printf.c:267
-TEST 137: OK: Expected execution at tests/format/printf.c:267
-TEST 138: OK: Expected execution at tests/format/printf.c:268
-TEST 139: OK: Expected execution at tests/format/printf.c:268
-TEST 140: OK: Expected execution at tests/format/printf.c:269
-TEST 141: OK: Expected execution at tests/format/printf.c:269
-TEST 142: OK: Expected execution at tests/format/printf.c:269
+TEST 135: OK: Expected signal at tests/format/printf.c:270
+TEST 136: OK: Expected execution at tests/format/printf.c:271
+TEST 137: OK: Expected execution at tests/format/printf.c:271
+TEST 138: OK: Expected execution at tests/format/printf.c:272
+TEST 139: OK: Expected execution at tests/format/printf.c:272
+TEST 140: OK: Expected execution at tests/format/printf.c:273
+TEST 141: OK: Expected execution at tests/format/printf.c:273
+TEST 142: OK: Expected execution at tests/format/printf.c:273
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [f]
-TEST 143: OK: Expected signal at tests/format/printf.c:272
+TEST 143: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [F]
-TEST 144: OK: Expected signal at tests/format/printf.c:272
+TEST 144: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [e]
-TEST 145: OK: Expected signal at tests/format/printf.c:272
+TEST 145: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [E]
-TEST 146: OK: Expected signal at tests/format/printf.c:272
+TEST 146: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [g]
-TEST 147: OK: Expected signal at tests/format/printf.c:272
+TEST 147: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [G]
-TEST 148: OK: Expected signal at tests/format/printf.c:272
+TEST 148: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [a]
-TEST 149: OK: Expected signal at tests/format/printf.c:272
+TEST 149: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [A]
-TEST 150: OK: Expected signal at tests/format/printf.c:272
+TEST 150: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [c]
-TEST 151: OK: Expected signal at tests/format/printf.c:272
+TEST 151: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [s]
-TEST 152: OK: Expected signal at tests/format/printf.c:272
+TEST 152: OK: Expected signal at tests/format/printf.c:276
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [z] to format specifier [p]
-TEST 153: OK: Expected signal at tests/format/printf.c:272
-TEST 154: OK: Expected execution at tests/format/printf.c:277
-TEST 155: OK: Expected execution at tests/format/printf.c:277
-TEST 156: OK: Expected execution at tests/format/printf.c:281
-TEST 157: OK: Expected execution at tests/format/printf.c:281
-TEST 158: OK: Expected execution at tests/format/printf.c:282
-TEST 159: OK: Expected execution at tests/format/printf.c:282
-TEST 160: OK: Expected execution at tests/format/printf.c:282
+TEST 153: OK: Expected signal at tests/format/printf.c:276
+TEST 154: OK: Expected execution at tests/format/printf.c:281
+TEST 155: OK: Expected execution at tests/format/printf.c:281
+TEST 156: OK: Expected execution at tests/format/printf.c:285
+TEST 157: OK: Expected execution at tests/format/printf.c:285
+TEST 158: OK: Expected execution at tests/format/printf.c:286
+TEST 159: OK: Expected execution at tests/format/printf.c:286
+TEST 160: OK: Expected execution at tests/format/printf.c:286
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [f]
-TEST 161: OK: Expected signal at tests/format/printf.c:287
+TEST 161: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [F]
-TEST 162: OK: Expected signal at tests/format/printf.c:287
+TEST 162: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [e]
-TEST 163: OK: Expected signal at tests/format/printf.c:287
+TEST 163: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [E]
-TEST 164: OK: Expected signal at tests/format/printf.c:287
+TEST 164: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [g]
-TEST 165: OK: Expected signal at tests/format/printf.c:287
+TEST 165: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [G]
-TEST 166: OK: Expected signal at tests/format/printf.c:287
+TEST 166: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [a]
-TEST 167: OK: Expected signal at tests/format/printf.c:287
+TEST 167: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [A]
-TEST 168: OK: Expected signal at tests/format/printf.c:287
+TEST 168: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [c]
-TEST 169: OK: Expected signal at tests/format/printf.c:287
+TEST 169: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [s]
-TEST 170: OK: Expected signal at tests/format/printf.c:287
+TEST 170: OK: Expected signal at tests/format/printf.c:291
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [t] to format specifier [p]
-TEST 171: OK: Expected signal at tests/format/printf.c:287
-TEST 172: OK: Expected execution at tests/format/printf.c:289
-TEST 173: OK: Expected execution at tests/format/printf.c:289
-TEST 174: OK: Expected execution at tests/format/printf.c:290
-TEST 175: OK: Expected execution at tests/format/printf.c:290
-TEST 176: OK: Expected execution at tests/format/printf.c:295
-TEST 177: OK: Expected execution at tests/format/printf.c:295
-TEST 178: OK: Expected execution at tests/format/printf.c:296
+TEST 171: OK: Expected signal at tests/format/printf.c:291
+TEST 172: OK: Expected execution at tests/format/printf.c:293
+TEST 173: OK: Expected execution at tests/format/printf.c:293
+TEST 174: OK: Expected execution at tests/format/printf.c:294
+TEST 175: OK: Expected execution at tests/format/printf.c:294
+TEST 176: OK: Expected execution at tests/format/printf.c:299
+TEST 177: OK: Expected execution at tests/format/printf.c:299
+TEST 178: OK: Expected execution at tests/format/printf.c:300
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [d]
-TEST 179: OK: Expected signal at tests/format/printf.c:299
+TEST 179: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [i]
-TEST 180: OK: Expected signal at tests/format/printf.c:299
+TEST 180: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [o]
-TEST 181: OK: Expected signal at tests/format/printf.c:299
+TEST 181: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [u]
-TEST 182: OK: Expected signal at tests/format/printf.c:299
+TEST 182: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [x]
-TEST 183: OK: Expected signal at tests/format/printf.c:299
+TEST 183: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [c]
-TEST 184: OK: Expected signal at tests/format/printf.c:299
+TEST 184: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [s]
-TEST 185: OK: Expected signal at tests/format/printf.c:299
+TEST 185: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [p]
-TEST 186: OK: Expected signal at tests/format/printf.c:299
+TEST 186: OK: Expected signal at tests/format/printf.c:303
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of length modifier [L] to format specifier [n]
-TEST 187: OK: Expected signal at tests/format/printf.c:299
-TEST 188: OK: Expected execution at tests/format/printf.c:300
-TEST 189: OK: Expected execution at tests/format/printf.c:300
-TEST 190: OK: Expected execution at tests/format/printf.c:301
-TEST 191: OK: Expected execution at tests/format/printf.c:301
-TEST 192: OK: Expected execution at tests/format/printf.c:302
-TEST 193: OK: Expected execution at tests/format/printf.c:302
-TEST 194: OK: Expected execution at tests/format/printf.c:303
-TEST 195: OK: Expected execution at tests/format/printf.c:303
+TEST 187: OK: Expected signal at tests/format/printf.c:303
+TEST 188: OK: Expected execution at tests/format/printf.c:304
+TEST 189: OK: Expected execution at tests/format/printf.c:304
+TEST 190: OK: Expected execution at tests/format/printf.c:305
+TEST 191: OK: Expected execution at tests/format/printf.c:305
+TEST 192: OK: Expected execution at tests/format/printf.c:306
+TEST 193: OK: Expected execution at tests/format/printf.c:306
+TEST 194: OK: Expected execution at tests/format/printf.c:307
+TEST 195: OK: Expected execution at tests/format/printf.c:307
 Format error: illegal format specifier 'C'
-TEST 196: OK: Expected signal at tests/format/printf.c:307
+TEST 196: OK: Expected signal at tests/format/printf.c:311
 Format error: illegal format specifier 'S'
-TEST 197: OK: Expected signal at tests/format/printf.c:308
+TEST 197: OK: Expected signal at tests/format/printf.c:312
 Format error: illegal format specifier 'm'
-TEST 198: OK: Expected signal at tests/format/printf.c:309
-TEST 199: OK: Expected execution at tests/format/printf.c:312
-TEST 200: OK: Expected execution at tests/format/printf.c:312
-TEST 201: OK: Expected execution at tests/format/printf.c:313
-TEST 202: OK: Expected execution at tests/format/printf.c:313
-TEST 203: OK: Expected execution at tests/format/printf.c:314
-TEST 204: OK: Expected execution at tests/format/printf.c:314
+TEST 198: OK: Expected signal at tests/format/printf.c:313
+TEST 199: OK: Expected execution at tests/format/printf.c:316
+TEST 200: OK: Expected execution at tests/format/printf.c:316
+TEST 201: OK: Expected execution at tests/format/printf.c:317
+TEST 202: OK: Expected execution at tests/format/printf.c:317
+TEST 203: OK: Expected execution at tests/format/printf.c:318
+TEST 204: OK: Expected execution at tests/format/printf.c:318
 printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 205: OK: Expected signal at tests/format/printf.c:315
+TEST 205: OK: Expected signal at tests/format/printf.c:319
 printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 206: OK: Expected signal at tests/format/printf.c:315
+TEST 206: OK: Expected signal at tests/format/printf.c:319
 printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 207: OK: Expected signal at tests/format/printf.c:316
+TEST 207: OK: Expected signal at tests/format/printf.c:320
 printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 208: OK: Expected signal at tests/format/printf.c:316
+TEST 208: OK: Expected signal at tests/format/printf.c:320
 printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'void*'
-TEST 209: OK: Expected signal at tests/format/printf.c:317
+TEST 209: OK: Expected signal at tests/format/printf.c:321
 printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'void*'
-TEST 210: OK: Expected signal at tests/format/printf.c:317
+TEST 210: OK: Expected signal at tests/format/printf.c:321
 printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 211: OK: Expected signal at tests/format/printf.c:318
+TEST 211: OK: Expected signal at tests/format/printf.c:322
 printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 212: OK: Expected signal at tests/format/printf.c:318
-TEST 213: OK: Expected execution at tests/format/printf.c:321
-TEST 214: OK: Expected execution at tests/format/printf.c:321
-TEST 215: OK: Expected execution at tests/format/printf.c:322
-TEST 216: OK: Expected execution at tests/format/printf.c:322
-TEST 217: OK: Expected execution at tests/format/printf.c:323
-TEST 218: OK: Expected execution at tests/format/printf.c:323
-TEST 219: OK: Expected execution at tests/format/printf.c:324
-TEST 220: OK: Expected execution at tests/format/printf.c:324
-TEST 221: OK: Expected execution at tests/format/printf.c:326
-TEST 222: OK: Expected execution at tests/format/printf.c:326
-TEST 223: OK: Expected execution at tests/format/printf.c:330
-TEST 224: OK: Expected execution at tests/format/printf.c:330
-TEST 225: OK: Expected execution at tests/format/printf.c:333
-TEST 226: OK: Expected execution at tests/format/printf.c:333
-TEST 227: OK: Expected execution at tests/format/printf.c:333
-TEST 228: OK: Expected execution at tests/format/printf.c:333
+TEST 212: OK: Expected signal at tests/format/printf.c:322
+TEST 213: OK: Expected execution at tests/format/printf.c:325
+TEST 214: OK: Expected execution at tests/format/printf.c:325
+TEST 215: OK: Expected execution at tests/format/printf.c:326
+TEST 216: OK: Expected execution at tests/format/printf.c:326
+TEST 217: OK: Expected execution at tests/format/printf.c:327
+TEST 218: OK: Expected execution at tests/format/printf.c:327
+TEST 219: OK: Expected execution at tests/format/printf.c:328
+TEST 220: OK: Expected execution at tests/format/printf.c:328
+TEST 221: OK: Expected execution at tests/format/printf.c:330
+TEST 222: OK: Expected execution at tests/format/printf.c:330
+TEST 223: OK: Expected execution at tests/format/printf.c:334
+TEST 224: OK: Expected execution at tests/format/printf.c:334
+TEST 225: OK: Expected execution at tests/format/printf.c:337
+TEST 226: OK: Expected execution at tests/format/printf.c:337
+TEST 227: OK: Expected execution at tests/format/printf.c:337
+TEST 228: OK: Expected execution at tests/format/printf.c:337
 printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 229: OK: Expected signal at tests/format/printf.c:334
+TEST 229: OK: Expected signal at tests/format/printf.c:338
 printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 230: OK: Expected signal at tests/format/printf.c:334
+TEST 230: OK: Expected signal at tests/format/printf.c:338
 printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 231: OK: Expected signal at tests/format/printf.c:334
+TEST 231: OK: Expected signal at tests/format/printf.c:338
 printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 232: OK: Expected signal at tests/format/printf.c:334
+TEST 232: OK: Expected signal at tests/format/printf.c:338
 printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 233: OK: Expected signal at tests/format/printf.c:335
+TEST 233: OK: Expected signal at tests/format/printf.c:339
 printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 234: OK: Expected signal at tests/format/printf.c:335
+TEST 234: OK: Expected signal at tests/format/printf.c:339
 printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 235: OK: Expected signal at tests/format/printf.c:335
+TEST 235: OK: Expected signal at tests/format/printf.c:339
 printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 236: OK: Expected signal at tests/format/printf.c:335
+TEST 236: OK: Expected signal at tests/format/printf.c:339
 printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 237: OK: Expected signal at tests/format/printf.c:336
+TEST 237: OK: Expected signal at tests/format/printf.c:340
 printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 238: OK: Expected signal at tests/format/printf.c:336
+TEST 238: OK: Expected signal at tests/format/printf.c:340
 printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 239: OK: Expected signal at tests/format/printf.c:336
+TEST 239: OK: Expected signal at tests/format/printf.c:340
 printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 240: OK: Expected signal at tests/format/printf.c:336
+TEST 240: OK: Expected signal at tests/format/printf.c:340
 printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 241: OK: Expected signal at tests/format/printf.c:337
+TEST 241: OK: Expected signal at tests/format/printf.c:341
 printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 242: OK: Expected signal at tests/format/printf.c:337
+TEST 242: OK: Expected signal at tests/format/printf.c:341
 printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 243: OK: Expected signal at tests/format/printf.c:337
+TEST 243: OK: Expected signal at tests/format/printf.c:341
 printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 244: OK: Expected signal at tests/format/printf.c:337
+TEST 244: OK: Expected signal at tests/format/printf.c:341
 printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 245: OK: Expected signal at tests/format/printf.c:338
+TEST 245: OK: Expected signal at tests/format/printf.c:342
 printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 246: OK: Expected signal at tests/format/printf.c:338
+TEST 246: OK: Expected signal at tests/format/printf.c:342
 printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 247: OK: Expected signal at tests/format/printf.c:338
+TEST 247: OK: Expected signal at tests/format/printf.c:342
 printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 248: OK: Expected signal at tests/format/printf.c:338
-TEST 249: OK: Expected execution at tests/format/printf.c:341
-TEST 250: OK: Expected execution at tests/format/printf.c:341
-TEST 251: OK: Expected execution at tests/format/printf.c:341
-TEST 252: OK: Expected execution at tests/format/printf.c:341
-TEST 253: OK: Expected execution at tests/format/printf.c:342
-TEST 254: OK: Expected execution at tests/format/printf.c:342
-TEST 255: OK: Expected execution at tests/format/printf.c:342
-TEST 256: OK: Expected execution at tests/format/printf.c:342
-TEST 257: OK: Expected execution at tests/format/printf.c:344
-TEST 258: OK: Expected execution at tests/format/printf.c:344
-TEST 259: OK: Expected execution at tests/format/printf.c:344
-TEST 260: OK: Expected execution at tests/format/printf.c:344
-TEST 261: OK: Expected execution at tests/format/printf.c:346
-TEST 262: OK: Expected execution at tests/format/printf.c:346
-TEST 263: OK: Expected execution at tests/format/printf.c:346
-TEST 264: OK: Expected execution at tests/format/printf.c:346
-TEST 265: OK: Expected execution at tests/format/printf.c:347
-TEST 266: OK: Expected execution at tests/format/printf.c:347
-TEST 267: OK: Expected execution at tests/format/printf.c:347
-TEST 268: OK: Expected execution at tests/format/printf.c:347
-TEST 269: OK: Expected execution at tests/format/printf.c:348
-TEST 270: OK: Expected execution at tests/format/printf.c:348
-TEST 271: OK: Expected execution at tests/format/printf.c:348
-TEST 272: OK: Expected execution at tests/format/printf.c:348
-TEST 273: OK: Expected execution at tests/format/printf.c:350
-TEST 274: OK: Expected execution at tests/format/printf.c:350
-TEST 275: OK: Expected execution at tests/format/printf.c:350
-TEST 276: OK: Expected execution at tests/format/printf.c:350
-TEST 277: OK: Expected execution at tests/format/printf.c:354
-TEST 278: OK: Expected execution at tests/format/printf.c:354
+TEST 248: OK: Expected signal at tests/format/printf.c:342
+TEST 249: OK: Expected execution at tests/format/printf.c:345
+TEST 250: OK: Expected execution at tests/format/printf.c:345
+TEST 251: OK: Expected execution at tests/format/printf.c:345
+TEST 252: OK: Expected execution at tests/format/printf.c:345
+TEST 253: OK: Expected execution at tests/format/printf.c:346
+TEST 254: OK: Expected execution at tests/format/printf.c:346
+TEST 255: OK: Expected execution at tests/format/printf.c:346
+TEST 256: OK: Expected execution at tests/format/printf.c:346
+TEST 257: OK: Expected execution at tests/format/printf.c:348
+TEST 258: OK: Expected execution at tests/format/printf.c:348
+TEST 259: OK: Expected execution at tests/format/printf.c:348
+TEST 260: OK: Expected execution at tests/format/printf.c:348
+TEST 261: OK: Expected execution at tests/format/printf.c:350
+TEST 262: OK: Expected execution at tests/format/printf.c:350
+TEST 263: OK: Expected execution at tests/format/printf.c:350
+TEST 264: OK: Expected execution at tests/format/printf.c:350
+TEST 265: OK: Expected execution at tests/format/printf.c:351
+TEST 266: OK: Expected execution at tests/format/printf.c:351
+TEST 267: OK: Expected execution at tests/format/printf.c:351
+TEST 268: OK: Expected execution at tests/format/printf.c:351
+TEST 269: OK: Expected execution at tests/format/printf.c:352
+TEST 270: OK: Expected execution at tests/format/printf.c:352
+TEST 271: OK: Expected execution at tests/format/printf.c:352
+TEST 272: OK: Expected execution at tests/format/printf.c:352
+TEST 273: OK: Expected execution at tests/format/printf.c:354
+TEST 274: OK: Expected execution at tests/format/printf.c:354
+TEST 275: OK: Expected execution at tests/format/printf.c:354
+TEST 276: OK: Expected execution at tests/format/printf.c:354
+TEST 277: OK: Expected execution at tests/format/printf.c:358
+TEST 278: OK: Expected execution at tests/format/printf.c:358
 printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 279: OK: Expected signal at tests/format/printf.c:355
+TEST 279: OK: Expected signal at tests/format/printf.c:359
 printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 280: OK: Expected signal at tests/format/printf.c:355
+TEST 280: OK: Expected signal at tests/format/printf.c:359
 printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 281: OK: Expected signal at tests/format/printf.c:356
+TEST 281: OK: Expected signal at tests/format/printf.c:360
 printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 282: OK: Expected signal at tests/format/printf.c:356
+TEST 282: OK: Expected signal at tests/format/printf.c:360
 printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 283: OK: Expected signal at tests/format/printf.c:357
+TEST 283: OK: Expected signal at tests/format/printf.c:361
 printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 284: OK: Expected signal at tests/format/printf.c:357
-TEST 285: OK: Expected execution at tests/format/printf.c:358
-TEST 286: OK: Expected execution at tests/format/printf.c:358
+TEST 284: OK: Expected signal at tests/format/printf.c:361
+TEST 285: OK: Expected execution at tests/format/printf.c:362
+TEST 286: OK: Expected execution at tests/format/printf.c:362
 printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 287: OK: Expected signal at tests/format/printf.c:359
+TEST 287: OK: Expected signal at tests/format/printf.c:363
 printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 288: OK: Expected signal at tests/format/printf.c:359
+TEST 288: OK: Expected signal at tests/format/printf.c:363
 printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 289: OK: Expected signal at tests/format/printf.c:360
+TEST 289: OK: Expected signal at tests/format/printf.c:364
 printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 290: OK: Expected signal at tests/format/printf.c:360
+TEST 290: OK: Expected signal at tests/format/printf.c:364
 printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 291: OK: Expected signal at tests/format/printf.c:361
+TEST 291: OK: Expected signal at tests/format/printf.c:365
 printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 292: OK: Expected signal at tests/format/printf.c:361
-TEST 293: OK: Expected execution at tests/format/printf.c:362
-TEST 294: OK: Expected execution at tests/format/printf.c:362
+TEST 292: OK: Expected signal at tests/format/printf.c:365
+TEST 293: OK: Expected execution at tests/format/printf.c:366
+TEST 294: OK: Expected execution at tests/format/printf.c:366
 printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 295: OK: Expected signal at tests/format/printf.c:363
+TEST 295: OK: Expected signal at tests/format/printf.c:367
 printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 296: OK: Expected signal at tests/format/printf.c:363
+TEST 296: OK: Expected signal at tests/format/printf.c:367
 printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 297: OK: Expected signal at tests/format/printf.c:364
+TEST 297: OK: Expected signal at tests/format/printf.c:368
 printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 298: OK: Expected signal at tests/format/printf.c:364
+TEST 298: OK: Expected signal at tests/format/printf.c:368
 printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 299: OK: Expected signal at tests/format/printf.c:365
+TEST 299: OK: Expected signal at tests/format/printf.c:369
 printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 300: OK: Expected signal at tests/format/printf.c:365
-TEST 301: OK: Expected execution at tests/format/printf.c:366
-TEST 302: OK: Expected execution at tests/format/printf.c:366
+TEST 300: OK: Expected signal at tests/format/printf.c:369
+TEST 301: OK: Expected execution at tests/format/printf.c:370
+TEST 302: OK: Expected execution at tests/format/printf.c:370
 printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 303: OK: Expected signal at tests/format/printf.c:367
+TEST 303: OK: Expected signal at tests/format/printf.c:371
 printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 304: OK: Expected signal at tests/format/printf.c:367
+TEST 304: OK: Expected signal at tests/format/printf.c:371
 printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 305: OK: Expected signal at tests/format/printf.c:368
+TEST 305: OK: Expected signal at tests/format/printf.c:372
 printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 306: OK: Expected signal at tests/format/printf.c:368
+TEST 306: OK: Expected signal at tests/format/printf.c:372
 printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 307: OK: Expected signal at tests/format/printf.c:369
+TEST 307: OK: Expected signal at tests/format/printf.c:373
 printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 308: OK: Expected signal at tests/format/printf.c:369
+TEST 308: OK: Expected signal at tests/format/printf.c:373
 printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 309: OK: Expected signal at tests/format/printf.c:372
+TEST 309: OK: Expected signal at tests/format/printf.c:376
 printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 310: OK: Expected signal at tests/format/printf.c:372
-TEST 311: OK: Expected execution at tests/format/printf.c:373
-TEST 312: OK: Expected execution at tests/format/printf.c:373
+TEST 310: OK: Expected signal at tests/format/printf.c:376
+TEST 311: OK: Expected execution at tests/format/printf.c:377
+TEST 312: OK: Expected execution at tests/format/printf.c:377
 printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 313: OK: Expected signal at tests/format/printf.c:374
+TEST 313: OK: Expected signal at tests/format/printf.c:378
 printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 314: OK: Expected signal at tests/format/printf.c:374
+TEST 314: OK: Expected signal at tests/format/printf.c:378
 printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 315: OK: Expected signal at tests/format/printf.c:375
+TEST 315: OK: Expected signal at tests/format/printf.c:379
 printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 316: OK: Expected signal at tests/format/printf.c:375
+TEST 316: OK: Expected signal at tests/format/printf.c:379
 printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 317: OK: Expected signal at tests/format/printf.c:376
+TEST 317: OK: Expected signal at tests/format/printf.c:380
 printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 318: OK: Expected signal at tests/format/printf.c:376
-TEST 319: OK: Expected execution at tests/format/printf.c:377
-TEST 320: OK: Expected execution at tests/format/printf.c:377
+TEST 318: OK: Expected signal at tests/format/printf.c:380
+TEST 319: OK: Expected execution at tests/format/printf.c:381
+TEST 320: OK: Expected execution at tests/format/printf.c:381
 printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 321: OK: Expected signal at tests/format/printf.c:378
+TEST 321: OK: Expected signal at tests/format/printf.c:382
 printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 322: OK: Expected signal at tests/format/printf.c:378
+TEST 322: OK: Expected signal at tests/format/printf.c:382
 printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 323: OK: Expected signal at tests/format/printf.c:379
+TEST 323: OK: Expected signal at tests/format/printf.c:383
 printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 324: OK: Expected signal at tests/format/printf.c:379
+TEST 324: OK: Expected signal at tests/format/printf.c:383
 printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 325: OK: Expected signal at tests/format/printf.c:380
+TEST 325: OK: Expected signal at tests/format/printf.c:384
 printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 326: OK: Expected signal at tests/format/printf.c:380
-TEST 327: OK: Expected execution at tests/format/printf.c:381
-TEST 328: OK: Expected execution at tests/format/printf.c:381
+TEST 326: OK: Expected signal at tests/format/printf.c:384
+TEST 327: OK: Expected execution at tests/format/printf.c:385
+TEST 328: OK: Expected execution at tests/format/printf.c:385
 printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 329: OK: Expected signal at tests/format/printf.c:382
+TEST 329: OK: Expected signal at tests/format/printf.c:386
 printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 330: OK: Expected signal at tests/format/printf.c:382
+TEST 330: OK: Expected signal at tests/format/printf.c:386
 printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 331: OK: Expected signal at tests/format/printf.c:383
+TEST 331: OK: Expected signal at tests/format/printf.c:387
 printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 332: OK: Expected signal at tests/format/printf.c:383
+TEST 332: OK: Expected signal at tests/format/printf.c:387
 printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 333: OK: Expected signal at tests/format/printf.c:384
+TEST 333: OK: Expected signal at tests/format/printf.c:388
 printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 334: OK: Expected signal at tests/format/printf.c:384
-TEST 335: OK: Expected execution at tests/format/printf.c:385
-TEST 336: OK: Expected execution at tests/format/printf.c:385
+TEST 334: OK: Expected signal at tests/format/printf.c:388
+TEST 335: OK: Expected execution at tests/format/printf.c:389
+TEST 336: OK: Expected execution at tests/format/printf.c:389
 printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 337: OK: Expected signal at tests/format/printf.c:386
+TEST 337: OK: Expected signal at tests/format/printf.c:390
 printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 338: OK: Expected signal at tests/format/printf.c:386
+TEST 338: OK: Expected signal at tests/format/printf.c:390
 printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 339: OK: Expected signal at tests/format/printf.c:387
+TEST 339: OK: Expected signal at tests/format/printf.c:391
 printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 340: OK: Expected signal at tests/format/printf.c:387
-TEST 341: OK: Expected execution at tests/format/printf.c:390
-TEST 342: OK: Expected execution at tests/format/printf.c:391
-TEST 343: OK: Expected execution at tests/format/printf.c:392
+TEST 340: OK: Expected signal at tests/format/printf.c:391
+TEST 341: OK: Expected execution at tests/format/printf.c:394
+TEST 342: OK: Expected execution at tests/format/printf.c:395
+TEST 343: OK: Expected execution at tests/format/printf.c:396
 printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 344: OK: Expected signal at tests/format/printf.c:393
+TEST 344: OK: Expected signal at tests/format/printf.c:397
 printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 345: OK: Expected signal at tests/format/printf.c:394
+TEST 345: OK: Expected signal at tests/format/printf.c:398
 printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 346: OK: Expected signal at tests/format/printf.c:395
+TEST 346: OK: Expected signal at tests/format/printf.c:399
 printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'char*'
-TEST 347: OK: Expected signal at tests/format/printf.c:396
-TEST 348: OK: Expected execution at tests/format/printf.c:399
+TEST 347: OK: Expected signal at tests/format/printf.c:400
+TEST 348: OK: Expected execution at tests/format/printf.c:403
 printf: directive 1 ('%lc') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 349: OK: Expected signal at tests/format/printf.c:400
-TEST 350: OK: Expected execution at tests/format/printf.c:407
-TEST 351: OK: Expected execution at tests/format/printf.c:408
+TEST 349: OK: Expected signal at tests/format/printf.c:404
+TEST 350: OK: Expected execution at tests/format/printf.c:411
+TEST 351: OK: Expected execution at tests/format/printf.c:412
 printf: directive 1 ('%s') expects argument of type 'char*' but the corresponding argument has type 'int'
-TEST 352: OK: Expected signal at tests/format/printf.c:409
+TEST 352: OK: Expected signal at tests/format/printf.c:413
 printf: directive 1 ('%s') expects argument of type 'char*' but the corresponding argument has type 'void*'
-TEST 353: OK: Expected signal at tests/format/printf.c:410
+TEST 353: OK: Expected signal at tests/format/printf.c:414
 printf: attempt to access unallocated memory via directive 1 ('%s')
-TEST 354: OK: Expected signal at tests/format/printf.c:415
+TEST 354: OK: Expected signal at tests/format/printf.c:419
 printf: attempt to access unallocated memory via directive 1 ('%s')
-TEST 355: OK: Expected signal at tests/format/printf.c:416
-TEST 356: OK: Expected execution at tests/format/printf.c:419
+TEST 355: OK: Expected signal at tests/format/printf.c:420
+TEST 356: OK: Expected execution at tests/format/printf.c:423
 printf: unterminated string in directive 1 ('%s')
-TEST 357: OK: Expected signal at tests/format/printf.c:421
-TEST 358: OK: Expected execution at tests/format/printf.c:424
-TEST 359: OK: Expected execution at tests/format/printf.c:425
-TEST 360: OK: Expected execution at tests/format/printf.c:426
-TEST 361: OK: Expected execution at tests/format/printf.c:427
+TEST 357: OK: Expected signal at tests/format/printf.c:425
+TEST 358: OK: Expected execution at tests/format/printf.c:428
+TEST 359: OK: Expected execution at tests/format/printf.c:429
+TEST 360: OK: Expected execution at tests/format/printf.c:430
+TEST 361: OK: Expected execution at tests/format/printf.c:431
 printf: attempt to access partially unallocated memory via directive 1 ('%.5s')
-TEST 362: OK: Expected signal at tests/format/printf.c:428
-TEST 363: OK: Expected execution at tests/format/printf.c:453
+TEST 362: OK: Expected signal at tests/format/printf.c:432
+TEST 363: OK: Expected execution at tests/format/printf.c:457
 printf: directive 1 ('%p') expects argument of type 'void*' but the corresponding argument has type 'char*'
-TEST 364: OK: Expected signal at tests/format/printf.c:454
+TEST 364: OK: Expected signal at tests/format/printf.c:458
 printf: argument 1 of directive %p not allocated
-TEST 365: OK: Expected signal at tests/format/printf.c:455
-TEST 366: OK: Expected execution at tests/format/printf.c:458
+TEST 365: OK: Expected signal at tests/format/printf.c:459
+TEST 366: OK: Expected execution at tests/format/printf.c:462
 printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding argument has type 'unsigned int*'
-TEST 367: OK: Expected signal at tests/format/printf.c:459
+TEST 367: OK: Expected signal at tests/format/printf.c:463
 printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding argument has type 'void*'
-TEST 368: OK: Expected signal at tests/format/printf.c:460
+TEST 368: OK: Expected signal at tests/format/printf.c:464
 printf: argument 0 of directive %n not allocated or writeable
-TEST 369: OK: Expected signal at tests/format/printf.c:461
+TEST 369: OK: Expected signal at tests/format/printf.c:465
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag ['] to format specifier [n]
-TEST 370: OK: Expected signal at tests/format/printf.c:464
+TEST 370: OK: Expected signal at tests/format/printf.c:468
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [0] to format specifier [n]
-TEST 371: OK: Expected signal at tests/format/printf.c:465
+TEST 371: OK: Expected signal at tests/format/printf.c:469
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of flag [#] to format specifier [n]
-TEST 372: OK: Expected signal at tests/format/printf.c:466
+TEST 372: OK: Expected signal at tests/format/printf.c:470
 Format error: one of more flags with [n] specifier
-TEST 373: OK: Expected signal at tests/format/printf.c:467
+TEST 373: OK: Expected signal at tests/format/printf.c:471
 Format error: one of more flags with [n] specifier
-TEST 374: OK: Expected signal at tests/format/printf.c:468
+TEST 374: OK: Expected signal at tests/format/printf.c:472
 Format error: one of more flags with [n] specifier
-TEST 375: OK: Expected signal at tests/format/printf.c:469
+TEST 375: OK: Expected signal at tests/format/printf.c:473
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
-TEST 376: OK: Expected signal at tests/format/printf.c:470
+TEST 376: OK: Expected signal at tests/format/printf.c:474
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
-TEST 377: OK: Expected signal at tests/format/printf.c:471
+TEST 377: OK: Expected signal at tests/format/printf.c:475
 FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:542: Format error: wrong application of precision [.] to format specifier [n]
-TEST 378: OK: Expected signal at tests/format/printf.c:472
+TEST 378: OK: Expected signal at tests/format/printf.c:476
 Format error: field width used with [n] specifier
-TEST 379: OK: Expected signal at tests/format/printf.c:473
+TEST 379: OK: Expected signal at tests/format/printf.c:477
 Format error: in directive '%d - %'% - %u times 
 '.the complete conversion specification for '%' is '%%'
-TEST 380: OK: Expected signal at tests/format/printf.c:476
+TEST 380: OK: Expected signal at tests/format/printf.c:480
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index b17069423578bbc19bb51f6d5e1bb9f688600035..26ede76d5fd85381070a041c6a34ac33840fe0a3 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -35,30 +35,31 @@
   function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:351: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:352: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:350: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:357: Warning: 
   function __gen_e_acsl_fread: postcondition 'initialization' got status unknown.
 [eva:alarm] tests/libc/file.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/libc/file.c:15: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/file.c:18: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/file.c:18: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/file.c:21: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/file.c:21: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/file.c:24: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/file.c:24: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/file.c:27: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/file.c:27: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/file.c:35: Warning: 
   function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
 [eva:alarm] tests/libc/file.c:37: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/file.c:37: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
index 83a5336a5de84fcd4e8449d822bf3bf7dcb3c3b4..218f631f75fdad170fc5d433dd7a2b5c94346209 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -43,7 +43,7 @@
 [eva:alarm] FRAMAC_SHARE/libc/string.h:134: Warning: 
   function __gen_e_acsl_memset: postcondition 'acsl_c_equiv' got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/string.h:101: Warning: 
   function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/string.h:124: Warning: 
diff --git a/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
index 11886784cadfea1cfd21c4893ef612d4c0e920a0..e477cc3d8212ab45c130b864f2ea26044a9e2607 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/sprintf.res.oracle
@@ -1,15 +1,20 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/libc/sprintf.c:13: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/sprintf.c:13: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/sprintf.c:14: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/sprintf.c:14: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/sprintf.c:21: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/sprintf.c:21: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/sprintf.c:22: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/libc/sprintf.c:22: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/sprintf.c:29: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/sprintf.c:29: Warning: assertion got status unknown.
 [eva:alarm] tests/libc/sprintf.c:30: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/sprintf.c:30: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
index 7bc785549f1a43e39bb37cdc46f62eca4b9c51e6..968679a56bfa6d106020403e352f258ad6d52820 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -141,4 +141,5 @@
 [eva:alarm] FRAMAC_SHARE/libc/string.h:373: Warning: 
   function __gen_e_acsl_strcpy: postcondition 'equal_contents' got status unknown.
 [eva:alarm] tests/libc/str.c:16: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/libc/str.c:16: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
index 689b7d855d85362d62e30c17ccee6538958bbda9..fdba473d4631aece519dc1b89be945396293d7ae 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
@@ -1,10 +1,14 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/block_valid.c:49: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/block_valid.c:50: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/block_valid.c:52: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/block_valid.c:52: Warning: 
   assertion got status unknown.
 [eva:alarm] tests/memory/block_valid.c:54: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/block_valid.c:54: Warning: 
   assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
index 72d8d0685d14f5e77f6e60be928e447d25c13a6c..61c8808202551d230a623137e95c4c4d451bbc86 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
@@ -21,12 +21,12 @@ int __gen_e_acsl_main(int argc, char **argv)
   int i;
   {
     int __gen_e_acsl_forall;
-    int __gen_e_acsl_k;
+    long __gen_e_acsl_k;
     __e_acsl_store_block((void *)(& argv),(size_t)8);
     __gen_e_acsl_forall = 1;
     __gen_e_acsl_k = 0;
     while (1) {
-      if (__gen_e_acsl_k < argc) ; else break;
+      if (__gen_e_acsl_k <= (long)argc) ; else break;
       {
         int __gen_e_acsl_valid;
         __gen_e_acsl_valid = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
@@ -42,10 +42,10 @@ int __gen_e_acsl_main(int argc, char **argv)
     }
     e_acsl_end_loop1: ;
     __e_acsl_assert(__gen_e_acsl_forall,1,"Assertion","main",
-                    "\\forall int k; 0 <= k < argc ==> \\valid(argv + k)",
+                    "\\forall int k; 0 <= k <= argc ==> \\valid(argv + k)",
                     "tests/memory/mainargs.c",12);
   }
-  /*@ assert ∀ int k; 0 ≤ k < argc ⇒ \valid(argv + k); */ ;
+  /*@ assert ∀ int k; 0 ≤ k ≤ argc ⇒ \valid(argv + k); */ ;
   {
     unsigned long __gen_e_acsl_block_length;
     __e_acsl_mpz_t __gen_e_acsl_block_length_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
index 8140477968bc3dc5a5630a28cf40be6698728164..4b7d6f59edd5e7d8248ce0cc155f8ef95f2dd407 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
@@ -29,39 +29,39 @@ int main(void)
     }
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,1,"RTE","main",
-                    "mem_access: \\valid_read(p)","tests/memory/ptr.i",11);
+                    "mem_access: \\valid_read(p)","tests/memory/ptr.i",12);
     __e_acsl_assert(*p == 1,1,"Assertion","main","*p == 1",
-                    "tests/memory/ptr.i",11);
+                    "tests/memory/ptr.i",12);
   }
   /*@ assert *p ≡ 1; */ ;
   __e_acsl_assert(t[0] == 2,1,"Assertion","main","t[0] == 2",
-                  "tests/memory/ptr.i",12);
+                  "tests/memory/ptr.i",13);
   /*@ assert t[0] ≡ 2; */ ;
   __e_acsl_assert(t[2] == 4,1,"Assertion","main","t[2] == 4",
-                  "tests/memory/ptr.i",13);
+                  "tests/memory/ptr.i",14);
   /*@ assert t[2] ≡ 4; */ ;
   __e_acsl_assert(t[2] == 4,1,"Assertion","main",
                   "t[(2 * sizeof(int)) / sizeof((int)0x0)] == 4",
-                  "tests/memory/ptr.i",14);
+                  "tests/memory/ptr.i",15);
   /*@ assert t[(2 * sizeof(int)) / sizeof((int)0x0)] ≡ 4; */ ;
   {
     int i = 0;
     while (i < 2) {
       __e_acsl_assert(i < 3,1,"RTE","main","index_bound: i < 3",
-                      "tests/memory/ptr.i",17);
+                      "tests/memory/ptr.i",18);
       __e_acsl_assert(0 <= i,1,"RTE","main","index_bound: 0 <= i",
-                      "tests/memory/ptr.i",17);
+                      "tests/memory/ptr.i",18);
       __e_acsl_assert((long)t[i] == i + 2L,1,"Assertion","main",
-                      "t[i] == i + 2","tests/memory/ptr.i",17);
+                      "t[i] == i + 2","tests/memory/ptr.i",18);
       /*@ assert t[i] ≡ i + 2; */ ;
       __e_acsl_assert(2L - i < 3L,1,"RTE","main",
                       "index_bound: (long)(2 - i) < 3","tests/memory/ptr.i",
-                      18);
+                      19);
       __e_acsl_assert(0L <= 2L - i,1,"RTE","main",
                       "index_bound: 0 <= (long)(2 - i)","tests/memory/ptr.i",
-                      18);
+                      19);
       __e_acsl_assert((long)t[2L - i] == 4L - i,1,"Assertion","main",
-                      "t[2 - i] == 4 - i","tests/memory/ptr.i",18);
+                      "t[2 - i] == 4 - i","tests/memory/ptr.i",19);
       /*@ assert t[2 - i] ≡ 4 - i; */ ;
       {
         int __gen_e_acsl_valid_read_2;
@@ -71,9 +71,9 @@ int main(void)
                                                         (void *)0);
         __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","main",
                         "mem_access: \\valid_read(&t[2] - i)",
-                        "tests/memory/ptr.i",19);
+                        "tests/memory/ptr.i",20);
         __e_acsl_assert((long)*(& t[2] - i) == 4L - i,1,"Assertion","main",
-                        "*(&t[2] - i) == 4 - i","tests/memory/ptr.i",19);
+                        "*(&t[2] - i) == 4 - i","tests/memory/ptr.i",20);
       }
       /*@ assert *(&t[2] - i) ≡ 4 - i; */ ;
       i ++;
@@ -97,9 +97,9 @@ int main(void)
     }
     else __gen_e_acsl_and_2 = 0;
     __e_acsl_assert(__gen_e_acsl_and_2,1,"RTE","main",
-                    "mem_access: \\valid_read(p)","tests/memory/ptr.i",25);
+                    "mem_access: \\valid_read(p)","tests/memory/ptr.i",26);
     __e_acsl_assert(*p == 5,1,"Assertion","main","*p == 5",
-                    "tests/memory/ptr.i",25);
+                    "tests/memory/ptr.i",26);
   }
   /*@ assert *p ≡ 5; */ ;
   int k = -1;
@@ -110,9 +110,9 @@ int main(void)
                                                     (void *)(& p));
     __e_acsl_assert(__gen_e_acsl_valid_read_4,1,"RTE","main",
                     "mem_access: \\valid_read(p + k)","tests/memory/ptr.i",
-                    27);
+                    28);
     __e_acsl_assert(*(p + k) == 3,1,"Assertion","main","*(p + k) == 3",
-                    "tests/memory/ptr.i",27);
+                    "tests/memory/ptr.i",28);
   }
   /*@ assert *(p + k) ≡ 3; */ ;
   __retres = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
index 152d6087e0c65af8113b81075ad7742310cf426b..a2f4abc18eb4c03a7f5809535b8d75be25b939b4 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
@@ -62,7 +62,7 @@ int main(void)
                                         (void *)(& a));
     __e_acsl_assert(__gen_e_acsl_valid,1,"Assertion","main",
                     "\\valid(a + (0 .. 4))",
-                    "tests/memory/ranges_in_builtins.c",19);
+                    "tests/memory/ranges_in_builtins.c",20);
   }
   /*@ assert \valid(a + (0 .. 4)); */ ;
   int j = 2;
@@ -78,7 +78,7 @@ int main(void)
                                           (void *)a,(void *)(& a));
     __e_acsl_assert(__gen_e_acsl_valid_2,1,"Assertion","main",
                     "\\valid(a + (4 .. 7 + j))",
-                    "tests/memory/ranges_in_builtins.c",21);
+                    "tests/memory/ranges_in_builtins.c",22);
   }
   /*@ assert \valid(a + (4 .. 7 + j)); */ ;
   {
@@ -93,7 +93,7 @@ int main(void)
                                           (void *)a,(void *)(& a));
     __e_acsl_assert(! __gen_e_acsl_valid_3,1,"Assertion","main",
                     "!\\valid(a + (10 .. 11))",
-                    "tests/memory/ranges_in_builtins.c",22);
+                    "tests/memory/ranges_in_builtins.c",23);
   }
   /*@ assert ¬\valid(a + (10 .. 11)); */ ;
   free((void *)a);
@@ -111,7 +111,7 @@ int main(void)
                                           (void *)b,(void *)(& b));
     __e_acsl_assert(__gen_e_acsl_valid_4,1,"Assertion","main",
                     "\\valid(b + (0 .. 9))",
-                    "tests/memory/ranges_in_builtins.c",27);
+                    "tests/memory/ranges_in_builtins.c",28);
   }
   /*@ assert \valid(b + (0 .. 9)); */ ;
   {
@@ -126,7 +126,7 @@ int main(void)
                                           (void *)b,(void *)(& b));
     __e_acsl_assert(! __gen_e_acsl_valid_5,1,"Assertion","main",
                     "!\\valid(b + (10 .. 15))",
-                    "tests/memory/ranges_in_builtins.c",28);
+                    "tests/memory/ranges_in_builtins.c",29);
   }
   /*@ assert ¬\valid(b + (10 .. 15)); */ ;
   long t[3] = {7l, 8l, 9l};
@@ -144,7 +144,7 @@ int main(void)
                                           (void *)(t),(void *)0);
     __e_acsl_assert(__gen_e_acsl_valid_6,1,"Assertion","main",
                     "\\valid(&t[0 .. 2])",
-                    "tests/memory/ranges_in_builtins.c",31);
+                    "tests/memory/ranges_in_builtins.c",32);
   }
   /*@ assert \valid(&t[0 .. 2]); */ ;
   {
@@ -159,7 +159,7 @@ int main(void)
                                           (void *)(t),(void *)0);
     __e_acsl_assert(! __gen_e_acsl_valid_7,1,"Assertion","main",
                     "!\\valid(&t[3 .. 5])",
-                    "tests/memory/ranges_in_builtins.c",32);
+                    "tests/memory/ranges_in_builtins.c",33);
   }
   /*@ assert ¬\valid(&t[3 .. 5]); */ ;
   __gen_e_acsl_g(t,(unsigned long)3);
@@ -179,7 +179,7 @@ int main(void)
                                                     (size_t)__gen_e_acsl_if_8);
     __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
                     "\\initialized(&t2[0 .. 1])",
-                    "tests/memory/ranges_in_builtins.c",38);
+                    "tests/memory/ranges_in_builtins.c",39);
   }
   /*@ assert \initialized(&t2[0 .. 1]); */ ;
   {
@@ -194,7 +194,7 @@ int main(void)
                                                       (size_t)__gen_e_acsl_if_9);
     __e_acsl_assert(! __gen_e_acsl_initialized_2,1,"Assertion","main",
                     "!\\initialized(&t2[2 .. 3])",
-                    "tests/memory/ranges_in_builtins.c",39);
+                    "tests/memory/ranges_in_builtins.c",40);
   }
   /*@ assert ¬\initialized(&t2[2 .. 3]); */ ;
   {
@@ -208,7 +208,7 @@ int main(void)
                                                       (size_t)__gen_e_acsl_if_10);
     __e_acsl_assert(! __gen_e_acsl_initialized_3,1,"Assertion","main",
                     "!\\initialized(b + (0 .. 9))",
-                    "tests/memory/ranges_in_builtins.c",41);
+                    "tests/memory/ranges_in_builtins.c",42);
   }
   /*@ assert ¬\initialized(b + (0 .. 9)); */ ;
   free((void *)b);
@@ -251,7 +251,7 @@ int main(void)
     e_acsl_end_loop2: ;
     __e_acsl_assert(! __gen_e_acsl_forall,1,"Assertion","main",
                     "!\\initialized(&t3[n - 1 .. n + 2][1][0 .. 1])",
-                    "tests/memory/ranges_in_builtins.c",46);
+                    "tests/memory/ranges_in_builtins.c",47);
   }
   /*@ assert ¬\initialized(&t3[n - 1 .. n + 2][1][0 .. 1]); */ ;
   {
@@ -268,7 +268,7 @@ int main(void)
                                                   (void *)0);
     __e_acsl_assert(! __gen_e_acsl_valid_read,1,"Assertion","main",
                     "!\\valid_read(&t3[6][1][0] + (2 .. 10))",
-                    "tests/memory/ranges_in_builtins.c",48);
+                    "tests/memory/ranges_in_builtins.c",49);
   }
   /*@ assert ¬\valid_read(&t3[6][1][0] + (2 .. 10)); */ ;
   {
@@ -295,7 +295,7 @@ int main(void)
     e_acsl_end_loop3: ;
     __e_acsl_assert(__gen_e_acsl_forall_3,1,"Assertion","main",
                     "\\valid_read(&t3[n - 1 .. n + 2][1])",
-                    "tests/memory/ranges_in_builtins.c",49);
+                    "tests/memory/ranges_in_builtins.c",50);
   }
   /*@ assert \valid_read(&t3[n - 1 .. n + 2][1]); */ ;
   {
@@ -324,7 +324,7 @@ int main(void)
     e_acsl_end_loop4: ;
     __e_acsl_assert(__gen_e_acsl_forall_4,1,"Assertion","main",
                     "\\let x = 5; \\valid(&t4[4][0 .. x][2])",
-                    "tests/memory/ranges_in_builtins.c",52);
+                    "tests/memory/ranges_in_builtins.c",53);
   }
   /*@ assert \let x = 5; \valid(&t4[4][0 .. x][2]); */ ;
   __e_acsl_initialize((void *)(& s.a[0]),sizeof(int));
@@ -343,7 +343,7 @@ int main(void)
                                                       (size_t)__gen_e_acsl_if_12);
     __e_acsl_assert(__gen_e_acsl_initialized_5,1,"Assertion","main",
                     "\\initialized(&s.a[0] + (1 .. 1))",
-                    "tests/memory/ranges_in_builtins.c",56);
+                    "tests/memory/ranges_in_builtins.c",57);
   }
   /*@ assert \initialized(&s.a[0] + (1 .. 1)); */ ;
   {
@@ -359,7 +359,7 @@ int main(void)
                                                       (size_t)__gen_e_acsl_if_13);
     __e_acsl_assert(! __gen_e_acsl_initialized_6,1,"Assertion","main",
                     "!\\initialized(s.b + (0 .. 1))",
-                    "tests/memory/ranges_in_builtins.c",57);
+                    "tests/memory/ranges_in_builtins.c",58);
   }
   /*@ assert ¬\initialized(s.b + (0 .. 1)); */ ;
   int size1 = 5;
@@ -384,7 +384,7 @@ int main(void)
                                                     (void *)(& multi_dynamic));
     __e_acsl_assert(__gen_e_acsl_valid_read_3,1,"RTE","main",
                     "mem_access: \\valid_read(multi_dynamic + 4)",
-                    "tests/memory/ranges_in_builtins.c",66);
+                    "tests/memory/ranges_in_builtins.c",67);
     __gen_e_acsl_size_14 = 4 * ((7 - 1) + 1);
     if (__gen_e_acsl_size_14 <= 0) __gen_e_acsl_if_14 = 0;
     else __gen_e_acsl_if_14 = __gen_e_acsl_size_14;
@@ -395,7 +395,7 @@ int main(void)
                                           (void *)(multi_dynamic + 4));
     __e_acsl_assert(__gen_e_acsl_valid_9,1,"Assertion","main",
                     "\\valid(*(multi_dynamic + 4) + (1 .. 7))",
-                    "tests/memory/ranges_in_builtins.c",66);
+                    "tests/memory/ranges_in_builtins.c",67);
   }
   /*@ assert \valid(*(multi_dynamic + 4) + (1 .. 7)); */ ;
   /*@ assert \valid(*(multi_dynamic + (2 .. 4)) + (1 .. 7)); */ ;
@@ -424,7 +424,7 @@ int main(void)
                                            (void *)(t5),(void *)0);
     __e_acsl_assert(__gen_e_acsl_valid_10,1,"Assertion","main",
                     "\\valid(&t5[2 .. 3])",
-                    "tests/memory/ranges_in_builtins.c",78);
+                    "tests/memory/ranges_in_builtins.c",79);
   }
   /*@ assert \valid(&t5[2 .. 3]); */ ;
   __retres = 0;
@@ -504,14 +504,14 @@ void __gen_e_acsl_g(long *ptr, size_t size)
                                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
     __e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","g",
                     "offset_lesser_or_eq_than_SIZE_MAX:\n  (\\let size = sizeof(long) * (((size - 1) - 0) + 1); size <= 0? 0: size) <=\n  18446744073709551615",
-                    "tests/memory/ranges_in_builtins.c",7);
+                    "tests/memory/ranges_in_builtins.c",8);
     __gen_e_acsl_size_3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
     __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)ptr + 8 * 0),
                                         __gen_e_acsl_size_3,(void *)ptr,
                                         (void *)(& ptr));
     __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","g",
                     "\\valid(ptr + (0 .. size - 1))",
-                    "tests/memory/ranges_in_builtins.c",7);
+                    "tests/memory/ranges_in_builtins.c",8);
     __gmpz_clear(__gen_e_acsl_size);
     __gmpz_clear(__gen_e_acsl_sizeof);
     __gmpz_clear(__gen_e_acsl_size_2);
@@ -585,7 +585,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
                                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
     __e_acsl_assert(__gen_e_acsl_le_4 <= 0,1,"RTE","g",
                     "offset_lesser_or_eq_than_SIZE_MAX:\n  (\\let size = sizeof(long) * (((\\old(size) + 1) - 0) + 1);\n   size <= 0? 0: size)\n  <= 18446744073709551615",
-                    "tests/memory/ranges_in_builtins.c",8);
+                    "tests/memory/ranges_in_builtins.c",9);
     __gen_e_acsl_size_6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
     __gen_e_acsl_valid_2 = __e_acsl_valid((void *)((char *)__gen_e_acsl_at + 
                                                    8 * 0),
@@ -594,7 +594,7 @@ void __gen_e_acsl_g(long *ptr, size_t size)
                                           (void *)(& __gen_e_acsl_at));
     __e_acsl_assert(! __gen_e_acsl_valid_2,1,"Postcondition","g",
                     "!\\valid(\\old(ptr) + (0 .. \\old(size) + 1))",
-                    "tests/memory/ranges_in_builtins.c",8);
+                    "tests/memory/ranges_in_builtins.c",9);
     __e_acsl_delete_block((void *)(& ptr));
     __gmpz_clear(__gen_e_acsl_size_4);
     __gmpz_clear(__gen_e_acsl_sizeof_2);
@@ -673,14 +673,14 @@ void __gen_e_acsl_f(char *s, long n)
                                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
     __e_acsl_assert(__gen_e_acsl_le_2 <= 0,1,"RTE","f",
                     "offset_lesser_or_eq_than_SIZE_MAX:\n  (\\let size = sizeof(char) * (((n + 1000) - 3) + 1); size <= 0? 0: size) <=\n  18446744073709551615",
-                    "tests/memory/ranges_in_builtins.c",5);
+                    "tests/memory/ranges_in_builtins.c",6);
     __gen_e_acsl_size_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
     __gen_e_acsl_valid = __e_acsl_valid((void *)(s + 1 * 3),
                                         __gen_e_acsl_size_2,(void *)s,
                                         (void *)(& s));
     __e_acsl_assert(! __gen_e_acsl_valid,1,"Precondition","f",
                     "!\\valid(s + (3 .. n + 1000))",
-                    "tests/memory/ranges_in_builtins.c",5);
+                    "tests/memory/ranges_in_builtins.c",6);
     __gmpz_clear(__gen_e_acsl_size);
     __gmpz_clear(__gen_e_acsl_sizeof);
     __gmpz_clear(__gen_e_acsl_n);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
index f522a84f1dc6d5c40dff444831cf795f4ab12930..f35eefe1d62032a0d7b35743ac9a0fc8150430d6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
@@ -45,7 +45,7 @@ int *new_inversed(int len, int *v)
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","new_inversed",
                     "\\valid(v) && \\offset(v) + len * sizeof(int) <= \\block_length(v)",
-                    "tests/memory/vector.c",11);
+                    "tests/memory/vector.c",12);
   }
   /*@
   assert \valid(v) ∧ \offset(v) + len * sizeof(int) ≤ \block_length(v);
@@ -79,7 +79,7 @@ int main(void)
     __gen_e_acsl_valid = __e_acsl_valid((void *)(& v1[2]),sizeof(int),
                                         (void *)(v1),(void *)0);
     __e_acsl_assert(__gen_e_acsl_valid,1,"Assertion","main",
-                    "\\valid(&v1[2])","tests/memory/vector.c",21);
+                    "\\valid(&v1[2])","tests/memory/vector.c",22);
   }
   /*@ assert \valid(&v1[2]); */ ;
   LAST = v1[2];
@@ -88,7 +88,7 @@ int main(void)
     __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& v1[2]),
                                                     sizeof(int));
     __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main",
-                    "\\initialized(&v1[2])","tests/memory/vector.c",23);
+                    "\\initialized(&v1[2])","tests/memory/vector.c",24);
   }
   /*@ assert \initialized(&v1[2]); */ ;
   __e_acsl_full_init((void *)(& v2));
@@ -99,11 +99,11 @@ int main(void)
     __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(v2 + 2),
                                                       sizeof(int));
     __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main",
-                    "\\initialized(v2 + 2)","tests/memory/vector.c",26);
+                    "\\initialized(v2 + 2)","tests/memory/vector.c",27);
   }
   /*@ assert \initialized(v2 + 2); */ ;
   __e_acsl_assert(LAST == 1,1,"Assertion","main","LAST == 1",
-                  "tests/memory/vector.c",27);
+                  "tests/memory/vector.c",28);
   /*@ assert LAST ≡ 1; */ ;
   free((void *)v2);
   __retres = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
index 2816887b72ce54bfe6226cf6fbca9b0d33dfb3fe..76649cc1f80bb48ea6bafd00cfe0f5c5add09a48 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
@@ -27,7 +27,7 @@ int main(int argc, char **argv)
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","main",
                     "alloca_bounds: 0 < sizeof(int) * LEN <= 18446744073709551615",
-                    "tests/memory/vla.c",8);
+                    "tests/memory/vla.c",9);
   }
   /*@ assert alloca_bounds: 0 < sizeof(int) * LEN ≤ 18446744073709551615;
    */
@@ -45,7 +45,7 @@ int main(int argc, char **argv)
         __gen_e_acsl_valid = __e_acsl_valid((void *)(arr + i),sizeof(int),
                                             (void *)arr,(void *)(& arr));
         __e_acsl_assert(__gen_e_acsl_valid,1,"Assertion","main",
-                        "\\valid(arr + i)","tests/memory/vla.c",12);
+                        "\\valid(arr + i)","tests/memory/vla.c",13);
       }
       /*@ assert \valid(arr + i); */ ;
     }
@@ -55,7 +55,7 @@ int main(int argc, char **argv)
         __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(arr + i),sizeof(int),
                                               (void *)arr,(void *)(& arr));
         __e_acsl_assert(! __gen_e_acsl_valid_2,1,"Assertion","main",
-                        "!\\valid(arr + i)","tests/memory/vla.c",14);
+                        "!\\valid(arr + i)","tests/memory/vla.c",15);
       }
       /*@ assert ¬\valid(arr + i); */ ;
     }
diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
index b8c20257c0db0f6d12c68721ef27c04f01360e40..338fa0d580e133b8b5c781cef207958f72e9b552 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
@@ -19,24 +19,22 @@
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/memory/mainargs.c:12: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:12: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/mainargs.c:13: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:13: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/mainargs.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:15: Warning: 
   out of bounds read. assert \valid_read(argv + argc);
-[eva:alarm] tests/memory/mainargs.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:15: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/mainargs.c:16: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:16: Warning: 
   out of bounds read. assert \valid_read(argv + argc);
 [eva:alarm] tests/memory/mainargs.c:16: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:16: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/mainargs.c:18: Warning: 
   function __gen_e_acsl_strlen: precondition 'valid_string_s' got status unknown.
@@ -45,8 +43,8 @@
 [eva:alarm] FRAMAC_SHARE/libc/string.h:143: Warning: 
   function __gen_e_acsl_strlen: postcondition 'acsl_c_equiv' got status unknown.
 [eva:alarm] tests/memory/mainargs.c:19: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:19: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/mainargs.c:20: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/mainargs.c:20: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
index 1c942fd837e8066e8d5ee869ce6051ed1308b305..177750cc1b5a35d97866594ce2f87fe414a5d7c5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
@@ -1,18 +1,16 @@
 [e-acsl] beginning translation.
-[e-acsl] tests/memory/ranges_in_builtins.c:67: Warning: 
+[e-acsl] tests/memory/ranges_in_builtins.c:68: Warning: 
   E-ACSL construct `arithmetic over set of pointers or arrays'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/ranges_in_builtins.c:7: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/memory/ranges_in_builtins.c:7: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/memory/ranges_in_builtins.c:8: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/memory/ranges_in_builtins.c:52: Warning: 
+[eva:alarm] tests/memory/ranges_in_builtins.c:9: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:9: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/ranges_in_builtins.c:53: Warning: 
   assertion got status unknown.
-[eva:alarm] tests/memory/ranges_in_builtins.c:57: Warning: 
+[eva:alarm] tests/memory/ranges_in_builtins.c:58: Warning: 
   accessing uninitialized left-value. assert \initialized(&s.b);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle
index a7fcc9e1936f864da954d3e794a5353a8c253cda..abcde03efaf9e4767e86147f9b2ac40f4c5aa3ad 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle
@@ -1,58 +1,52 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/memory/separated.c:14: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:21: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:22: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:23: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:24: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:25: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:26: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:27: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:36: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:37: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:46: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:47: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:48: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:49: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:50: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:51: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:52: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/memory/separated.c:60: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:60: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:61: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] tests/memory/separated.c:61: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/memory/separated.c:62: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] tests/memory/separated.c:62: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:62: Warning: assertion got status unknown.
-[eva:alarm] tests/memory/separated.c:63: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
 [eva:alarm] tests/memory/separated.c:63: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:63: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/separated.c:63: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/separated.c:64: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
index 79a52ff2ddcb8bc2851df1be752f7430e2cb9a49..0aaf460e7936d9bbbe4c61c83a1fd0c8a5db71ea 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
@@ -1,11 +1,11 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/memory/stdout.c:8: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/stdout.c:8: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/stdout.c:9: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/stdout.c:9: Warning: assertion got status unknown.
 [eva:alarm] tests/memory/stdout.c:10: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/memory/stdout.c:10: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
index 62cadf38b70123632d864225a66ffaeeda77503a..7c772edc7d68123d8d7bf560b2b9f2be246e513a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
@@ -1,4 +1,4 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/vector.c:11: Warning: 
+[eva:alarm] tests/memory/vector.c:12: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
index 9ab440d9473aa89b0a64b109452dc12e499ab0e2..bbabb8e52c514a69429c33990bb30604c23d7907 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
@@ -1,4 +1,4 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/vla.c:8: Warning: 
+[eva:alarm] tests/memory/vla.c:9: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
index 2c2f479abd8ae3c4f16bd78bcd19837fdac4fa00..f24c001c7e29db2bb32513318a30564fb2da30c3 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
@@ -1,4 +1,4 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/special/e-acsl-functions.c:31: Warning: 
+[eva:alarm] tests/special/e-acsl-functions.c:36: Warning: 
   function g: precondition *p ≡ 1 got status invalid.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
index 53b0044b3238c5ffb4eb8025aba47338062d3cb9..44b32fb0b13f0699b87c1da69c93901bee899264 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
@@ -21,7 +21,7 @@ int main(void)
       __gen_e_acsl_valid = __e_acsl_valid((void *)(p + i),sizeof(int *),
                                           (void *)p,(void *)(& p));
       __e_acsl_assert(__gen_e_acsl_valid,1,"Assertion","main",
-                      "\\valid(p + i)","tests/temporal/t_dpointer.c",12);
+                      "\\valid(p + i)","tests/temporal/t_dpointer.c",13);
     }
     /*@ assert \valid(p + i); */ ;
     __e_acsl_initialize((void *)(p + i),sizeof(int *));
@@ -43,7 +43,7 @@ int main(void)
                                                       (void *)(& p));
         __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","main",
                         "mem_access: \\valid_read(p + i)",
-                        "tests/temporal/t_dpointer.c",14);
+                        "tests/temporal/t_dpointer.c",15);
         __gen_e_acsl_valid_2 = __e_acsl_valid((void *)*(p + i),sizeof(int),
                                               (void *)*(p + i),
                                               (void *)(p + i));
@@ -51,7 +51,7 @@ int main(void)
       }
       else __gen_e_acsl_and = 0;
       __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","main",
-                      "\\valid(*(p + i))","tests/temporal/t_dpointer.c",14);
+                      "\\valid(*(p + i))","tests/temporal/t_dpointer.c",15);
     }
     /*@ assert \valid(*(p + i)); */ ;
     i ++;
@@ -77,7 +77,7 @@ int main(void)
                                                       (void *)(& p));
       __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","main",
                       "mem_access: \\valid_read(p + 2)",
-                      "tests/temporal/t_dpointer.c",20);
+                      "tests/temporal/t_dpointer.c",21);
       /*@ assert Eva: dangling_pointer: ¬\dangling(p + 2); */
       __gen_e_acsl_valid_3 = __e_acsl_valid((void *)*(p + 2),sizeof(int),
                                             (void *)*(p + 2),(void *)(
@@ -86,7 +86,7 @@ int main(void)
     }
     else __gen_e_acsl_and_2 = 0;
     __e_acsl_assert(! __gen_e_acsl_and_2,1,"Assertion","main",
-                    "!\\valid(*(p + 2))","tests/temporal/t_dpointer.c",20);
+                    "!\\valid(*(p + 2))","tests/temporal/t_dpointer.c",21);
   }
   /*@ assert ¬\valid(*(p + 2)); */ ;
   __retres = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index c46be04e1a5f209abe3710a60d6f3dde50d82eb0..4fba571813a17b49f10b9f97e17d13f2a01bb565 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -34,7 +34,7 @@ int main(void)
       }
       else __gen_e_acsl_and = 0;
       __e_acsl_assert(__gen_e_acsl_and,1,"Assertion","main","\\valid(q)",
-                      "tests/temporal/t_while.c",28);
+                      "tests/temporal/t_while.c",29);
     }
     /*@ assert \valid(q); */ ;
     __e_acsl_initialize((void *)q,sizeof(int));
@@ -57,7 +57,7 @@ int main(void)
     }
     else __gen_e_acsl_and_2 = 0;
     __e_acsl_assert(! __gen_e_acsl_and_2,1,"Assertion","main","!\\valid(q)",
-                    "tests/temporal/t_while.c",36);
+                    "tests/temporal/t_while.c",37);
   }
   /*@ assert ¬\valid(q); */ ;
   __retres = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
index b6037f9ecb8ff9165b9d38cbed61f26783ec60be..d1a7d5a008bb05cfa2c8986371a0fd2c9312b9c5 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
@@ -1,7 +1,7 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/temporal/t_args.c:9: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/temporal/t_args.c:9: Warning: assertion got status unknown.
 [eva:alarm] tests/temporal/t_args.c:10: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
index 1b3d9def751b087648e1413b9ff0a064ba1a7beb..be99b03ac0e2a4d60f8dd1374232a3bab4b5229c 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
@@ -1,11 +1,11 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/temporal/t_dpointer.c:14: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/temporal/t_dpointer.c:20: Warning: 
+[eva:alarm] tests/temporal/t_dpointer.c:15: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:21: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(p + 2);
-[eva:alarm] tests/temporal/t_dpointer.c:20: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
-[eva:alarm] tests/temporal/t_dpointer.c:20: Warning: 
+[eva:alarm] tests/temporal/t_dpointer.c:21: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/temporal/t_dpointer.c:21: Warning: 
   assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index aadcdf72e067db0cf2a7de97042b9d0162805b10..90c9c2ce8328b0b0f4f36de3c7a1534a55454544 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -15,12 +15,12 @@
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning: 
   function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
 [eva:alarm] tests/temporal/t_getenv.c:14: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
 [eva:alarm] tests/temporal/t_getenv.c:15: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 9eaa9235534b4443a58d74e7e9d5122ffa202ca0..cb751d8a0f1ffbade8c51b16888393ebb55839e4 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -26,7 +26,7 @@
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status invalid.
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/string.h:101: Warning: 
   function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/string.h:134: Warning: