Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Tjark W. <tja...@it...> - 2015-02-11 15:19:16
|
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 |