diff --git a/tests/constant_propagation/oracle/enum.res.oracle b/tests/constant_propagation/oracle/enum.res.oracle
index cbd71cd5823f8857dc1be38d4f25f5b387a0cb98..d7c4e9f6ea0bf3521fa720adbe26fe05202eb5b9 100644
--- a/tests/constant_propagation/oracle/enum.res.oracle
+++ b/tests/constant_propagation/oracle/enum.res.oracle
@@ -14,7 +14,7 @@
 [eva] Recording results for f
 [eva] Done for function f
 [eva:alarm] tests/constant_propagation/enum.i:13: Warning: 
-  signed overflow. assert B + c ≤ 2147483647;
+  signed overflow. assert (int)B + c ≤ 2147483647;
 [eva:alarm] tests/constant_propagation/enum.i:15: Warning: 
   signed overflow. assert (int)(y + z) + t ≤ 2147483647;
 [eva:alarm] tests/constant_propagation/enum.i:15: Warning: 
@@ -43,7 +43,7 @@ int main(int c, unsigned int u)
   enum E x = A;
   int y = f(0U);
   int z = f(D);
-  /*@ assert Eva: signed_overflow: B + c ≤ 2147483647; */
+  /*@ assert Eva: signed_overflow: (int)B + c ≤ 2147483647; */
   int t = B + c;
   int v = (int)(2U + u);
   /*@ assert Eva: signed_overflow: (int)(y + z) + t ≤ 2147483647; */
