[SMT-COMP] [SMT-LIB] How to submit benchmarks to smtlib

Tue Mar 17 08:49:46 EDT 2015

When accepting benchmarks for the 2014 competition we required

- benchmark in valid SMT-LIB form with correct logic in the set-logic 
command (and actually there is an undefined subset of SMT-LIB that is 
used for competition...)

- the status known and set using (set-info :status xxx ) in the 
benchmark: sat or unsat (or unknown if necessary)

- the metadata populated for these  keys

(set-info :source |<information about where the benchmark came from
including author contact, paper citations, etc.>|)
(set-info :smt-lib-version 2.0)
(set-info :category <either "industrial", "crafted", or "random">)

The category values need the quotes

I'm presuming the SMT_COMP 2015 will use SMT-LIB 2.0, not 2.5. If the 
latter, set-info will become meta-info.

- David

On 3/17/2015 8:33 AM, Christoph Wintersteiger wrote:
> Hi Florian,
>
> That sounds great, we definitely want your benchmarks! I'm the keeper of the library for all things FP and BV, so somehow we need to get them from you to me. Are they small enough for an email attachment?
>
> Cheers,
> Christoph
>
>
> Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter
>
>
> Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB
>
> -----Original Message-----
> From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Florian Schanda
> Sent: 17 March 2015 11:49
> To: smt-lib at cs.nyu.edu
> Subject: [SMT-LIB] How to submit benchmarks to smtlib
>
> Hi,
>
> I am compiling benchmarks for QF_FP and QF_FPBV (and probably more) that have been inspired by the kind of floating point issues we and our users have in SPARK (http://www.spark-2014.org)
>
> I've looked on smt-lib.org but I could not actually find any instructions on how I would go about submitting them. What should I do?
>
> Thanks,
>
> 	Florian
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib