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

[Clark Barrett]

I also agree with this.  I think that if the SMT-LIB benchmarks are still
labeled with "QF_AUFBV" then the competition benchmarks should be labeled
the same way (however, the SMT-LIB benchmarks should be updated to read
"QF_ABV" after this competition).

-Clark


On Mon, Jul 18, 2011 at 1:35 PM, Roberto Sebastiani <rseba at disi.unitn.it>wrote:

> 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 <roberto.sebastiani at disi.unitn.it>
>      url: http://disi.unitn.it/~rseba
> OKKAM id:  http://www.okkam.org/ens/**id4e14c363-3008-4752-b243-**
> 480c87eb2b4c<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<http://cs.nyu.edu/mailman/listinfo/smt-comp>
>>
>>  ______________________________**_________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/**listinfo/smt-comp<http://cs.nyu.edu/mailman/listinfo/smt-comp>
>