The International Satisfiability Modulo Theories (SMT) Competition.


Benchmark Submission
Previous Editions


Parallel & Cloud Tracks

Final Call for Solvers

07 May 2021

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

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.


The organizing team