diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 62e84f90c706cfb4d1e3c468321d6a1e7ba890dc..7ce1e025fb66a17a01ee926b8ba03a8f95a77c05 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -399,8 +399,14 @@ let rec term_to_exp t res =
   | TConst (LWStr l) -> new_exp ~loc (Const (CWStr l))
   | TConst (LChr c) -> new_exp ~loc (Const (CChr c))
   | TConst (LReal l_real) ->
-    (* r_nearest is by definition in double precision. *)
-    new_exp ~loc (Const (CReal (l_real.r_nearest, FDouble, None)))
+    let fk,_ = Floating_point.parse l_real.r_literal in
+    let cst =
+      if Cil.isExactFloat fk l_real then
+        (CReal (l_real.r_nearest, fk, Some l_real.r_literal))
+      else (* fallback to double, r_nearest being in that format anyways *)
+        (CReal (l_real.r_nearest, FDouble, None))
+    in
+    new_exp ~loc (Const cst)
   | TConst (LEnum e) -> new_exp ~loc (Const (CEnum e))
   | TLval tlval -> new_exp ~loc (Lval (tlval_to_lval tlval res))
   | TSizeOf ty -> new_exp ~loc (SizeOf ty)
@@ -413,6 +419,15 @@ let rec term_to_exp t res =
   | TBinOp (binop, t1, t2)->
     new_exp ~loc
       (BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil.intType))
+  | TCastE(ty, { term_node = TConst(LReal lreal) })
+    when Cil.isArithmeticType ty && not (Cil.isIntegralType ty) ->
+    (match Cil.unrollType ty with
+     | TFloat(fk,_) ->
+       new_exp ~loc
+         (Const (CReal (lreal.r_nearest,fk,Some lreal.r_literal)))
+     | _ ->
+       Aorai_option.fatal
+         "A floating-point type was expected, got %a." Printer.pp_typ ty)
   | TCastE (ty, t) -> new_exp ~loc (CastE (ty, term_to_exp t res))
   | TAddrOf tlval -> new_exp ~loc (AddrOf (tlval_to_lval tlval res))
   | TStartOf tlval -> new_exp ~loc (StartOf (tlval_to_lval tlval res))
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index f65b5d988b1f293b1ccf2033a0d6207cbbe738ef..5cd54943e86d5589f36fa80cd8d86f13d30b4266 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -124,6 +124,7 @@ let extend () =
         Wp.Wp_parameters.SplitBranch.on();
         Wp.Wp_parameters.SplitConj.on();
         Wp.Wp_parameters.SplitMax.set 32;
+        Wp.Wp_parameters.Model.As_string.set "+real";
         if not (Wp.Wp_parameters.Verbose.is_set()) then
           Wp.Wp_parameters.Verbose.set 0;
         Globals.Functions.iter check_auto_func;
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index a614ddfed926fdc3e44666c4744adf18e2ae4123..a5a1b263a40e8a838d4fe35a43b3b6cd12fce6f1 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -176,7 +176,7 @@ check lemma B_deterministic_trans{L}:
     aorai_CurOpStatus = aorai_Called;
     aorai_CurOperation = op_square_root_aux;
     if ((unsigned int)1 == aorai_CurStates) 
-      if (x >= 1.f) 
+      if (x >= 1.0f) 
         if (x <= n) aorai_CurStates = B; else aorai_CurStates = aorai_reject;
       else aorai_CurStates = aorai_reject;
     else aorai_CurStates = aorai_reject;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
index 1da703e983a6603fa01b9060f5f85ed3a00d3abc..28b4a5aa18615ebfd8af4e80290b8e8385453f1c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
@@ -85,11 +85,3 @@
   ----------------------------------------------------------------------------
 [kernel] Parsing TMPDIR/aorai_floats_0_prove.i (no preprocessing)
 [wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
-  aorai_CurStates ≡ B in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
-  aorai_CurStates ≡ B in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
-  aorai_CurStates ≢ aorai_reject in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
-  aorai_CurStates ≢ aorai_reject in automaton function square_root_aux_pre_func