# HG changeset patch
# User blanchet
# Date 1292535802 -3600
# Node ID 41f3fdc49ec3877f3f35c073771a5640e72aeaea
# Parent  028449eb1548aa92f4a3318e7dfa786822a7ec53
keep track of errors in Z3 input file for debugging purposes

diff -r 028449eb1548 -r 41f3fdc49ec3 src/HOL/Tools/SMT/lib/scripts/z3_wrapper
--- a/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 21:53:31 2010 +0100
+++ b/src/HOL/Tools/SMT/lib/scripts/z3_wrapper	Thu Dec 16 22:43:22 2010 +0100
@@ -29,12 +29,18 @@
 print STDERR join("", @err_lines);
 
 if ($code != 0) {
-  foreach (@err_lines) {
-    if (m/[lL]ine ([0-9]+)/) {
+  foreach my $err_line (@err_lines) {
+    if ($err_line =~ /[lL]ine ([0-9]+)/) {
+      my $line_num = $1;
+
       open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\"";
       my @in_lines = <IN_FILE>;
       close(IN_FILE);
-      delete $in_lines[$1 - 1];
+
+      $err_line =~ s/[\n\r]//g;
+      $in_lines[$line_num - 1] = ";;; " . $err_line . " -- "
+                                 . $in_lines[$line_num - 1];
+
       open(IN_FILE, ">$in_file") || die "Cannot open file \"$in_file\"";
       print IN_FILE join ("", @in_lines);
       close(IN_FILE);