remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper Wed Feb 09 17:18:57 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Jasmin Blanchette, TU Muenchen
-#
-# Invoke Z3 with error detection and correction.
-# To use this wrapper, set
-#
-# Z3_REAL_SOLVER=/path-to-z3/z3
-# Z3_SOLVER=$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/z3_wrapper
-#
-# in your "~/.isabelle/etc/settings" file.
-
-use strict;
-use warnings;
-use POSIX;
-
-my $in_file = $ARGV[$#ARGV];
-my $out_file = tmpnam();
-my $err_file = tmpnam();
-
-$ENV{'Z3_REAL_SOLVER'} || exit 10;
-
-RUN:
-my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file";
-
-open(ERR_FILE, "<$err_file") || exit 11;
-my @err_lines = <ERR_FILE>;
-close(ERR_FILE);
-print STDERR join("", @err_lines);
-
-if ($code != 0) {
- foreach my $err_line (reverse(@err_lines)) {
- if ($err_line =~ /[lL]ine ([0-9]+)/) {
- my $line_num = $1;
-
- open(IN_FILE, "<$in_file") || exit 12;
- my @in_lines = <IN_FILE>;
- close(IN_FILE);
-
- $err_line =~ s/[\n\r]//g;
- $in_lines[$line_num - 1] = ";;; " . $err_line . " -- "
- . $in_lines[$line_num - 1];
-
- open(IN_FILE, ">$in_file") || exit 13;
- print IN_FILE join ("", @in_lines);
- close(IN_FILE);
- goto RUN;
- }
- }
-}
-
-open(OUT_FILE, "<$out_file") || exit 14;
-my @out_lines = <OUT_FILE>;
-close(OUT_FILE);
-print join("", @out_lines);
-
-unlink($out_file);
-unlink($err_file);
-exit(($code >> 8 | $code) & 0xff);