# HG changeset patch
# User boehmes
# Date 1253797217 -7200
# Node ID 5fe601aff9bec26a770cf942310edeb659c00d8f
# Parent  b629fbcc53134d2e7193db037ca4ccf5804fae46
added quotes for filenames;
truncated remaining time (no floats supported by ulimit)

diff -r b629fbcc5313 -r 5fe601aff9be Admin/E/eproof
--- a/Admin/E/eproof	Thu Sep 24 08:28:27 2009 +0200
+++ b/Admin/E/eproof	Thu Sep 24 15:00:17 2009 +0200
@@ -11,6 +11,7 @@
 
 use File::Basename qw/ dirname /;
 use File::Temp qw/ tempfile /;
+use English;
 
 
 # E executables
@@ -44,7 +45,7 @@
 # run E, redirecting output into a temporary file
 
 my ($fh, $filename) = tempfile(UNLINK => 1);
-my $r = system "$eprover_cmd > $filename";
+my $r = system "$eprover_cmd > '$filename'";
 exit ($r >> 8) if $r != 0;
 
 
@@ -55,7 +56,7 @@
   # Note: Like the original eproof, we only look at the last 60 lines.
 
 if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
-  $timelimit = $timelimit - $1 - 1;
+  $timelimit = int($timelimit - $1 - 1);
 
   if ($content =~ m/No proof found!/) {
     print "# Problem is satisfiable (or invalid), " .
@@ -85,7 +86,7 @@
   print if (m/# SZS status/ or m/"# Failure"/);
 }
 $r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
-  "'$epclextract' $format -f --competition-framing $filename\"");
+  "'$epclextract' $format -f --competition-framing '$filename'\"");
   # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
   # and prints and error message. How could we then limit the execution time?
 exit ($r >> 8);