[SMT-LIB] How to submit benchmarks to smtlib

[Christoph Wintersteiger]

Hi Florian,

Fantastic, thanks a lot!

Of course, when you get new ones, send them directly to me and I'll add them to the library. The "everything" benchmarks are of course also interesting, but not all solvers might support that (Z3 does, but I don't know about the others). 

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: Florian Schanda [mailto:florian.schanda at altran.com] 
Sent: 17 March 2015 13:22
To: Christoph Wintersteiger
Cc: smt-lib at cs.nyu.edu; David R. Cok; smt-comp at cs.nyu.edu
Subject: Re: [SMT-LIB] How to submit benchmarks to smtlib

On Tuesday 17 Mar 2015 12:33:26 Christoph Wintersteiger wrote:
> 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?

Sure - attached and annotated as David noted, split up into QF_FP and QF_FPBV. 
I've used the smtlib 2.5 syntax but its obviously not hard to change.

I will produce more as time goes on, shall I email them directly to you once I have more?

I will also have benchmarks that combine pretty much everything (AUFBVFPNIRA); where should something like that go?

Thanks,

	Florian