The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
07 May 2021
We now invite registration of solvers for SMT-COMP 2021.
Solvers must be uploaded to StarExec, and entered into the competition via the web form at
The submission deadline for (first versions of) solvers is
May 30, 2021.
After the above date, no new entrants will be accepted. However, submitted solvers may be updated until
June 13, 2021.
We plan to publish the results including all materials under the CC-BY-ND license. We therefore ask you to give us permission to include your solver under this license. Otherwise, it is not possible to include your solver in the final artifact.
Note that a short system description of 1-2 pages (see Section 4 of the competition rules) is part of the solver submission and MANDATORY. Submission of the system description is due until the final solver deadline on June 13, 2021. Participants are however asked to provide a link to the system description in the registration form to facilitate the registration, even if the actual description would not yet be available at the time of the registration. The StarExec links to the final solver submission must be provided via email to the organisers by the final deadline.
The pre- and post-processors we plan to use in the SMT-COMP 2021 were uploaded to StarExec. Note that for testing your solver in the incremental track you need to wrap the trace executor around your solver. Nonetheless, you should provide us with the link to the original unwrapped solver; we will wrap your solver during the competition.
This year we will organise also a separate, experimental track for parallel and cloud solvers. For more information on the participation on these two tracks, see Parallel & Cloud Tracks.
Please see the competition rules for further details.
Sincerely,
The organizing team