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

[Clark Barrett]

I agree with Tjark.  We should not sweep errors under the rug - this sends
the wrong message.  As a community, we should incentivize making tools that
are correct.  The scoring reflects this and so does the fact that errors
will be revealed.  Ultimately, I hope we will move even further in this
direction,  For example, we could follow the SAT community in requiring
proofs.

-Clark


On Fri, Jul 14, 2023 at 2:09 PM Tjark Weber <tjark.weber at it.uu.se> wrote:

> 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
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp
>