diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 0e7823ec685103d07645efcea8e3cceae7ffcdb0..4202b6e1aa9f87c9f83d14e99ddbc16f7e981374 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4783,7 +4783,7 @@ int unsetenv(char const *name)
     requires
       alignment_is_a_suitable_power_of_two:
         alignment ≥ sizeof(void *) ∧
-        ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+        ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
     assigns __fc_heap_status, \result;
     assigns __fc_heap_status
       \from (indirect: alignment), size, __fc_heap_status;
@@ -4820,7 +4820,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
   assert
   alignment_is_a_suitable_power_of_two:
     alignment ≥ sizeof(void *) ∧
-    ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+    ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
    */
   ;
   *memptr = malloc(size);
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 124447020ca076a79b8ea78a720bd642a027255f..c56321364a9234201c52fb7a0fca9f131488c7ca 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -123,7 +123,7 @@ int F3(int f2)
   V3 = 0;
   if (f2) goto L2;
   V3 ++;
-  /*@ assert property: V3 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
+  /*@ assert property: V3? 1 ≢ 0: 0 ≢ 0; */ ;
   L2: ;
   return V3;
 }
diff --git a/tests/spec/oracle/all.res.oracle b/tests/spec/oracle/all.res.oracle
index eb8254c5c9c3b52924be4b72237c40fad9952ed7..8543e35a53dd6a642a6fbf9b70a36729fee547aa 100644
--- a/tests/spec/oracle/all.res.oracle
+++ b/tests/spec/oracle/all.res.oracle
@@ -29,7 +29,7 @@ axiomatic Test {
   
   axiom e: P ⊻ Q;
   
-  axiom f: 0 ≢ 0? P: Q;
+  axiom f: 0? P: Q;
   
   axiom g: (P ⇒ P) ∧ (¬P ⇒ Q);
   
@@ -39,13 +39,13 @@ axiomatic Test {
   
   }
  */
-/*@ predicate R(ℤ i, ℤ j) = (1 ≢ 0? i + j: (j: j)) ≡ i + j;
+/*@ predicate R(ℤ i, ℤ j) = (1? i + j: (j: j)) ≡ i + j;
  */
-/*@ predicate S(ℤ i, ℤ j) = (1 ≢ 0? (i: j): j) ≡ j;
+/*@ predicate S(ℤ i, ℤ j) = (1? (i: j): j) ≡ j;
  */
-/*@ predicate T(ℤ i, ℤ j) = (1 ≢ 0? i: j) ≡ i;
+/*@ predicate T(ℤ i, ℤ j) = (1? i: j) ≡ i;
  */
-/*@ lemma tauto: 0 ≢ 0? T(0, 0): R(1, 2);
+/*@ lemma tauto: 0? T(0, 0): R(1, 2);
  */
 /*@ lemma tauto2: (R(0, 1) ⇒ S(3, 4)) ∧ (¬R(0, 1) ⇒ T(5, 6));
  */
diff --git a/tests/spec/oracle/null_ptr.res.oracle b/tests/spec/oracle/null_ptr.res.oracle
index 5412691e03a9c6d7725e8c152d128c7d7cfe42d4..59e76f0ef7d1ec8f5036e6f2d518783aee6394d3 100644
--- a/tests/spec/oracle/null_ptr.res.oracle
+++ b/tests/spec/oracle/null_ptr.res.oracle
@@ -22,7 +22,7 @@ void f(char *x)
   return;
 }
 
-/*@ ensures (\result ≢ 0) ≡ \true; */
+/*@ ensures \result ≡ \true; */
 int g(void)
 {
   int __retres;
diff --git a/tests/spec/oracle/parsing.res.oracle b/tests/spec/oracle/parsing.res.oracle
index 487e29fb1342d37790ec6a7cdc4e8a3fa70e0c09..37ceb452828771824c64f560b20240993372d9ef 100644
--- a/tests/spec/oracle/parsing.res.oracle
+++ b/tests/spec/oracle/parsing.res.oracle
@@ -7,9 +7,9 @@
 /* Generated by Frama-C */
 /*@ lemma bidon{Here}: ∀ int *t; ¬(*(t + 0) > 0);
  */
-/*@ lemma bidon1{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
+/*@ lemma bidon1{Here}: ∀ int *t; !*(t + 0) ≡ 0;
  */
-/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
+/*@ lemma bidon2{Here}: ∀ int *t; !*(t + 0) ≡ 0;
  */
 /*@
 predicate foo{L}(int *a, int *b, int length) =
diff --git a/tests/spec/oracle/real_typing_bts1309.res.oracle b/tests/spec/oracle/real_typing_bts1309.res.oracle
index 263809eb1832681d56202f6c8e08218c15c769e5..47e5a9adb68ca12d63af065b1c40d96180a32eb2 100644
--- a/tests/spec/oracle/real_typing_bts1309.res.oracle
+++ b/tests/spec/oracle/real_typing_bts1309.res.oracle
@@ -3,7 +3,7 @@
 void foo(int c)
 {
   float f = (float)1.0;
-  /*@ assert 0.0 ≤ (c ≢ 0? f: 2.0); */ ;
+  /*@ assert 0.0 ≤ (c? f: 2.0); */ ;
   return;
 }
 
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index a699b713faad14c29361449e3f4a8152e80d9635..33d75e1e69f2608ecd23ae500afad522912fb7ac 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -2,23 +2,23 @@
 [kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
 /* Generated by Frama-C */
 /*@ requires /* vid:23, lvid:23 */x < 10; */
-static int /* vid:52 */f(int /* vid:23, lvid:23 */x);
+static int /* vid:54 */f(int /* vid:23, lvid:23 */x);
 
-int /* vid:26 */g(void)
+int /* vid:28 */g(void)
 {
-  int /* vid:27 */tmp;
-  /* vid:27 */tmp = /* vid:52 */f(4);
-  return /* vid:27 */tmp;
+  int /* vid:29 */tmp;
+  /* vid:29 */tmp = /* vid:54 */f(4);
+  return /* vid:29 */tmp;
 }
 
-/*@ requires /* vid:47, lvid:47 */x < 10; */
-static int /* vid:53 */f_0(int /* vid:47, lvid:47 */x);
+/*@ requires /* vid:49, lvid:49 */x < 10; */
+static int /* vid:55 */f_0(int /* vid:49, lvid:49 */x);
 
-int /* vid:50 */h(void)
+int /* vid:52 */h(void)
 {
-  int /* vid:51 */tmp;
-  /* vid:51 */tmp = /* vid:53 */f_0(6);
-  return /* vid:51 */tmp;
+  int /* vid:53 */tmp;
+  /* vid:53 */tmp = /* vid:55 */f_0(6);
+  return /* vid:53 */tmp;
 }