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

[Tjark Weber]

François,

It goes without saying that SMT solvers are complex software tools, and
errors are to be expected. The aim in documenting these errors is not
to point fingers, of course; and the competition rules need to
carefully balance incentives for new features and continued solver
development against disincentives for incorrect answers.

With that being said, I think that having a record of errors in
competition versions of solvers is highly useful: first, for solver
developers (who can then fix these errors); second, for users (who can
develop a more informed understanding of solver capabilities and
limitations); third, for the overall state of solver development. If
these errors are not published in easily accessible form, it will
become much harder to reason about the reliability (or possibly lack
thereof) of SMT solvers.

Best,
Tjark


On Thu, 2023-07-13 at 13:51 +0000, 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?
>
> Best,
>
> --
> François
>
>
> VARNING: Klicka inte på länkar och öppna inte bilagor om du inte
> känner igen avsändaren och vet att innehållet är säkert.
> CAUTION: Do not click on links or open attachments unless you
> recognise the sender and know the content is safe.
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy