diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 60c0efae3922f9f7c5b7ae12876965847cd93b65..8f0c5dd0358b15a7b63d478b793b41a13013ee51 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -579,7 +579,11 @@ struct
     | L_cint _ ->
         L.map Cint.to_integer (C.logic env t)
     | L_integer -> C.logic env t
-    | L_cfloat _|L_bool|L_pointer _|L_array _ ->
+    | L_cfloat f ->
+        L.map
+          (fun x -> Cmath.int_of_real (Cfloat.real_of_float f x))
+          (C.logic env t)
+    | L_bool|L_pointer _|L_array _ ->
         Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
           Printer.pp_logic_type src_ltype Printer.pp_logic_type Linteger