[SMT-LIB] submitting SMTLIB2 benchmarks?

[Tinelli, Cesare]

On 26 Jul 2013, at 18:36, Martin Brain <martin.brain at cs.ox.ac.uk> wrote:

> 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!
> 
Philipp, thanks for the updated file with the theory declarations.


> 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.
> 
Thanks, Martin. I'll get back to you on this later. 

Again tough, the main need is for benchmarks that would use some of those theories (finite sets, finite maps, finite relations, ...).

Ranjit has provided some with sets. It would be good to have more from other sources.

Cheers, 


Cesare

> Cheers,
> - Martin
> 
>