diff --git a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
index 482ab448a925f729a070d9dd2fae978030386513..3fcbe6979c0408e461a31fcabe4acf5d8d0a67f8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
@@ -60,38 +60,38 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:21: Warning: 
   assertion got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning: 
-  signed overflow.
-  assert __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:24: Warning: 
-  assertion got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
   signed overflow.
-  assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+  assert __gen_e_acsl_k_10 + __gen_e_acsl_one_10 ≤ 2147483647;
 [eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:25: Warning: 
   assertion got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
   signed overflow.
-  assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+  assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
 [eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:26: Warning: 
   assertion got status unknown.
 [eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
-  signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+  signed overflow.
+  assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
 [eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+  signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
   signed overflow.
   assert __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning: 
   signed overflow. assert 2 * __gen_e_acsl_k_16 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
+[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning: 
   signed overflow.
   assert __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
-[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning: 
+[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning: 
   assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 9ce1b434c485160e05fdb10d8e60635435748e0d..0dc365800f3a322f927c8f285959f3d817a014eb 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -398,7 +398,7 @@ int main(void)
                                  (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
     __e_acsl_assert(__gen_e_acsl_ge >= 0,1,"Assertion","main",
                     "\\product(1, 100, \\lambda integer k; k) >= 3628800",
-                    "tests/arith/extended_quantifiers.c",24);
+                    "tests/arith/extended_quantifiers.c",25);
     __gmpz_clear(__gen_e_acsl_lambda_10);
     __gmpz_clear(__gen_e_acsl_accumulator_10);
     __gmpz_clear(__gen_e_acsl__7);
@@ -431,7 +431,7 @@ int main(void)
     __e_acsl_assert(__gen_e_acsl_accumulator_11 == 3628800UL,1,"Assertion",
                     "main",
                     "\\product(1, 10, \\lambda integer k; k) == 3628800",
-                    "tests/arith/extended_quantifiers.c",25);
+                    "tests/arith/extended_quantifiers.c",26);
   }
   /*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
   {
@@ -473,7 +473,7 @@ int main(void)
                                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
     __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main",
                     "\\product(-10, 10, \\lambda integer k; k) == 0",
-                    "tests/arith/extended_quantifiers.c",26);
+                    "tests/arith/extended_quantifiers.c",27);
     __gmpz_clear(__gen_e_acsl_lambda_12);
     __gmpz_clear(__gen_e_acsl_accumulator_12);
     __gmpz_clear(__gen_e_acsl__8);
@@ -553,7 +553,7 @@ int main(void)
                                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_14));
     __e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
                     "\\product(-20, -1, \\lambda integer k; 2 * k) ==\n\\product(1, 20, \\lambda integer k; 2 * k)",
-                    "tests/arith/extended_quantifiers.c",27);
+                    "tests/arith/extended_quantifiers.c",28);
     __gmpz_clear(__gen_e_acsl_lambda_13);
     __gmpz_clear(__gen_e_acsl_accumulator_13);
     __gmpz_clear(__gen_e_acsl_lambda_14);