SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2023

Rules
Benchmarks
Specs
Model Validation Track
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

SMT-COMP 2023 is Live

05 Jun 2023

The SMT-COMP 2023 is live. You can follow it on StarExec:

https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=543471

So far we have only started the single query track. The benchmark selected for the other tracks will depend on the results of this track. We will add the jobs for the other tracks to the same space.

Note that the job summary is not always accurate: Benchmarks with unknown status are classified as unknown, even if the solver replied with sat or unsat. In the model validation track an error message in the output is classified as wrong, even though our script classifies it as unknown. We will use a script running on the Job Information downloaded from the StarExec site and, especially in cases of unsoundness, confirm manually whether the classification is correct or not.