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

[Leonardo de Moura]

Hi Roberto,

> I don't think that sentences like "boolector would have won anyway"
> or "Z3 people are ok with the results" make sense.

Why does it not make sense that we are ok with the results?
BTW, we are not the organizers; we did not create the problem; we were affected by it; we acknowledge that Boolector is the best solver; and we are saying we are ok with that and we don't care if the division will be re-executed or not. This is our position, and I think it is really harsh to say it doesn't make sense.

Cheers,
Leo


-----Original Message-----
From: Roberto Sebastiani [mailto:rseba at disi.unitn.it] 
Sent: Monday, July 18, 2011 10:36 AM
To: Alberto Griggio
Cc: Leonardo de Moura; florian at informatik.uni-bremen.de; smt-comp at cs.nyu.edu; jp at informatik.uni-bremen.de; Christoph Wintersteiger; elenav at informatik.uni-bremen.de
Subject: Re: [SMT-COMP] IMPORTANT: QF_ABV at SMT-COMP'11

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
>