diff --git a/tests/syntax/oracle/assembly_gmp.1.res.oracle b/tests/syntax/oracle/assembly_gmp.1.res.oracle
index 63a12b1b07bab4c049fb972e2f853cc2330cf8dd..70ffc4d780c3a76abd0e4e060e91dec0c49f39e2 100644
--- a/tests/syntax/oracle/assembly_gmp.1.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.1.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
       p0 = (long)(__m0 * __m1);
     }
     /*@ assigns r2, r1, r0;
-        assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
-        assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
-        assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+        assigns r2 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+        assigns r1 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+        assigns r0 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
     */
     __asm__ (
       "add\t%6, %q2\n\t"
diff --git a/tests/syntax/oracle/assembly_gmp.2.res.oracle b/tests/syntax/oracle/assembly_gmp.2.res.oracle
index 2684a9a66550dfd450d38cd9166036597ebdab3b..d3e9aca3737cce222093576d7e70a7e44cf4d481 100644
--- a/tests/syntax/oracle/assembly_gmp.2.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.2.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
       p0 = (long)(__m0 * __m1);
     }
     /*@ assigns r2, r1, r0;
-        assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
-        assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
-        assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+        assigns r2 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+        assigns r1 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+        assigns r0 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
     */
     __asm__ (
       "add%I6c\t%2, %5, %6\n\t"
diff --git a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
index 809576ab5a896f46826575c7a6cba00ccf7a8bff..97b551d63eb90d30964fb8910c53a61c73f989fd 100644
--- a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
+++ b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
@@ -16,19 +16,25 @@ void funk(int rounds)
   int i;
   unsigned int __lengthof_k_long_long_size;
   int k_positive_size[4 - 2];
-  /*@ assert alloca_bounds: 0 < sizeof(int) * (2 * rounds) ≤ 4294967295; */
+  /*@
+  assert alloca_bounds: 0 < sizeof(int) * (int)(2 * rounds) ≤ 4294967295;
+   */
   ;
   __lengthof_k = (unsigned int)(2 * rounds);
   int *k = __fc_vla_alloc(sizeof(int) * __lengthof_k);
   /*@
   assert
-  alloca_bounds: 0 < sizeof(int) * (unsigned int)(2 * rounds) ≤ 4294967295;
+  alloca_bounds:
+    0 < sizeof(int) * (unsigned int)((int)(2 * rounds)) ≤ 4294967295;
    */
   ;
   __lengthof_kk = (unsigned int)(2 * rounds);
   int *kk = __fc_vla_alloc(sizeof(int) * __lengthof_kk);
   long long j = (long long)(rounds * rounds);
-  /*@ assert alloca_bounds: 0 < sizeof(int) * (j * 2) ≤ 4294967295; */ ;
+  /*@
+  assert alloca_bounds: 0 < sizeof(int) * (long long)(j * 2) ≤ 4294967295;
+   */
+  ;
   __lengthof_k_long_long_size = (unsigned int)(j * (long long)2);
   int *k_long_long_size =
     __fc_vla_alloc(sizeof(int) * __lengthof_k_long_long_size);
diff --git a/tests/syntax/oracle/vla_strlen.res.oracle b/tests/syntax/oracle/vla_strlen.res.oracle
index 49dc5fb0597065d6ebcc3a9412b46b1a04719d72..0fe38231c89af62740bef5c9bca1ab60a670c39d 100644
--- a/tests/syntax/oracle/vla_strlen.res.oracle
+++ b/tests/syntax/oracle/vla_strlen.res.oracle
@@ -17,7 +17,11 @@ void f(char *s)
   unsigned int __lengthof_t;
   size_t tmp;
   tmp = strlen((char const *)s);
-  /*@ assert alloca_bounds: 0 < sizeof(char) * (tmp + 1) ≤ 4294967295; */ ;
+  /*@
+  assert
+  alloca_bounds: 0 < sizeof(char) * (unsigned int)(tmp + 1) ≤ 4294967295;
+   */
+  ;
   __lengthof_t = tmp + (size_t)1;
   char *t = __fc_vla_alloc(sizeof(char) * __lengthof_t);
   char *p = t;
diff --git a/tests/value/oracle/descending.res.oracle b/tests/value/oracle/descending.res.oracle
index 3b11d3495c607a8fe2f9068f6ac1faa87a5d17f6..7e67df6441b64d7719631c3bc6a09fc8caf77f81 100644
--- a/tests/value/oracle/descending.res.oracle
+++ b/tests/value/oracle/descending.res.oracle
@@ -14,7 +14,7 @@
 [eva:alarm] tests/value/descending.i:13: Warning: 
   accessing out of bounds index. assert (int)(i - 1) < 10;
 [eva:alarm] tests/value/descending.i:13: Warning: 
-  accessing uninitialized left-value. assert \initialized(&A[i - 1]);
+  accessing uninitialized left-value. assert \initialized(&A[(int)(i - 1)]);
 [eva] Recording results for test1
 [eva] Done for function test1
 [eva] computing for function test2 <- main.
diff --git a/tests/value/oracle/downcast.3.res.oracle b/tests/value/oracle/downcast.3.res.oracle
index 8f130d992c0907a57e5f46612bbcb59c879dfce5..8d2a9ee99b2b0162311fae95e37a7c09cc0ef24d 100644
--- a/tests/value/oracle/downcast.3.res.oracle
+++ b/tests/value/oracle/downcast.3.res.oracle
@@ -61,7 +61,7 @@
 [eva] computing for function main6_val_warn_converted_signed <- main.
   Called from tests/value/downcast.i:161.
 [eva:alarm] tests/value/downcast.i:75: Warning: 
-  signed downcast. assert (int)65300u ≤ 32767;
+  signed downcast. assert 65300u ≤ 32767;
 [eva:alarm] tests/value/downcast.i:91: Warning: 
   signed downcast. assert -32768 ≤ (int)e_1;
 [eva:alarm] tests/value/downcast.i:95: Warning: 
diff --git a/tests/value/oracle/incompatible_states.res.oracle b/tests/value/oracle/incompatible_states.res.oracle
index 9cd3bb24391f4465605fdb1d0b224608334bcc3d..d020cc431768e426b4883194da3f4b86841a0c0a 100644
--- a/tests/value/oracle/incompatible_states.res.oracle
+++ b/tests/value/oracle/incompatible_states.res.oracle
@@ -22,9 +22,11 @@
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva:alarm] tests/value/incompatible_states.c:38: Warning: 
-  accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+  accessing uninitialized left-value.
+  assert \initialized(&t[(int)((int)(2 * i) / 2)]);
 [eva:alarm] tests/value/incompatible_states.c:41: Warning: 
-  accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+  accessing uninitialized left-value.
+  assert \initialized(&t[(int)((int)(2 * i) / 2)]);
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.