src/HOL/Mirabelle/lib/scripts/report.pl

 my $sh_succeeded = 0;
 my $sh_time = 0;
 
 my $metis_calls = 0;
 my $metis_succeeded = 0;
-my $metis_time_out = 0;
+my $metis_timeout = 0;
 my $metis_time = 0;
 
 foreach (@lines) {
   if (m/^unhandled exception/) {
     $unhandled++;

   if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
     $metis_succeeded++;
     $metis_time += $1;
   }
   if (m/^metis \(sledgehammer\): time out/) {
-    $metis_time_out++;
+    $metis_timeout++;
   }
 }
 
 open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
 

 if ($sh_calls > 0) {
   my $percent = $sh_succeeded / $sh_calls * 100;
   my $time = $sh_time / 1000;
   my $avg_time = $time / $sh_succeeded;
   print FILE "Total number of sledgehammer calls: $sh_calls\n";
-  print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
-  printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
+  print FILE "Number of successful sledgehammer calls:  $sh_succeeded\n";
+  printf FILE "Success rate: %.0f%%\n", $percent;
   printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
   printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
 }
 
 if ($metis_calls > 0) {
   my $percent = $metis_succeeded / $metis_calls * 100;
   my $time = $metis_time / 1000;
   my $avg_time = $time / $metis_succeeded;
+  my $metis_exc = $sh_succeeded - $metis_succeeded - $metis_timeout;
   print FILE "Total number of metis calls: $metis_calls\n";
   print FILE "Number of successful metis calls: $metis_succeeded\n";
-  print FILE "Number of metis time outs: $metis_time_out\n";
-  printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
+  print FILE "Number of metis timeouts: $metis_timeout\n";
+  print FILE "Number of metis exceptions: $metis_exc\n";
+  printf FILE "Success rate: %.0f%%\n", $percent;
   printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
   printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
 }
 
 close(FILE);