Refactor the Z3 solver backend (ocaml#4878)

rjbou · Nov 11, 2021 · d812c59 · d812c59
1 parent f3b6c47
commit d812c59
Show file tree

Hide file tree

Showing 6 changed files with 244 additions and 146 deletions.
diff --git a/master_changes.md b/master_changes.md
@@ -130,6 +130,7 @@ users)
 ## Solver
   * [BUG] Remove z3 debug output [#4723 @rjbou - fix #4717] [2.1.0~rc2 #4720]
   * Fix and improve the Z3 solver backend [#4880 @altgr]
+  * Refactored, fixed, improved and optimised the z3 solver backend [#4878 @altgr]
 
 ## Client
   *

diff --git a/src/core/opamConsole.ml b/src/core/opamConsole.ml
@@ -506,12 +506,9 @@ let print_message =
 
 let timestamp () =
   let time = Unix.gettimeofday () -. global_start_time in
-  let tm = Unix.gmtime time in
-  let msec = time -. (floor time) in
-  Printf.ksprintf (colorise `blue) "%.2d:%.2d.%.3d"
-    (tm.Unix.tm_hour * 60 + tm.Unix.tm_min)
-    tm.Unix.tm_sec
-    (int_of_float (1000.0 *. msec))
+  Printf.ksprintf (colorise `blue) "%02.0f:%06.3f"
+    (time /. 60.)
+    (mod_float time 60.)
 
 let log_formatter, finalise_output =
   if Sys.win32 then