Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category

[Christoph W. <cw...@mi...>]

Hi Tjark,

I've uploaded a first set of benchmarks for QF_FP onto starexec, they are in SMT-LIB benchmarks/2015/non-incremental/QF_FP. I've added you to the user list, I hope that makes them visible to you but if not, let me know.

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: Tjark Weber [mailto:tja...@it...] 
Sent: 11 February 2015 15:19
To: Christoph Wintersteiger
Cc: smt...@li...; Martin Brain; ces...@ui...
Subject: Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category

Christoph,

On Wed, 2015-02-11 at 14:20 +0000, Christoph Wintersteiger wrote:
> Martin Brain and I discussed the possibility of a category for 
> floating-point arithmetic at this year’s SMT comp. We believe that 
> there are enough solvers and sufficient interest, and the theory 
> definition has recently been finalized. We are happy to collect 
> benchmarks (we have a few ready) and to assist with the running of the 
> competition if there are any issues of course. What would be the next 
> steps for us to make this happen?

I think this is an excellent suggestion. I reckon the next step would be for you to make these benchmarks available to us, so that they can be reviewed and (hopefully) incorporated into SMT-LIB.

Best,
Tjark