# HG changeset patch
# User blanchet
# Date 1292530873 -3600
# Node ID 5cee84180cd77162ea727e85f73d16d319018fbc
# Parent  ee24717e3fe39e490fb82a2d2a00e072e7b808a5
cleaner handling of temporary files

diff -r ee24717e3fe3 -r 5cee84180cd7 src/HOL/Tools/SMT/lib/scripts/z3_wrapper
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:02:08 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:21:13 2010 +0100
@@ -10,9 +10,13 @@
 #
 # in your "~/.isabelle/etc/settings" file.
 
+use POSIX;
+
 my $in_file = @ARGV[$ARGV - 1];
-my $out_file = "/tmp/foo"; # FIXME
-my $err_file = "/tmp/bar"; # FIXME
+my $out_file = tmpnam();
+my $err_file = tmpnam();
+
+print ;
 
 $ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set";
 
@@ -28,6 +32,7 @@
   open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\"";
   my @err_lines = <ERR_FILE>;
   close(ERR_FILE);
+  print STDERR @err_lines;
   foreach (@err_lines) {
     if (m/[lL]ine ([0-9]+)/) {
       open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\"";
@@ -40,6 +45,8 @@
       goto RUN;
     }
   }
-  print STDERR @err_lines;
-  exit $code;
 }
+
+unlink($out_file);
+unlink($err_file);
+exit $code;