src/HOL/Tools/SMT/lib/scripts/z3_wrapper
Fri, 17 Dec 2010 11:12:37 +0100 blanchet Z3 sometimes reports two errors, with the first one referring to line 1 for some strange reason -- but it makes no sense to kill line 1, so we traverse the errors in reverse and consider only the last error
Fri, 17 Dec 2010 00:11:06 +0100 blanchet fixed off-by-one and return proper error code -- never underestimate the number of oddities in Perl
Thu, 16 Dec 2010 22:43:22 +0100 blanchet keep track of errors in Z3 input file for debugging purposes
Thu, 16 Dec 2010 21:53:31 +0100 blanchet better propagation of stdout in case of failure + comply with strict/warnings
Thu, 16 Dec 2010 21:21:13 +0100 blanchet cleaner handling of temporary files
Thu, 16 Dec 2010 21:02:08 +0100 blanchet added self-correcting wrapper for Z3 -- see comment in the file for details
less more (0) tip