# HG changeset patch
# User blanchet
# Date 1292532811 -3600
# Node ID 028449eb1548aa92f4a3318e7dfa786822a7ec53
# Parent  fc9a6d2d7b760812a09a891590262c2483ae03c5
better propagation of stdout in case of failure + comply with strict/warnings

diff -r fc9a6d2d7b76 -r 028449eb1548 src/HOL/Tools/SMT/lib/scripts/z3_wrapper
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:21:52 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:53:31 2010 +0100
@@ -10,29 +10,25 @@
 #
 # in your "~/.isabelle/etc/settings" file.
 
+use strict;
+use warnings;
 use POSIX;
 
-my $in_file = @ARGV[$ARGV - 1];
+my $in_file = $ARGV[$#ARGV - 1];
 my $out_file = tmpnam();
 my $err_file = tmpnam();
 
-print ;
-
 $ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set";
 
 RUN:
 my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file";
 
-if ($code == 0) {
-  open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\"";
-  my @out_lines = <OUT_FILE>;
-  close(OUT_FILE);
-  print @out_lines;
-} else {
-  open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\"";
-  my @err_lines = <ERR_FILE>;
-  close(ERR_FILE);
-  print STDERR @err_lines;
+open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\"";
+my @err_lines = <ERR_FILE>;
+close(ERR_FILE);
+print STDERR join("", @err_lines);
+
+if ($code != 0) {
   foreach (@err_lines) {
     if (m/[lL]ine ([0-9]+)/) {
       open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\"";
@@ -47,6 +43,11 @@
   }
 }
 
+open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\"";
+my @out_lines = <OUT_FILE>;
+close(OUT_FILE);
+print join("", @out_lines);
+
 unlink($out_file);
 unlink($err_file);
 exit $code;