diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index b2c51f3b799cf440f88f6e4ff3cc918df3687252..727d6639ffd39c87b79ad04acfda62f86d667a62 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1229,7 +1229,8 @@ struct
       | t1, Ltype ({lt_name = name},[])
         when name = Utf8_logic.boolean && is_integral_type t1 ->
         let t2 = Ltype (C.find_logic_type Utf8_logic.boolean,[]) in
-        { e with term_node = TLogic_coerce(t2,e); term_type = t2 }
+        let e = mk_cast e Linteger in
+        Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) t2
       | t1, Linteger when Logic_const.is_boolean_type t1 && explicit ->
         logic_coerce Linteger e
       | t1, Ctype t2 when Logic_const.is_boolean_type t1
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
index e6908ae18690a3b70e4fa4d5ccd1c3781a8d1d3b..0071a69eb1e7fb791cc0233cb8322a7c9a4b96a0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/precedence.res.oracle
@@ -778,19 +778,19 @@ void predicate(int x, int a, int b)
     ensures
       ko: r_precedence_and_eq:
         \old(p) ≡ \old(q) ∧ \old(r) ≢ 0 ⇔
-        (𝔹)\old(p) ≡ ((𝔹)\old(q) ∧ (𝔹)\old(r));
+        (\old(p) ≢ 0) ≡ (\old(q) ≢ 0 ∧ \old(r) ≢ 0);
     ensures
       ko: l_precedence_and_eq:
         \old(p) ≢ 0 ∧ \old(q) ≡ \old(r) ⇔
-        ((𝔹)\old(p) ∧ (𝔹)\old(q)) ≡ (𝔹)\old(r);
+        (\old(p) ≢ 0 ∧ \old(q) ≢ 0) ≡ (\old(r) ≢ 0);
     ensures
       ko: l_nonassoc_eq:
         \old(p) ≡ \old(q) ≡ \old(r) ⇔
-        (\old(p) ≡ \old(q)) ≡ (𝔹)\old(r);
+        (\old(p) ≡ \old(q)) ≡ (\old(r) ≢ 0);
     ensures
       ko: r_nonassoc_eq:
         \old(p) ≡ \old(q) ≡ \old(r) ⇔
-        (𝔹)\old(p) ≡ (\old(q) ≡ \old(r));
+        (\old(p) ≢ 0) ≡ (\old(q) ≡ \old(r));
     ensures
       r_precedence_neq_and:
         \old(p) ≢ \old(q) ∧ R ⇔ \old(p) ≢ \old(q) ∧ R;
@@ -800,11 +800,11 @@ void predicate(int x, int a, int b)
     ensures
       ko: r_precedence_and_neq:
         \old(p) ≢ \old(q) ∧ \old(r) ≢ 0 ⇔
-        (𝔹)\old(p) ≢ ((𝔹)\old(q) ∧ (𝔹)\old(r));
+        (\old(p) ≢ 0) ≢ (\old(q) ≢ 0 ∧ \old(r) ≢ 0);
     ensures
       ko: l_precedence_and_neq:
         \old(p) ≢ 0 ∧ \old(q) ≢ \old(r) ⇔
-        ((𝔹)\old(p) ∧ (𝔹)\old(q)) ≢ (𝔹)\old(r);
+        (\old(p) ≢ 0 ∧ \old(q) ≢ 0) ≢ (\old(r) ≢ 0);
  */
 void comparison(int p, int q, int r)
 {
diff --git a/tests/misc/oracle/booleans.res.oracle b/tests/misc/oracle/booleans.res.oracle
index d54bc6a7cc3754cb499512a1a92b132b191ea45d..8f7927c6bceb80d83a27026a4ecd2ad4e9c7862b 100644
--- a/tests/misc/oracle/booleans.res.oracle
+++ b/tests/misc/oracle/booleans.res.oracle
@@ -29,8 +29,8 @@ int main(void)
 {
   int __retres;
   int x = 42;
-  /*@ check (𝔹)x ≡ (𝔹)17; */ ;
-  /*@ check (ℤ)(𝔹)x ≡ 17; */ ;
+  /*@ check (x ≢ 0) ≡ (17 ≢ 0); */ ;
+  /*@ check ((ℤ)x ≢ 0) ≡ 17; */ ;
   __retres = 0;
   return __retres;
 }
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index 3c55a38dad0c053de28e653be83d2f8c445f8fd4..124447020ca076a79b8ea78a720bd642a027255f 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? 1 ≢ 0: 0 ≢ 0; */ ;
+  /*@ assert property: V3 ≢ 0? 1 ≢ 0: 0 ≢ 0; */ ;
   L2: ;
   return V3;
 }
