added quotes for filenames;
authorboehmes
Thu Sep 24 15:00:17 2009 +0200 (2009-09-24)
changeset 326755fe601aff9be
parent 32674 b629fbcc5313
child 32677 8854e892cf3e
added quotes for filenames;
truncated remaining time (no floats supported by ulimit)
Admin/E/eproof
     1.1 --- a/Admin/E/eproof	Thu Sep 24 08:28:27 2009 +0200
     1.2 +++ b/Admin/E/eproof	Thu Sep 24 15:00:17 2009 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  
     1.5  use File::Basename qw/ dirname /;
     1.6  use File::Temp qw/ tempfile /;
     1.7 +use English;
     1.8  
     1.9  
    1.10  # E executables
    1.11 @@ -44,7 +45,7 @@
    1.12  # run E, redirecting output into a temporary file
    1.13  
    1.14  my ($fh, $filename) = tempfile(UNLINK => 1);
    1.15 -my $r = system "$eprover_cmd > $filename";
    1.16 +my $r = system "$eprover_cmd > '$filename'";
    1.17  exit ($r >> 8) if $r != 0;
    1.18  
    1.19  
    1.20 @@ -55,7 +56,7 @@
    1.21    # Note: Like the original eproof, we only look at the last 60 lines.
    1.22  
    1.23  if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
    1.24 -  $timelimit = $timelimit - $1 - 1;
    1.25 +  $timelimit = int($timelimit - $1 - 1);
    1.26  
    1.27    if ($content =~ m/No proof found!/) {
    1.28      print "# Problem is satisfiable (or invalid), " .
    1.29 @@ -85,7 +86,7 @@
    1.30    print if (m/# SZS status/ or m/"# Failure"/);
    1.31  }
    1.32  $r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
    1.33 -  "'$epclextract' $format -f --competition-framing $filename\"");
    1.34 +  "'$epclextract' $format -f --competition-framing '$filename'\"");
    1.35    # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
    1.36    # and prints and error message. How could we then limit the execution time?
    1.37  exit ($r >> 8);