# HG changeset patch
# User blanchet
# Date 1292530912 -3600
# Node ID fc9a6d2d7b760812a09a891590262c2483ae03c5
# Parent  5cee84180cd77162ea727e85f73d16d319018fbc# Parent  ebeb9424c54b10faa009131eb45b4fd2af895d16
merge

diff -r ebeb9424c54b -r fc9a6d2d7b76 src/HOL/Tools/SMT/lib/scripts/z3_wrapper
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 20:14:21 2010 +0000
+++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:21:52 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;