[SMT-LIB] [SMT-COMP] SMT-COMP 2016: Draft Rules and Timeline Available

[Christoph Wintersteiger]

Hi all,

Yes, that was the reason and indeed, the rest is just basic test cases. What would be the procedure for assigning statuses? Can we just run a couple of solvers and assign a status if they agree on them?

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: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of Tjark Weber
Sent: 13 May 2016 13:01
To: Zhoulai Fu <wbd0730 at 163.com>
Cc: Zhoulai <zell08v at gmail.com>; David Deharbe <david.deharbe at clearsy.com>; Sylvain Conchon <sylvain.conchon at lri.fr>; smt-lib <smt-lib at cs.nyu.edu>; smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

Zhoulai,

On Fri, 2016-05-13 at 13:26 +0800, Zhoulai Fu wrote:

> I find that Alberto Griggio proposed >200 benchmarks for the SMT-COMP 
> 15'QF_FP division, but for some reason they were not used in the final
> competition.    Would you let me know whether those benchmarks will be
> used in this year's competition?  In fact,  since the other 2015's 
> QF_FP benchmarks  mostly consist in sanity checks (e.g. "x==1e-242 /\ 
> y == 1e-197") only and can even be solved via a quick syntax analysis 
> I guess, will you add more challenging floating-point benchmarks such 
> as Griggio's for SMT-COMP 2016?  Thanks for your help.

If I remember correctly, Griggio's benchmarks were ineligible for the competition because their satisfiability status was unknown. I do not think that this has changed until now.

Ideally, we (or the SMT-LIB maintainers) would make an attempt to determine the status of these benchmarks, and then include them in the competition. However, I am not very confident that there will be enough time to do this before the benchmark freeze for 2016.

Best,
Tjark


_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fcs.nyu.edu%2fmailman%2flistinfo%2fsmt-comp&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c11c88759a8554d25588008d37b26712c%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=UuB57bytOvzy903zFi5RAsvCYXIasevdVKyeuT6Irm8%3d