equal
deleted
inserted
replaced
37 } |
37 } |
38 if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) { |
38 if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) { |
39 $metis_succeeded++; |
39 $metis_succeeded++; |
40 $metis_time += $1; |
40 $metis_time += $1; |
41 } |
41 } |
42 if (m/^metis \(sledgehammer\): time out/) { |
42 if (m/^metis \(sledgehammer\): timeout/) { |
43 $metis_timeout++; |
43 $metis_timeout++; |
44 } |
44 } |
45 } |
45 } |
46 |
46 |
47 open(FILE, ">>$log_file") || die "Cannot open file '$log_file'"; |
47 open(FILE, ">>$log_file") || die "Cannot open file '$log_file'"; |