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

[Tjark W. <tja...@it...>]

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