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

[Michal Moskal]

On 1/13/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > While I still haven't got the original Simplify files that were used
> > to generate those (maybe somebody has them around?), I have some other
> > ESC/Java benchmarks generated by running it on parts of its own source
> > code. I also used Boogie benchmarks available on the Spec# web page.
>
> The benchmarks can be found bundled with the Simplify theorem prover.  I put
> up
> a tarball of the benchmarks here:
> http://www.cs.nyu.edu/~barrett/tmp/simplify_benchmarks.tar.gz
>

Thank you!

> We've been looking at doing the same translation ourselves, but I'm always
> happy to let someone else do the work :)
>
> We'll take a closer look at your translation and get back to you about it.

It seems my treatment of (DEFPRED (foo x y) (some formula with x y))
is wrong. I  though of it as a macro-definition, but it turns out
'foo' is used in triggers (and it seems to matter in some benchmarks).
I'll try to fix it, as soon as I get back home from Nice.


-- 
   Michał