diff --git a/tests/spec/oracle/all.res.oracle b/tests/spec/oracle/all.res.oracle
index 26a8ebc75b72bc9e54f8828f04b4d593f4c36364..eb8254c5c9c3b52924be4b72237c40fad9952ed7 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? P: Q;
+  axiom f: 0 ≢ 0? P: Q;
   
   axiom g: (P ⇒ P) ∧ (¬P ⇒ Q);
   
@@ -39,13 +39,13 @@ axiomatic Test {
   
   }
  */
-/*@ predicate R(ℤ i, ℤ j) = ((𝔹)1? i + j: (j: j)) ≡ i + j;
+/*@ predicate R(ℤ i, ℤ j) = (1 ≢ 0? i + j: (j: j)) ≡ i + j;
  */
-/*@ predicate S(ℤ i, ℤ j) = ((𝔹)1? (i: j): j) ≡ j;
+/*@ predicate S(ℤ i, ℤ j) = (1 ≢ 0? (i: j): j) ≡ j;
  */
-/*@ predicate T(ℤ i, ℤ j) = ((𝔹)1? i: j) ≡ i;
+/*@ predicate T(ℤ i, ℤ j) = (1 ≢ 0? i: j) ≡ i;
  */
-/*@ lemma tauto: (𝔹)0? T(0, 0): R(1, 2);
+/*@ lemma tauto: 0 ≢ 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/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index c1cc68010da5418638cd91e6ff40804e382e07eb..c7f4d27c228754c51e314be1178c710e024d7775 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -55,11 +55,11 @@ void h(void)
  */
 /*@ logic _Bool _Bool_from_boolean(𝔹 b) = (_Bool)b;
  */
-/*@ logic 𝔹 boolean_from_integer(ℤ b) = (𝔹)b;
+/*@ logic 𝔹 boolean_from_integer(ℤ b) = b ≢ 0;
  */
-/*@ logic 𝔹 boolean_from_int(int b) = (𝔹)b;
+/*@ logic 𝔹 boolean_from_int(int b) = b ≢ 0;
  */
-/*@ logic 𝔹 boolean_from_Bool(_Bool b) = b;
+/*@ logic 𝔹 boolean_from_Bool(_Bool b) = b ≢ 0;
 
 */
 
diff --git a/tests/spec/oracle/null_ptr.res.oracle b/tests/spec/oracle/null_ptr.res.oracle
index 55b0cc5e43312b983654cf48e3e5a50d64ddbb3e..5412691e03a9c6d7725e8c152d128c7d7cfe42d4 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 ≡ \true; */
+/*@ ensures (\result ≢ 0) ≡ \true; */
 int g(void)
 {
   int __retres;
diff --git a/tests/spec/oracle/parsing.res.oracle b/tests/spec/oracle/parsing.res.oracle
index 4cff9264d422478156e431d11abad6f852f7fcd1..487e29fb1342d37790ec6a7cdc4e8a3fa70e0c09 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;
+/*@ lemma bidon1{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (0 ≢ 0);
  */
-/*@ lemma bidon2{Here}: ∀ int *t; !(𝔹)*(t + 0) ≡ (𝔹)0;
+/*@ lemma bidon2{Here}: ∀ int *t; !(*(t + 0) ≢ 0) ≡ (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 1a15afbf483fe756bc42c913b61ebc7a4337b275..263809eb1832681d56202f6c8e08218c15c769e5 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? f: 2.0); */ ;
+  /*@ assert 0.0 ≤ (c ≢ 0? f: 2.0); */ ;
   return;
 }