diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 39aa508ee32fa5f528ad703960827edae45accab..460b93f8db9c6b8c13154c5d6e4ec98c455d4322 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -196,12 +196,14 @@ let printers = [
   Printf.sprintf "%.64g" ;
 ]
 
-let re_int = Str.regexp "[0-9]+"
+let re_int_float = Str.regexp "\\(-?[0-9]+\\)\\(e[+-]?[0-9]+\\)?$"
 
 let force_float r =
-  if Str.string_match re_int r 0 &&
-     Str.match_end () = String.length r
-  then (r ^ ".0") else r
+  if Str.string_match re_int_float r 0
+  then
+    let group n r = try Str.matched_group n r with Not_found -> ""
+    in group 1 r ^ ".0" ^ group 2 r
+  else r
 
 let float_lit ulp (q : Q.t) =
   let v = match ulp with
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index c6d48f85cc31f16c9983b13534f09e9e6c629f93..f1e5eb696a3302ef8d4da90ea9428d9d62c21219 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -107,6 +107,11 @@ let f_bit_export   = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" (
 let () = let open LogicBuiltins in add_builtin "\\bit_test_stdlib" [Z;Z] f_bit_stdlib
 let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit_positive
 
+let f_bits = [ f_bit_stdlib ; f_bit_positive ; f_bit_export ]
+
+let bit_test e k =
+  F.e_fun (if k <= 0 then f_bit_positive else f_bit_stdlib) [e ; e_int k]
+
 (* -------------------------------------------------------------------------- *)
 (* --- Matching utilities for simplifications                             --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index be94baad52b5c7285e47f53342ba4fa9ec609a62..2b830151f316fe3a125aa8db73c3f1e4aae93416 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -73,6 +73,9 @@ val f_lsl  : lfun
 val f_lsr  : lfun
 
 val f_bitwised : lfun list (** All except f_bit_positive *)
+val f_bits : lfun list (** All bit-test functions *)
+
+val bit_test : term -> int -> term
 
 (** Simplifiers *)