[SMT-COMP] IMPORTANT: QF_ABV at SMT-COMP'11

[Roberto Sebastiani]

sorry for the very-late (maybe too late) reply.

IMHO, I'd (have?) rerun. 
I don't think that sentences like "boolector would have won anyway"
or "Z3 people are ok with the results" make sense.

There is a competition with some specifications and regulations, and there 
has been a clear flaw in the process, which may have seriously altered the outcome of the 
results. 
THe competitions are not only for the competitors, but also for the (possibly many)
people who want to see the actual status of the art, observe the progressof state-of-the-art,
and so on.

Thus, if it is practically possible, I suggest to rerun.

Roberto

--------------------------------------------------------------------------
Prof. ROBERTO SEBASTIANI, PhD
Dept of Information Engineering and Computer Science   Ph: +39 0461 281514
University of Trento                                  Fax: +39 0461 283964
Via Sommarive 14, Povo, I-38123, Trento, Italy  Skype: roberto.sebastiani1
roberto.sebastiani at disi.unitn.it          url: http://disi.unitn.it/~rseba
OKKAM id:  http://www.okkam.org/ens/id4e14c363-3008-4752-b243-480c87eb2b4c
--------------------------------------------------------------------------

On Sun, 17 Jul 2011, Alberto Griggio wrote:

> Hello Leo,
>
>> Hi Alberto,
>>
>> I believe the winner will not change. Boolector is clearly the best
> solver
>> for QF_ABV. I talked with Christoph and we are ok with the current
>> results.
>
> Well, this makes things much simpler then. FWIW, I also think Boolector
> is so ahead of the others in QF_ABV that its victory is out of
> question. So, if nobody disagrees, we can stick with the current result,
> and apologies once more for the confusion. Running the competition
> "live" is very exciting, but also highly subject to Murphy's law...
>
> Alberto
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>