diff --git a/colibri2.opam b/colibri2.opam
index d1c4ee231e43cb2806d33721f60f2a4da8d292fb..e67d68c236f8798255ba270991cc62bfb76e2b6b 100644
--- a/colibri2.opam
+++ b/colibri2.opam
@@ -49,11 +49,3 @@ build: [
   ]
 ]
 dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
-pin-depends: [
-  [ "dune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-site.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-private-libs.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dyn.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "ordering.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "stdune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-]
diff --git a/colibrics.opam b/colibrics.opam
index 423c9412a986b7c207d803ed838a1242ddb635be..0f90f1de73131d142f07b8c31bfec800f44455c8 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -36,11 +36,3 @@ build: [
   ]
 ]
 dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
-pin-depends: [
-  [ "dune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-site.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-private-libs.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dyn.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "ordering.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "stdune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-]
diff --git a/dune b/dune
index 81b443b85c783efc1f46be758a875d959c9254ed..357ed95ef4c3d97659b67e18ff5f5c22643a54f8 100644
--- a/dune
+++ b/dune
@@ -1,4 +1,4 @@
-(vendored_dirs dolmen farith farith2)
+(vendored_dirs dolmen farith)
 
 (rule (copy generic.opam.template colibrics.opam.template))
 (rule (copy generic.opam.template colibri2.opam.template))
diff --git a/farith2/extract/farith_Big.ml b/farith2/extract/farith_Big.ml
index 3ba55d18b0d35b4687e6acccade4b8aebcc8e0aa..6dcac828f099c4560705a35ee7717d9e9186a744 100644
--- a/farith2/extract/farith_Big.ml
+++ b/farith2/extract/farith_Big.ml
@@ -248,7 +248,7 @@ module Z = Z (* zarith *)
 
 (* Q *)
 (* must be already normalize *)
-let q_mk (den, num) = { Q.den; Q.num }
+let q_mk (num, den) = { Q.den; Q.num }
 
 let q_case f q = f q.Q.den q.Q.num
 
diff --git a/farith2/farith2.ml b/farith2/farith2.ml
index c3bacd31ee23cb93c239f7d17111ba6ce1556aa0..a99fe665216e96f6afc88884a29d1100528596e8 100644
--- a/farith2/farith2.ml
+++ b/farith2/farith2.ml
@@ -20,6 +20,8 @@
 (**************************************************************************)
 open Base
 
+module Format = Stdlib.Format
+
 module Z = struct
   include Z
 
@@ -85,7 +87,7 @@ module F = struct
         (Z.of_string m, Z.of_string e)
     | None -> (Z.of_string s, Z.zero)
 
-  let of_q ~mw ~ew ~mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
+  let of_q ~mw ~ew mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
   let of_bits ~mw ~ew z = of_bits (Z.of_int mw) (Z.of_int ew) z
   let to_bits t = to_bits t
   let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
@@ -95,6 +97,23 @@ module F = struct
   let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
   let is_nan t = match t.value with B754_nan -> true | _ -> false
 
+  let round ~mw ~ew mode (f:t) : t =
+    (match f.value with
+        | B754_zero _
+        | B754_infinity _
+        | B754_nan -> { mw = Z.of_int mw; ew = Z.of_int ew; value = f.value }
+        | B754_finite (_, _, _) ->
+          (of_q ~mw ~ew mode (to_q f))
+    )
+
+  let of_float f = of_bits ~mw:52 ~ew:11
+    @@ Z.extract (Z.of_int64 (Int64.bits_of_float f)) 0 64
+  let to_float mode f = round ~mw:52 ~ew:11 mode f
+                        |> to_bits
+                        |> fun z -> Z.signed_extract z 0 64
+                        |> Z.to_int64
+                        |> Int64.float_of_bits
+
   let is_negative t =
     match t.value with
     | B754_zero true | B754_finite (true, _, _) -> true
diff --git a/farith2/farith2.mli b/farith2/farith2.mli
index afae526f593f21d9d6990c00b9ba9850fc5ab80c..93600496671f309c56aeb5c0855d4066d5aca6a0 100644
--- a/farith2/farith2.mli
+++ b/farith2/farith2.mli
@@ -46,7 +46,7 @@ module F : sig
 
   val pp : Format.formatter -> t -> unit
 
-  val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
+  val of_q : mw:int -> ew:int -> mode -> Q.t -> t
 
   val to_q : t -> Q.t
 
@@ -74,6 +74,12 @@ module F : sig
 
   val to_bits : t -> Z.t
 
+  val of_float : float -> t
+
+  val to_float : mode -> t -> float
+
+  val round: mw:int -> ew:int -> mode -> t -> t
+
   val ge : t -> t -> bool
 
   val gt : t -> t -> bool
@@ -133,6 +139,8 @@ module I : sig
   val is_singleton : t -> F.t option
 end
 
+val flocq_version: Z.t
+
 (* (\** {2 Generic Version } *\)
  * 
  * 
diff --git a/farith2/tests/issue_005.expected b/farith2/tests/issue_005.expected
new file mode 100644
index 0000000000000000000000000000000000000000..ed307829500e365446db32fa3dc0b7b6c12fbf40
--- /dev/null
+++ b/farith2/tests/issue_005.expected
@@ -0,0 +1 @@
+[F] 0.100000 : +3602879701896397p-55
diff --git a/farith2/tests/issue_005.ml b/farith2/tests/issue_005.ml
new file mode 100644
index 0000000000000000000000000000000000000000..363837f36f5977fda8004cb8d4568566aca3cb76
--- /dev/null
+++ b/farith2/tests/issue_005.ml
@@ -0,0 +1,11 @@
+open Format
+open Farith2
+
+let f_convert r =
+  let fp = F.of_float r in
+  printf "[F] %f : %a@." r F.pp fp ; fp
+
+let () =
+  begin
+    ignore (f_convert 0.1) ;
+  end
diff --git a/farith2/tests/mode.expected b/farith2/tests/mode.expected
new file mode 100644
index 0000000000000000000000000000000000000000..5d6065ed5c2ced2bf520fa368f19f29952f58ca7
--- /dev/null
+++ b/farith2/tests/mode.expected
@@ -0,0 +1,61 @@
+[F]  3.1 = +6980579422424269p-51
+[Fp] 3.1 = +6501171p-21
+[Fq] 3.1 = +6501171p-21
+-----------------------
+ Simple Roundings
+-----------------------
+Q=31/10
+[F-NE] +6980579422424269p-51
+[F-NE] -6980579422424269p-51
+-----------------------
+Q=31/10
+[F-NA] +6980579422424269p-51
+[F-NA] -6980579422424269p-51
+-----------------------
+Q=31/10
+[F-ZR] +1745144855606067p-49
+[F-ZR] -1745144855606067p-49
+-----------------------
+Q=31/10
+[F-UP] +6980579422424269p-51
+[F-UP] -1745144855606067p-49
+-----------------------
+Q=31/10
+[F-DN] +1745144855606067p-49
+[F-DN] -6980579422424269p-51
+-----------------------
+ Tie Breaks (NE)
+-----------------------
+Q=562949953421313/562949953421312
+[F-NE-ex] +562949953421313p-49
+[F-NE-ex] -562949953421313p-49
+-----------------------
+Q=2251799813685253/2251799813685248
+[F-NE-lo] +2251799813685253p-51
+[F-NE-lo] -2251799813685253p-51
+-----------------------
+Q=1125899906842627/1125899906842624
+[F-NE-ti] +1125899906842627p-50
+[F-NE-ti] -1125899906842627p-50
+-----------------------
+Q=2251799813685255/2251799813685248
+[F-NE-up] +2251799813685255p-51
+[F-NE-up] -2251799813685255p-51
+-----------------------
+ Tie Breaks (NA)
+-----------------------
+Q=562949953421313/562949953421312
+[F-NA-ex] +562949953421313p-49
+[F-NA-ex] -562949953421313p-49
+-----------------------
+Q=2251799813685253/2251799813685248
+[F-NA-lo] +2251799813685253p-51
+[F-NA-lo] -2251799813685253p-51
+-----------------------
+Q=1125899906842627/1125899906842624
+[F-NA-ti] +1125899906842627p-50
+[F-NA-ti] -1125899906842627p-50
+-----------------------
+Q=2251799813685255/2251799813685248
+[F-NA-up] +2251799813685255p-51
+[F-NA-up] -2251799813685255p-51
diff --git a/farith2/tests/mode.ml b/farith2/tests/mode.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8771308e86fff9b01880eece6632d16b0c983832
--- /dev/null
+++ b/farith2/tests/mode.ml
@@ -0,0 +1,43 @@
+module F = Farith2.F
+
+let fpp mode fmt q = F.pp fmt (F.of_q mode ~mw:52 ~ew:11 q)
+
+let () =
+  begin
+    let f = (F.of_float 3.1) in
+    Format.printf "[F]  3.1 = %a@." F.pp f;
+    let q = Q.make (Z.of_int 31) (Z.of_int 10) in
+    Format.printf "[Fp] 3.1 = %a@." F.pp (F.round ~mw:24 ~ew:11 ZR (F.of_float 3.1)) ;
+    Format.printf "[Fq] 3.1 = %a@." F.pp (F.of_q ~mw:24 ~ew:11 ZR q) ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Simple Roundings@." ;
+    let job m m2 q =
+      begin
+        Format.printf "-----------------------@." ;
+        Format.printf "Q=%a@." Q.pp_print q ;
+        Format.printf "[F-%s] %a@." m (fpp m2) q ;
+        Format.printf "[F-%s] %a@." m (fpp m2) (Q.neg q) ;
+      end in
+    job "NE" Farith2.NE q ;
+    job "NA" Farith2.NA q ;
+    job "ZR" Farith2.ZR q ;
+    job "UP" Farith2.UP q ;
+    job "DN" Farith2.DN q ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Tie Breaks (NE)@." ;
+    let eps = Z.shift_left Z.one 51 in
+    let e_ex = Q.make (Z.of_int 0b100) eps in
+    let e_lo = Q.make (Z.of_int 0b101) eps in
+    let e_ti = Q.make (Z.of_int 0b110) eps in
+    let e_up = Q.make (Z.of_int 0b111) eps in
+    job "NE-ex" Farith2.NE (Q.add Q.one e_ex) ;
+    job "NE-lo" Farith2.NE (Q.add Q.one e_lo) ;
+    job "NE-ti" Farith2.NE (Q.add Q.one e_ti) ;
+    job "NE-up" Farith2.NE (Q.add Q.one e_up) ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Tie Breaks (NA)@." ;
+    job "NA-ex" Farith2.NA (Q.add Q.one e_ex) ;
+    job "NA-lo" Farith2.NA (Q.add Q.one e_lo) ;
+    job "NA-ti" Farith2.NA (Q.add Q.one e_ti) ;
+    job "NA-up" Farith2.NA (Q.add Q.one e_up) ;
+  end
diff --git a/farith2/tests/subnormal.expected b/farith2/tests/subnormal.expected
new file mode 100644
index 0000000000000000000000000000000000000000..cf3afb2fcfa9b83fb1f4e2c1e0312639f1c0daff
--- /dev/null
+++ b/farith2/tests/subnormal.expected
@@ -0,0 +1,7 @@
+of-float 1p1023 = +1p1023 (normal)
+of-float 1p1024 = +∞ (infinity)
+of-float 1p-1022 = +1p-1022 (normal)
+of-float 1p-1023 = +1p-1023 (sub-normal)
+of-float 1p-1048 = +1p-1048 (sub-normal)
+of-float 1p-1074 = +1p-1074 (sub-normal)
+of-float 1p-1075 = +0 (zero)
diff --git a/farith2/tests/subnormal.ml b/farith2/tests/subnormal.ml
new file mode 100644
index 0000000000000000000000000000000000000000..75445605cfa730d6285ff08da562fb90aea8f7f1
--- /dev/null
+++ b/farith2/tests/subnormal.ml
@@ -0,0 +1,39 @@
+open Farith2
+
+let eps n = Stdlib.ldexp 1.0 n
+
+let pp_class fmt u =
+  Format.pp_print_string fmt
+    begin
+      match classify_float u with
+      | FP_zero -> "zero"
+      | FP_normal -> "normal"
+      | FP_subnormal -> "sub-normal"
+      | FP_infinite -> "infinity"
+      | FP_nan -> "nan"
+    end
+
+let test_of_float n =
+  let u = eps n in
+    let f = F.of_float u in
+    Format.printf "of-float 1p%d = %a (%a)@." n F.pp f pp_class u
+
+(* let test_to_float n =
+ *   begin
+ *     let u = eps n in
+ *     let f = F.power2 n in
+ *     let v = F.to_float f in
+ *     Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ;
+ *     let fu,eu = Stdlib.frexp u in
+ *     let fv,ev = Stdlib.frexp v in
+ *     Format.printf "   expected = %fp%d@\n" fu eu ;
+ *     Format.printf "   obtained = %fp%d@." fv ev ;
+ *   end *)
+
+let limits = [ 1023;1024;-1022;-1023;-1048;-1074;-1075 ]
+
+let () =
+  begin
+    List.iter test_of_float limits ;
+    (* List.iter test_to_float limits ; *)
+  end
diff --git a/farith2/tests/test.expected b/farith2/tests/test.expected
new file mode 100644
index 0000000000000000000000000000000000000000..e823e1d3c8a5a76637106ea5e407c1e84f389616
--- /dev/null
+++ b/farith2/tests/test.expected
@@ -0,0 +1,18 @@
+Flocq version: 40000
+Run tests with Farith2.F
+   0.100000 + 2.000000 = 2.100000
+   0.100000 : +3602879701896397p-55
+   2.000000 : +1p1
+   2.100000 : +4728779608739021p-51
+-0.100000 + 2.000000 = 1.900000
+-0.100000 : -3602879701896397p-55
+2.000000 : +1p1
+1.900000 : +4278419646001971p-51
+-0.100000 + -2.000000 = -2.100000
+-0.100000 : -3602879701896397p-55
+-2.000000 : -1p1
+-2.100000 : -4728779608739021p-51
+0.100000 + -2.000000 = -1.900000
+0.100000 : +3602879701896397p-55
+-2.000000 : -1p1
+-1.900000 : -4278419646001971p-51
diff --git a/farith2/tests/test.ml b/farith2/tests/test.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2b49f0f1194af80f17037d3b6a435f0bf2f5ba9b
--- /dev/null
+++ b/farith2/tests/test.ml
@@ -0,0 +1,26 @@
+open Format
+
+let () =
+  printf "Flocq version: %a@."
+    Z.pp_print Farith2.flocq_version
+
+open Farith2
+
+module Run = struct
+  let () =
+    printf "@[<3>Run tests with %s@\n" "Farith2.F";
+    let add u v =
+      let fu = F.of_float u in
+      let fv = F.of_float v in
+      let fr = F.add NE fu fv in
+      let r = F.to_float NE fr in
+      printf "%f + %f = %f@\n" u v r;
+      printf "%f : %a@\n" u F.pp fu;
+      printf "%f : %a@\n" v F.pp fv;
+      printf "%f : %a@]@\n" r F.pp fr;
+    in
+    add (0.1)   (2.0);
+    add (-.0.1) (2.0);
+    add (-.0.1) (-.2.0);
+    add (0.1)   (-.2.0)
+end
diff --git a/farith2/tests/tie.expected b/farith2/tests/tie.expected
new file mode 100644
index 0000000000000000000000000000000000000000..8b916f28184d51a62b34e9a8869e04a5557abad1
--- /dev/null
+++ b/farith2/tests/tie.expected
@@ -0,0 +1,22 @@
+------------------------------------------
+         - +4503599627370496    (+1p52)
+1p52+1/2 = +9007199254740993p-1 (+9007199254740993p-1)
+         + +4503599627370497    (+4503599627370497)
+mantissa =  9007199254740992
+=NE +1p52
++NE +1p52 (+4503599627370496)
+-NE -1p52 (-4503599627370496)
+=NA +4503599627370497p0
++NA +4503599627370497 (+4503599627370497)
+-NA -4503599627370497 (-4503599627370497)
+------------------------------------------
+         - +4503599627370497    (+4503599627370497)
+1p52+3/2 = +9007199254740995p-1 (+9007199254740995p-1)
+         + +4503599627370498    (+2251799813685249p1)
+mantissa =  9007199254740992
+=NE +2251799813685249p1
++NE +2251799813685249p1 (+4503599627370498)
+-NE -2251799813685249p1 (-4503599627370498)
+=NA +2251799813685249p1
++NA +2251799813685249p1 (+4503599627370498)
+-NA -2251799813685249p1 (-4503599627370498)
diff --git a/farith2/tests/tie.ml b/farith2/tests/tie.ml
new file mode 100644
index 0000000000000000000000000000000000000000..111be991c70dc4fcc4da0dd674f16da4d87bf04d
--- /dev/null
+++ b/farith2/tests/tie.ml
@@ -0,0 +1,34 @@
+open Farith2
+
+(** not tested *)
+
+let tiebreak a b n =
+  begin
+    (* Tie breaks at [2^(n-1) + e] with [n] bits precision *)
+    let m = n-1 in
+    let up = Q.mul_2exp Q.one m in
+    let q = Q.(up + Q.make (Z.of_int a) (Z.of_int b)) in
+    let f0 = F.of_qint ~bits:(n+1) q in (* exact *)
+    let f1,f2 = F.seize ~bits:n f0 in
+    Format.printf "------------------------------------------@\n" ;
+    Format.printf "         - %a    (%a)@\n" F.pp f1 F.pp f1 ;
+    Format.printf "1p%d+%d/%d = %a (%a)@\n" m a b pp f0 F.pp f0 ;
+    Format.printf "         + %a    (%a)@\n" pp f2 F.pp f2 ;
+    Format.printf "mantissa =  %a@\n" Z.pp_print (Z.shift_left Z.one n) ;
+    let f1 = F.neg f0 in
+    let pos_ne = F.round ~mode:F.NE ~bits:n f0 in
+    let pos_na = F.round ~mode:F.NA ~bits:n f0 in
+    let neg_ne = F.round ~mode:F.NE ~bits:n f1 in
+    let neg_na = F.round ~mode:F.NA ~bits:n f1 in
+    Format.printf "+NE %a (%a)@\n" F.pp pos_ne pp pos_ne ;
+    Format.printf "-NE %a (%a)@\n" F.pp neg_ne pp neg_ne ;
+    Format.printf "+NA %a (%a)@\n" F.pp pos_na pp pos_na ;
+    Format.printf "-NA %a (%a)@\n" F.pp neg_na pp neg_na ;
+    Format.print_flush () ;
+  end
+
+let () =
+  begin
+    tiebreak 1 2 F.b64 ;
+    tiebreak 3 2 F.b64 ;
+  end
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index 85f19507a2204d601e65b7096b993981d3b8715a..1bdb8211fe7663d52a8c0475e92b1397767bfc8f 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -93,18 +93,18 @@ let compute_ground d t =
   | { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; args; _ } ->
       let m, r = IArray.extract2_exn args in
       let r = match !>>>r with Q q -> q | A _ -> assert false (* TODO *) in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m r)
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m r)
   | { app = { builtin = Expr.Fp_to_fp (_ew1, _prec1, ew2, prec2); _ }; args; _ }
     ->
       let m, f1 = IArray.extract2_exn args in
-      !<(F.of_q ~ew:ew2 ~mw:(prec2 - 1) ~mode:!>>m (F.to_q !>f1))
+      !<(F.of_q ~ew:ew2 ~mw:(prec2 - 1) !>>m (F.to_q !>f1))
   | { app = { builtin = Expr.Sbv_to_fp (n, ew, prec); _ }; args; _ } ->
       let m, bv = IArray.extract2_exn args in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m
            (Q.of_bigint (Colibri2_theories_LRA.RealValue.signed_bitv n !>>>bv)))
   | { app = { builtin = Expr.Ubv_to_fp (n, ew, prec); _ }; args; _ } ->
       let m, bv = IArray.extract2_exn args in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m
            (Q.of_bigint
               (Colibri2_theories_LRA.RealValue.unsigned_bitv n !>>>bv)))
   | { app = { builtin = Expr.Fp (ew, prec); _ }; args; _ } ->
@@ -256,7 +256,7 @@ let converter d (f : Ground.t) =
         (set r
            (let* va = getq a in
             match va with
-            | Q va -> Some (F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m va)
+            | Q va -> Some (F.of_q ~ew ~mw:(prec - 1) !>>m va)
             | A _ -> None
             (* TODO *)))
   | { app = { builtin = Expr.NaN (ew, prec); _ }; args; _ } ->