diff --git a/.ocamlformat b/.ocamlformat
index 777b2f13..2ea44df4 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version = 0.20.1
+version = 0.24.1
 profile=conventional
 margin=80
 if-then-else=k-r
diff --git a/dune-project b/dune-project
index 244f1a5c..6ec16743 100644
--- a/dune-project
+++ b/dune-project
@@ -33,7 +33,8 @@
   (alcotest :with-test)
   (odoc :with-doc))
  (depopts
-  mtime ; for profiling stuff
+  (mtime
+   (>= 2.0)) ; for profiling stuff
   memtrace ; memory profiling
   zarith ; for arith
   )
diff --git a/sidekick.opam b/sidekick.opam
index c82c4a08..671080eb 100644
--- a/sidekick.opam
+++ b/sidekick.opam
@@ -16,7 +16,11 @@ depends: [
   "alcotest" {with-test}
   "odoc" {with-doc}
 ]
-depopts: ["mtime" "memtrace" "zarith"]
+depopts: [
+  "mtime" {>= "2.0"}
+  "memtrace"
+  "zarith"
+]
 conflicts: [
   "zarith" {< "1.8"}
 ]
diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml
index 0a8c4ecb..9a572b91 100644
--- a/src/smtlib/Driver.ml
+++ b/src/smtlib/Driver.ml
@@ -69,7 +69,10 @@ let decl_fun (self : t) f args ret const : unit =
 let build_model (self : t) (sat : Solver.sat_result) : Model.t =
   Build_model.build self.build_model sat
 
-let check_model (self : t) (m : Model.t) : unit = assert false
+(* FIXME *)
+let check_model (_self : t) (_m : Model.t) : unit =
+  Log.debugf 0 (fun k -> k "; TODO: check model");
+  ()
 
 (* call the solver to check satisfiability *)
 let solve (self : t) ~assumptions () : Solver.res =
diff --git a/src/tef/Sidekick_tef.real.ml b/src/tef/Sidekick_tef.real.ml
index e025ca10..61e698f8 100644
--- a/src/tef/Sidekick_tef.real.ml
+++ b/src/tef/Sidekick_tef.real.ml
@@ -31,7 +31,7 @@ module Make () : P.BACKEND = struct
 
   let get_ts () : float =
     let now = Mtime_clock.now () in
-    Mtime.Span.to_us (Mtime.span program_start now)
+    Mtime.Span.to_float_ns (Mtime.span program_start now) /. 1e3
 
   let emit_sep_ () =
     if !first_ then