equal
deleted
inserted
replaced
94 Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input |
94 Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input |
95 val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
95 val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err |
96 |
96 |
97 val output = drop_suffix (equal "") res |
97 val output = drop_suffix (equal "") res |
98 val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output |
98 val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output |
99 val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)] |
99 val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] |
100 val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)] |
100 val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] |
101 |
101 |
102 val _ = member (op =) normal_return_codes return_code orelse |
102 val _ = member (op =) normal_return_codes return_code orelse |
103 raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
103 raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
104 in output end |
104 in output end |
105 |
105 |