12 |
12 |
13 use strict; |
13 use strict; |
14 use warnings; |
14 use warnings; |
15 use POSIX; |
15 use POSIX; |
16 |
16 |
17 my $in_file = $ARGV[$#ARGV - 1]; |
17 my $in_file = $ARGV[$#ARGV]; |
18 my $out_file = tmpnam(); |
18 my $out_file = tmpnam(); |
19 my $err_file = tmpnam(); |
19 my $err_file = tmpnam(); |
20 |
20 |
21 $ENV{'Z3_REAL_SOLVER'} || die "Environment variable \"Z3_REAL_SOLVER\" not set"; |
21 $ENV{'Z3_REAL_SOLVER'} || exit 10; |
22 |
22 |
23 RUN: |
23 RUN: |
24 my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file"; |
24 my $code = system $ENV{'Z3_REAL_SOLVER'} . " " . join(" ", @ARGV) . " >$out_file 2>$err_file"; |
25 |
25 |
26 open(ERR_FILE, "<$err_file") || die "Cannot open file \"$err_file\""; |
26 open(ERR_FILE, "<$err_file") || exit 11; |
27 my @err_lines = <ERR_FILE>; |
27 my @err_lines = <ERR_FILE>; |
28 close(ERR_FILE); |
28 close(ERR_FILE); |
29 print STDERR join("", @err_lines); |
29 print STDERR join("", @err_lines); |
30 |
30 |
31 if ($code != 0) { |
31 if ($code != 0) { |
32 foreach my $err_line (@err_lines) { |
32 foreach my $err_line (@err_lines) { |
33 if ($err_line =~ /[lL]ine ([0-9]+)/) { |
33 if ($err_line =~ /[lL]ine ([0-9]+)/) { |
34 my $line_num = $1; |
34 my $line_num = $1; |
35 |
35 |
36 open(IN_FILE, "<$in_file") || die "Cannot open file \"$in_file\""; |
36 open(IN_FILE, "<$in_file") || exit 12; |
37 my @in_lines = <IN_FILE>; |
37 my @in_lines = <IN_FILE>; |
38 close(IN_FILE); |
38 close(IN_FILE); |
39 |
39 |
40 $err_line =~ s/[\n\r]//g; |
40 $err_line =~ s/[\n\r]//g; |
41 $in_lines[$line_num - 1] = ";;; " . $err_line . " -- " |
41 $in_lines[$line_num - 1] = ";;; " . $err_line . " -- " |
42 . $in_lines[$line_num - 1]; |
42 . $in_lines[$line_num - 1]; |
43 |
43 |
44 open(IN_FILE, ">$in_file") || die "Cannot open file \"$in_file\""; |
44 open(IN_FILE, ">$in_file") || exit 13; |
45 print IN_FILE join ("", @in_lines); |
45 print IN_FILE join ("", @in_lines); |
46 close(IN_FILE); |
46 close(IN_FILE); |
47 goto RUN; |
47 goto RUN; |
48 } |
48 } |
49 } |
49 } |
50 } |
50 } |
51 |
51 |
52 open(OUT_FILE, "<$out_file") || die "Cannot open file \"$out_file\""; |
52 open(OUT_FILE, "<$out_file") || exit 14; |
53 my @out_lines = <OUT_FILE>; |
53 my @out_lines = <OUT_FILE>; |
54 close(OUT_FILE); |
54 close(OUT_FILE); |
55 print join("", @out_lines); |
55 print join("", @out_lines); |
56 |
56 |
57 unlink($out_file); |
57 unlink($out_file); |
58 unlink($err_file); |
58 unlink($err_file); |
59 exit $code; |
59 exit(($code >> 8 | $code) & 0xff); |