[SMT-COMP] [EXTERNAL] Proposal for handling errors differently in SMTCOMP results

[Stéphane Graham-Lengrand]

On 7/13/23 06:51, BOBOT Francois wrote:
> Dear SMT-COMP enthusiast,
> 
>     The results of the SMT-COMP have been announced last week. I hope people had fun participating in the competition.
> 
>   During the preparation of the presentation (the pdf is attached), I filled the list of solvers with errors, as presented each previous years. But this list is not fun at all, often errors come from little mistakes. Moreover if one would have the time to test more thoroughly its solver in all the track and logic it could have caught the problem, it could have fixed the bug or it could have not participated in this track-logic. An error disqualify a solver for the track-logic, which often disqualify for the division. I think it is enough of a sanction.
> 
> That's why I propose for next year:
>    - to not pinpoint solver with errors
>    - to remove the solvers from the results page of the track-logic as if the solver chooses not to participate
>    - to remove from the solver summary the track-logic where it has some errors.
> 
> What do you think?

I agree, but have no strong opinion.
The solver authors should still be made aware of what happened, but I 
imagine you already communicate with the authors when errors are found?

To go in your direction, perhaps the fixed solvers could be renamed 
something else than XXX-fixed (which is a strong indication that the 
original solver produced errors - in a broad sense). Like 
XXX-post-deadline, which could cover more than fixes for errors.

Stéphane

> 
> Best,
> 
> --
> François
> 
> 
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp