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

BOBOT Francois Francois.BOBOT at cea.fr
Thu Jul 13 09:51:09 EDT 2023


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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: slides.pdf
Type: application/pdf
Size: 1580288 bytes
Desc: slides.pdf
URL: </pipermail/smt-comp/attachments/20230713/1e19b985/attachment-0001.pdf>


More information about the SMT-COMP mailing list