[SMT-LIB] logic for ESC/Java and Boogie benchmarks

[Jim Saxe]

Michal,

I wrote, at the end of my reply to your message about trying to
translate ESC/Java verification conditions to SMT-Lib format:

 >There are many more details to how ESC/Java generates verification
 >conditions than I can go into here ...

I should add that much of what ESC/Java does is explained in the
design notes available at

    
http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/design-notes/

particularly notes ESCJ 8a ("The logic of ESC/Java"), and ESCJ 16c
("Java to Guarded Commands translation").  These notes are not be
totally up-to-date and accurate.  In particular, I know that there
are many small changes and corrections for ESCJ 16c that never got
put into the on-line copy after active work on the project at Compaq
started winding down.  Nonetheless, you may find these notes quite
helpful if you run into something that seems mysterious from just
looking at the Simplify input files.

Regards,
--Jim Saxe