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 c5f401dc6b87195d387f73cf20996261f7a061ca..217df1e0d43af0579fd78e3308f5841c998d066c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
@@ -204,6 +204,36 @@ int main(void)
       \lambda ℤ k; 1)
   ≡ 6; */
   ;
+  {
+    unsigned int __gen_e_acsl_k_6;
+    unsigned int __gen_e_acsl_one_6;
+    int __gen_e_acsl_cond_6;
+    int __gen_e_acsl_lambda_6;
+    int __gen_e_acsl_sum_6;
+    __gen_e_acsl_one_6 = 1;
+    __gen_e_acsl_cond_6 = 0;
+    __gen_e_acsl_lambda_6 = 0;
+    __gen_e_acsl_sum_6 = 0;
+    __gen_e_acsl_k_6 = 2147483647U;
+    while (1) {
+      __gen_e_acsl_cond_6 = __gen_e_acsl_k_6 > 2147483647U;
+      if (__gen_e_acsl_cond_6) break;
+      else {
+        __gen_e_acsl_lambda_6 = (int)__gen_e_acsl_k_6;
+        __gen_e_acsl_sum_6 += __gen_e_acsl_lambda_6;
+        __gen_e_acsl_k_6 += __gen_e_acsl_one_6;
+      }
+    }
+    /*@ assert Eva: signed_overflow: __gen_e_acsl_sum_6 + 1 ≤ 2147483647;
+    */
+    __e_acsl_assert((unsigned int)(__gen_e_acsl_sum_6 + 1) > 2147483647U,1,
+                    "Assertion","main",
+                    "\\sum(2147483647, 2147483647, \\lambda integer k; k) + 1 > 2147483647",
+                    "tests/arith/sum.c",16);
+  }
+  /*@ assert \sum(2147483647, 2147483647, \lambda ℤ k; k) + 1 > 2147483647;
+   */
+  ;
   __retres = 0;
   return __retres;
 }
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 fabbced782eec857e56330db0aa640f77a2ca944..b6ea52e13cb7621a3b3ed4a0b7f6fc52b609b37a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle
@@ -16,3 +16,5 @@
 [eva:alarm] tests/arith/sum.c:15: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/sum.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/sum.c:16: Warning: 
+  signed overflow. assert __gen_e_acsl_sum_6 + 1 ≤ 2147483647;
diff --git a/src/plugins/e-acsl/tests/arith/sum.c b/src/plugins/e-acsl/tests/arith/sum.c
index 3d8e9a551fe10f8c3ff3e637a47f6ae4a8bd90a5..dfa6b761cb4736b52f408241be2ed744d6598c25 100644
--- a/src/plugins/e-acsl/tests/arith/sum.c
+++ b/src/plugins/e-acsl/tests/arith/sum.c
@@ -13,6 +13,7 @@ int main(void) {
   /*@ assert \sum(10, 2, \lambda integer k; k) == 0; */;
   /*@ assert \sum(x * x, 2, \lambda integer k; k) == 0; */;
   /*@ assert \sum(ULLONG_MAX - 5, ULLONG_MAX, \lambda integer k; 1) == 6; */;
+  /*@ assert \sum(INT_MAX, INT_MAX, \lambda integer k; k) + 1 > INT_MAX; */
 
   return 0;
 }