[SMT-LIB] FP demo track at SMT-COMP

Christoph Wintersteiger cwinter at microsoft.com
Wed Jun 10 08:53:20 EDT 2015


Hi all,

So far, none of the submissions to SMT-COMP 2015 have select QF_FP or QF_BVFP as categories they would like to take part in:
http://smtcomp.sourceforge.net/2015/participants.shtml

We would like to run the floating-point demo track alongside the other competition track, i.e., starting June 14. So, if you would like to participate, please let us know as soon as possible. As Tjark said, if we don't hear from you, your solver(s) will not take part.

If you want to take a look at the latest benchmarks before committing to it, they are available on starexec in root/SMT/SMT-LIB benchmarks/2015-06-01/non-incremental/QF_FP and .../QF_BVFP.

Thanks,
Christoph


Tjark Weber tjark.weber at it.uu.se <mailto:smt-comp%40cs.nyu.edu?Subject=Re%3A%20%5BSMT-COMP%5D%20Floating-Point%20Divisions&In-Reply-To=%3C1433712417.3478.33.camel%40it.uu.se%3E>
Sun Jun 7 17:26:57 EDT 2015

  *   Previous message: [SMT-COMP] SMT-COMP 2015: Benchmarks and Tools Available <http://cs.nyu.edu/pipermail/smt-comp/2015/000327.html>
  *   Next message: [SMT-COMP] SMT-COMP 2015: exit Command Optional <http://cs.nyu.edu/pipermail/smt-comp/2015/000329.html>
  *   Messages sorted by: [ date ]<http://cs.nyu.edu/pipermail/smt-comp/2015/date.html#328> [ thread ]<http://cs.nyu.edu/pipermail/smt-comp/2015/thread.html#328> [ subject ]<http://cs.nyu.edu/pipermail/smt-comp/2015/subject.html#328> [ author ]<http://cs.nyu.edu/pipermail/smt-comp/2015/author.html#328>

________________________________

Dear SMT-COMP participants,



The recent 2015-06-01 release of SMT-LIB features floating-point

benchmarks in two new logics, QF_BVFP and QF_FP. Accordingly, SMT-COMP

2015 will have two experimental floating-point divisions.



Please let us know before the final solver deadline on June 14 if you

wish to enter your solver(s) into one or both of QF_BVFP and QF_FP.



We will not enter your solver(s) into these divisions unless we hear

from you, even if you previously entered your solver into "all

divisions."



Best,

Tjark



Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter<http://research.microsoft.com/people/cwinter>

[MSFT_logo_Gray DE sized SIG1.png]
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.jpg
Type: image/jpeg
Size: 1168 bytes
Desc: image001.jpg
URL: </pipermail/smt-lib/attachments/20150610/e8ca408e/attachment.jpg>


More information about the SMT-LIB mailing list