--- a/src/HOL/Tools/SMT/smt_solver.ML Thu Oct 15 14:31:55 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Oct 15 14:42:05 2020 +0200
@@ -96,8 +96,8 @@
val output = drop_suffix (equal "") res
val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
- val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)]
- val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)]
+ val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
+ val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
val _ = member (op =) normal_return_codes return_code orelse
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)