From acee652ae712571f773166c61fe22941c643148c Mon Sep 17 00:00:00 2001
From: Benjamin Monate <benjamin.monate@cea.fr>
Date: Wed, 18 May 2011 12:46:09 +0000
Subject: [PATCH] Propagate oracle from enum typing fix

---
 .../tests/e-acsl-runtime/oracle/gen_addrOf.c       | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c  | 10 +++++-----
 .../tests/e-acsl-runtime/oracle/gen_comparison.c   | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_false.c | 10 +++++-----
 .../e-acsl-runtime/oracle/gen_integer_constant.c   | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c  | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_not.c   | 10 +++++-----
 .../e-acsl-runtime/oracle/gen_other_constants.c    | 14 ++++++--------
 .../tests/e-acsl-runtime/oracle/gen_sizeof.c       | 10 +++++-----
 .../e-acsl/tests/e-acsl-runtime/oracle/gen_true.c  | 10 +++++-----
 .../oracle/other_constants.res.oracle              |  4 +---
 12 files changed, 57 insertions(+), 61 deletions(-)

diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index b390c68ee8b..55773197f9b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index b113dc2a124..b2bed027f32 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -142,7 +142,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -166,7 +166,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -190,7 +190,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -215,7 +215,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -231,7 +231,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index 890d4809614..35e5f2596d2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index 6314572f511..bffa806ee79 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -102,7 +102,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -126,7 +126,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -150,7 +150,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -175,7 +175,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -191,7 +191,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index c421b9d08fc..28cb35703c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 2f8d4ef60a3..397d3f50c84 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -106,7 +106,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -130,7 +130,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -154,7 +154,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -179,7 +179,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -195,7 +195,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index aea4759f166..c8521f9c1e5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -116,7 +116,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -140,7 +140,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -164,7 +164,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -189,7 +189,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -205,7 +205,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 073aca9609a..a365ad94736 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index e2e610c62b1..79471acb879 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -106,7 +106,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -130,7 +130,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -154,7 +154,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -179,7 +179,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -195,7 +195,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
@@ -584,9 +584,7 @@ int main(void)
   }
   
   /*@ assert false ≢ true; */ ;
-  if (! ((unsigned int)false != (unsigned int)true)) {
-    e_acsl_fail((char *)"(false != true)");
-  }
+  if (! (false != true)) { e_acsl_fail((char *)"(false != true)"); }
   __retres = 0;
   return (__retres);
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 8bce5f3f5d7..91e233f19d9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 6a641969a85..e65624f378f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -89,7 +89,7 @@ __inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -113,7 +113,7 @@ __inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -137,7 +137,7 @@ __inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
   mp_size_t __gmp_n;
   mp_ptr __gmp_p;
   int tmp;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_p = __gmp_z->_mp_d;
   if (__gmp_n == (mp_size_t)0) { tmp = 1; }
   else {
@@ -162,7 +162,7 @@ __inline static unsigned long __gmpz_get_ui(mpz_srcptr __gmp_z)
   mp_limb_t __gmp_l;
   mp_limb_t tmp;
   __gmp_p = __gmp_z->_mp_d;
-  __gmp_n = (mp_size_t)__gmp_z->_mp_size;
+  __gmp_n = (long)__gmp_z->_mp_size;
   __gmp_l = *(__gmp_p + 0);
   if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
   else { tmp = (unsigned long)0; }
@@ -178,7 +178,7 @@ __inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
   mp_limb_t __gmp_result;
   long tmp_1;
   int tmp_0;
-  __gmp_result = (mp_limb_t)0;
+  __gmp_result = (unsigned long)0;
   { /*undefined sequence*/ 
     if (__gmp_n >= (mp_size_t)0) {
       int tmp;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index 5aebbdd4cb4..746755d7444 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -112,9 +112,7 @@ int main(void)
   }
   
   /*@ assert false ≢ true; */ ;
-  if (! ((unsigned int)false != (unsigned int)true)) {
-    e_acsl_fail((char *)"(false != true)");
-  }
+  if (! (false != true)) { e_acsl_fail((char *)"(false != true)"); }
   __retres = 0;
   return (__retres);
 }
-- 
GitLab