[SMT-COMP] SMT-COMP 2016: Main Track Test Job

[Christoph Wintersteiger]

Hi all,

Could you explain what the result "starexec-unknown" means?

Regarding the benchmarks in QF_FP\wintersteiger\rem: Those have very recently (less than two months ago) been updated, because when they were first generated, the wrong semantics of the fp.rem operator were used. Not all solver developers may have realized this yet. The current benchmarks should hopefully be correct, but solvers that were not updated yet may produce wrong results (so does z3 4.4.1; and the latest development version is still not fully compliant either). I'd suggest not to use these benchmarks in the competition (the other QF_FP\wintersteiger\* should be ok though), but I'll leave that decision to the organizers of course. 

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: 27 May 2016 13:04
To: smt-comp at cs.nyu.edu
Cc: Sylvain Conchon <Sylvain.Conchon at lri.fr>; David Deharbe <david at dimap.ufrn.br>
Subject: [SMT-COMP] SMT-COMP 2016: Main Track Test Job

Dear SMT-COMP participants,

I have run a small test job on StarExec to exercise all main track solvers on a small number of benchmarks from each division. The results are available at https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fwww.starexec.org%2fstarexec%2fsecure%2fdetails%2fjob.jsp%3fid%3d15862&data=01%7c01%7ccwinter%40064d.mgd.microsoft.com%7c5a378e2e458d4b1b824208d3862713fa%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=uLhZ9H6NilXmxA3P57A3D%2fZykhYlpgPUO7E82inj9NM%3d

I would suggest that you investigate results flagged as wrong. The competition will use a more liberal post-processor that attempts to ignore malformed output, but you might still want to ensure that your solver is compliant with SMT-LIB (or notify us if there are ill-formed benchmarks).

Please let me know if your solver was tested in divisions where it should not be competing, and vice versa.

If your main track solver was not tested, then it was not visible to me on StarExec. If you have updated your solver since its first submission, please let me know the new solver ID before the final solver deadline, and remember to make your solver visible.

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%7c5a378e2e458d4b1b824208d3862713fa%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=KDV7Z2r3Zp8I%2bEE3u5vnofFtViHcPLVETEqfJpOfUh8%3d