diff --git a/src/transformations/utils.ml b/src/transformations/utils.ml
index 659bd88f41c9f3a9118448922700427e0c66f119..ad9e5e48a3b3b711c434b4415cb2d485d5f21882 100644
--- a/src/transformations/utils.ml
+++ b/src/transformations/utils.ml
@@ -35,19 +35,17 @@ let float_of_real_constant rc =
   if is_neg then Float.neg f else f
 
 let real_constant_of_float value =
-  let neg = Float.is_negative value in
-  let value = Fmt.str "%.64f" (Float.abs value) in
-  (* Split into integer and fractional parts. *)
-  let int_frac = String.split value ~on:'.' in
-  let int = List.hd_exn int_frac in
-  let frac =
-    match List.tl_exn int_frac with
-    | [] -> ""
-    | [ s ] -> s
-    | _ -> assert false (* Since every float has one '.' at most. *)
-  in
+  assert (Float.is_finite value);
+  let m, e = Float.frexp value in
+  (* put into the form m * 2^e, where m is an integer *)
+  let m, e = (Int.of_float (Float.ldexp m 53), e - 53) in
   Why3.Constant.ConstReal
-    (Why3.Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+    {
+      rl_kind = RLitDec 0;
+      rl_real =
+        Why3.Number.real_value ~pow2:(Why3.BigInt.of_int e)
+          (Why3.BigInt.of_int m);
+    }
 
 let term_of_float env f =
   let th = Symbols.Float64.create env in