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

[Alberto Griggio]

Hi Tjark,

> 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.

I see, thanks for the clarification! My understanding was that for
floating-points the competition was more like a "demo" than a real
competition, so I thought it might make sense to run on all the
benchmarks, just to have something more to demo... However, your
explanation also makes sense :-)

Best,
Alberto