[SMT-LIB] submitting SMTLIB2 benchmarks?

[Martin Brain]

On Sun, 2013-07-21 at 21:58 +0200, Philipp Ruemmer wrote:
> Hi Cesare & all,
> 
> On Sat, 2013-07-20 at 21:16 +0000, Tinelli, Cesare wrote:
> > 
> > We worked out a declaration with Philipp Ruemmer a while ago based on
> > a larger proposal by him, Daniel Kroening and Georg Weissenbacher
> > (http://www.philipp.ruemmer.org/publications/smt-lsm.pdf).
> > But the theory was never added because, as I recall, the promise of
> > benchmarks did not materialize in the end (apologies to Philipp if I
> > am misremembering this now).
> 
> That is largely correct I'm afraid. We were expecting to obtain larger
> amounts of verification conditions involving sets (and other datatypes),
> but in the end did not really get to this point. Since quite some work
> went into working out syntax and semantics of the theories, it would be
> great if this effort could be continued of course!

FWIW, Daniel mentioned wanting to continue this work to me when I first
arrived and it is nominally on my todo list.  In practise I highly doubt
I'll have time but there is interest in continuing the work here and if
anyone else wants to pick this up we'd be glad to assist.

Cheers,
 - Martin