[SMT-COMP] SMT-COMP 2015: All Jobs Complete

[Christoph Wintersteiger]

Hi all,

Yes, the files didn't contain status values, and I didn't want to use Z3's result or values copied over from the corresponding files that contain real-numbered numerals as I didn't want to introduce faulty values. 

I'm a bit surprised to see that only Z3 and MathSAT took part though, was there a problem with other solvers (sonolar, CVC4?) or did they simply not submit a solver?

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: Tjark Weber [mailto:tjark.weber at it.uu.se] 
Sent: 23 June 2015 10:36
To: Alberto Griggio
Cc: smt-comp at cs.nyu.edu; Sylvain Conchon; David Deharbe; Christoph Wintersteiger
Subject: Re: [SMT-COMP] SMT-COMP 2015: All Jobs Complete

Alberto,

On Tue, 2015-06-23 at 08:41 +0200, Alberto Griggio wrote:
> I just had a quick look at QF_FP, and IIUC only "schanda" and 
> "wintersteiger" benchmarks were considered, but not "griggio/fmcad12"
> (at least looking at
> https://www.starexec.org/starexec/secure/details/job.jsp?id=7772)
> Is this a mistake, or have those benchmarks been excluded on purpose?

As far as I can see, all benchmarks in QF_FP/griggio/fmcad12 have "unknown" status. This renders them ineligible for the competition.

I believe these benchmarks were uploaded by Christoph (cc'ed). I can only assume that he did not have more accurate status information.
Certainly the preparations for the floating-point divisions were a bit rushed; it is not without reason that we consider these divisions experimental in 2015.

We intend to make an effort to compute the status of all unknown benchmarks some time after the competition (depending on StarExec availability), so that these benchmarks may become eligible for 2016.

Best,
Tjark