SMT-COMP 2021 Final Call for Solvers

[Jochen Hoenicke]

===============================================================

    16th International Satisfiability Modulo Theories Competition

                              (SMT-COMP'21)

                         FINAL CALL FOR SOLVERS

===============================================================

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

https://forms.gle/9Eged2txtvJxGXeD9

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 at https://smt-comp.github.io/2021/rules.pdf) 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, see https://github.com/smt-comp/trace-executor#wrapping-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 https://smt-comp.github.io/2021/parallel-and-cloud-tracks.html.

Please see the competition rules for further details.

Sincerely,

The organizing team

Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil

Jochen Hoenicke (chair), Albert-Ludwigs-Universität Freiburg, Germany

Antti Hyvärinen, Università della Svizzera italiana, Switzerland