SMT-COMP 2021

The 16th International Satisfiability Modulo Theories Competition (SMT-COMP 2021) is part of the SMT Workshop 2021, affiliated with CAV 2021. The SMT Workshop will include a block of time to present the competitors and results of the competition.

News

• 18 Jul 2021 Competition results

• 30 Jun 2021 Wrongly Classified Benchmarks

• 18 Jun 2021 SMT-COMP 2021 is Live

• 01 Jun 2021 SMT-COMP Competing Solvers

• 07 May 2021 Final Call for Solvers

• 05 Feb 2021 Preliminary Call for Solvers

• 05 Feb 2021 SMT-COMP Cloud and Parallel Tracks

• 05 Feb 2021 Call for Benchmarks

• 17 Dec 2020 SMT-COMP 2021 pre-announcement

Key dates

• March 15   Deadline for new benchmark contributions
• May 7   Final versions of competition tools
• May 30   Deadline for first versions of solvers (for all tracks)
• June 13   Deadline for final versions of solvers, including system descriptions
• July 18/19   SMT Workshop (presentation of results)

Organizers

• Haniel Barbosa - Universidade Federal de Minas Gerais, Brazil
• Jochen Hoenicke (chair) - Albert-Ludwigs-Universität Freiburg, Germany
• Antti Hyvarinen - Universita della Svizzera italiana, Switzerland

SMT-COMP 2021 is organized under the direction of the SMT Steering Committee.
The competition is run on StarExec, a service that is hosted at the University of Iowa. The parallel and cloud tracks are run on AWS.

Acknowledgment

• Andrew Reynolds (Spotting wrong logic classification)
• Andrea Micheli (pySMT model validator)
• Aaron Stump (StarExec)
• Clark Barrett, Pascal Fontaine, Aina Niemetz, Mathias Preiner, and Hans-Jörg Schurr (smt-lib maintenance)
• Jonathan Eidelman and Mike Whalen (Cloud and Parallel Tracks AWS Support)