diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index cd8d3806d7e91d1f1fc4bd7d8213b8bb832abb99..3c1d7735a8d20fe5bc64b4d5644a33718b188147 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2530,14 +2530,14 @@ class cil_printer () = object (self)
       fprintf fmt "@[%a@]" self#tand_list (get_tand_list l [r])
     | TBinOp (op,l,r) ->
       fprintf fmt "@[%a@ %a@ %a@]" term l self#term_binop op term r
-    | TCastE (ty,e) ->
+    | TCastE (ty,t) ->
       begin match ty, t.term_node with
         | TFloat(fk,_) , TConst(LReal r as cst) when
             not Kernel.(is_debug_key_enabled dkey_print_logic_coercions) &&
             Floating_point.has_suffix fk r.r_literal ->
           self#logic_constant fmt cst
         | _ ->
-          fprintf fmt "(%a)%a" (self#typ None) ty term e
+          fprintf fmt "(%a)%a" (self#typ None) ty term t
       end
     | TAddrOf lv ->
       fprintf fmt "&%a" (self#term_lval_prec Precedence.addrOfLevel) lv
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index 5cfef8b4842d47fdb96478c571d46bccd98b42a0..a614ddfed926fdc3e44666c4744adf18e2ae4123 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -120,14 +120,14 @@ check lemma B_deterministic_trans{L}:
      ¬(\at(aorai_CurOperation,L) ≡ op_square_root_aux ∧
         \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
         \at(aorai_CurOperation,L) ≡ op_square_root_aux ∧
-        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
-        x ≥ (float)((float)1.0f) ∧ x ≤ n)) ∧
+        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≥ 1.0f ∧ 
+        x ≤ n)) ∧
   (∀ float n, float x;
      ¬(\at(aorai_CurOperation,L) ≡ op_square_root ∧
         \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
         \at(aorai_CurOperation,L) ≡ op_square_root_aux ∧
-        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
-        x ≥ (float)((float)1.0f) ∧ x ≤ n)) ∧
+        \at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≥ 1.0f ∧ 
+        x ≤ n)) ∧
   ¬(\at(aorai_CurOperation,L) ≡ op_square_root ∧
      \at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
      \at(aorai_CurOperation,L) ≡ op_square_root_aux ∧
@@ -136,8 +136,7 @@ check lemma B_deterministic_trans{L}:
 /*@ ghost enum aorai_States aorai_CurStates = I; */
 /*@ ghost
   /@ requires aorai_CurStates ≡ B;
-     requires
-       aorai_CurStates ≡ B ⇒ x ≥ (float)((float)1.0f) ∧ x ≤ n;
+     requires aorai_CurStates ≡ B ⇒ x ≥ 1.0f ∧ x ≤ n;
      ensures aorai_CurOpStatus ≡ aorai_Called;
      ensures aorai_CurOperation ≡ op_square_root_aux;
      assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
@@ -152,13 +151,11 @@ check lemma B_deterministic_trans{L}:
        ensures aorai_CurStates ≢ A;
      
      behavior buch_state_B_in:
-       assumes
-         aorai_CurStates ≡ B ∧ x ≥ (float)((float)1.0f) ∧ x ≤ n;
+       assumes aorai_CurStates ≡ B ∧ x ≥ 1.0f ∧ x ≤ n;
        ensures aorai_CurStates ≡ B;
      
      behavior buch_state_B_out:
-       assumes
-         aorai_CurStates ≢ B ∨ ¬(x ≥ (float)((float)1.0f) ∧ x ≤ n);
+       assumes aorai_CurStates ≢ B ∨ ¬(x ≥ 1.0f ∧ x ≤ n);
        ensures aorai_CurStates ≢ B;
      
      behavior buch_state_C_out:
@@ -236,8 +233,7 @@ check lemma B_deterministic_trans{L}:
 */
 
 /*@ requires aorai_CurStates ≡ B;
-    requires
-      aorai_CurStates ≡ B ⇒ x ≥ (float)((float)1.0f) ∧ x ≤ n;
+    requires aorai_CurStates ≡ B ⇒ x ≥ 1.0f ∧ x ≤ n;
     assigns \result, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
     assigns \result \from x, n;
     
diff --git a/tests/float/oracle/const1.res.oracle b/tests/float/oracle/const1.res.oracle
index a843cb7cf3b3001cd1594f0f21aa7148c4b6b5d4..8fbb1ef225d90d95581c0e8b293af2795ff5da08 100644
--- a/tests/float/oracle/const1.res.oracle
+++ b/tests/float/oracle/const1.res.oracle
@@ -5,7 +5,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva:alarm] const1.i:1: Warning: 
-  non-finite float value. assert \is_finite((float)1e40f);
+  non-finite float value. assert \is_finite(1e40f);
 [eva] const1.i:1: Warning: 
   evaluation of initializer '(unsigned long long)1e40f' failed
 [eva] Initial state computed
diff --git a/tests/float/oracle/const2.res.oracle b/tests/float/oracle/const2.res.oracle
index 94744b2de338fad025efb90e4b9908e02488725a..8dd6596c994a7f134c54f94a632b43f205e9c061 100644
--- a/tests/float/oracle/const2.res.oracle
+++ b/tests/float/oracle/const2.res.oracle
@@ -5,7 +5,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva:alarm] const2.i:2: Warning: 
-  non-finite float value. assert \is_finite((float)1e40f);
+  non-finite float value. assert \is_finite(1e40f);
 [eva] const2.i:2: Warning: evaluation of initializer '1e40f' failed
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
diff --git a/tests/float/oracle/const4.0.res.oracle b/tests/float/oracle/const4.0.res.oracle
index fa336743685bb9299c681af68b70f7df506c97d1..6582b5a74178ba39ffb450f0d02a75fb248d2a60 100644
--- a/tests/float/oracle/const4.0.res.oracle
+++ b/tests/float/oracle/const4.0.res.oracle
@@ -6,7 +6,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva:alarm] const4.i:7: Warning: 
-  non-finite float value. assert \is_finite((float)3.405e38f);
+  non-finite float value. assert \is_finite(3.405e38f);
 [eva] const4.i:7: Warning: evaluation of initializer '(double)3.405e38f' failed
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
diff --git a/tests/float/oracle/const4.1.res.oracle b/tests/float/oracle/const4.1.res.oracle
index 85a2c33e173e9932409b5cc8a4778d10b568ec68..8854b8b2448d6cd9fd7ec98ede98a3d0cbabde8b 100644
--- a/tests/float/oracle/const4.1.res.oracle
+++ b/tests/float/oracle/const4.1.res.oracle
@@ -8,7 +8,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva:alarm] const4.i:7: Warning: 
-  non-finite float value. assert \is_finite((float)3.405e38f);
+  non-finite float value. assert \is_finite(3.405e38f);
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   f1 ∈ [3.39999995214e+38 .. 3.40000015497e+38]
diff --git a/tests/float/oracle/cte_overflow.res.oracle b/tests/float/oracle/cte_overflow.res.oracle
index 50328773570d84b2cc7982447936bb3466e625f3..d7287cf5d95221001a911e1a0f56f073a9be7f31 100644
--- a/tests/float/oracle/cte_overflow.res.oracle
+++ b/tests/float/oracle/cte_overflow.res.oracle
@@ -15,7 +15,7 @@
 [eva:alarm] cte_overflow.i:12: Warning: 
   non-finite double value. assert \is_finite((double)1e500);
 [eva:alarm] cte_overflow.i:17: Warning: 
-  non-finite float value. assert \is_finite((float)1e80f);
+  non-finite float value. assert \is_finite(1e80f);
 [eva] Recording results for main
 [eva] done for function main
 [eva] cte_overflow.i:12: 
diff --git a/tests/float/oracle/parse.res.oracle b/tests/float/oracle/parse.res.oracle
index f9c65e85c126e12b56abc0f52d25d2027bd2b99e..57d0b1b1bce9064e56bc30a472ca0c93a691c1fd 100644
--- a/tests/float/oracle/parse.res.oracle
+++ b/tests/float/oracle/parse.res.oracle
@@ -18,7 +18,7 @@
 [eva] parse.i:36: Warning: 
   cannot parse floating-point constant, returning imprecise result
 [eva:alarm] parse.i:36: Warning: 
-  non-finite long double value. assert \is_finite((long double)0x1p32767L);
+  non-finite long double value. assert \is_finite(0x1p32767L);
 [eva:alarm] parse.i:37: Warning: 
   non-finite long double value. assert \is_finite(l);
 [eva:alarm] parse.i:37: Warning: 
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 45092e46f291f3ead9cfe6dae97543f9ee079c99..7d5d9b9a27ffa3af3cfee2f8c7c4a62d0ad02977 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3523,8 +3523,7 @@ extern float frexpf(float x, int *exp);
 extern long double frexpl(long double x, int *exp);
 
 /*@ requires
-      finite_logic_res:
-        \is_finite((double)(x * pow((double)2.0d, (double)exp)));
+      finite_logic_res: \is_finite((double)(x * pow(2.0d, (double)exp)));
     ensures finite_result: \is_finite(\result);
     ensures
       __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);
@@ -3536,8 +3535,7 @@ extern double ldexp(double x, int exp);
 
 /*@ requires
       finite_logic_res:
-        \is_finite((float)(x *
-                           pow((double)((float)2.0f), (double)((float)exp))));
+        \is_finite((float)(x * pow((double)(2.0f), (double)((float)exp))));
     ensures finite_result: \is_finite(\result);
     ensures
       __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);