Merge branch 'master' into wip-produce-smtlib-models

.ocamlformat

@@ -1,4 +1,4 @@
-version = 0.20.1
+version = 0.24.1
 profile=conventional
 margin=80
 if-then-else=k-r

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
   )

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"}
 ]

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 =

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