SMT-COMP 2024: Preliminary Call for Solvers

[Martin Bromberger]

Hello everybody,

The submission deadline for the first version of the solvers is on May 27. However, it is useful for the organizing team to know in advance which and how many solvers may be entering. If you have not submitted a solver before, or if you think there may be unusual circumstances, please let us know at your earliest convenience if you think you may be submitting a solver to SMT-COMP'24. We require a system description for all submitted solvers as part of the submission of the preliminary solver versions (deadline May 27).

The single query, incremental, unsat-core, model-validation and proof exhibition tracks will no longer run on StarExec (http://www.starexec.org) because StarExec is in the process of being decommissioned. Starting this year, we will run these tracks on the BenchExec cluster (https://github.com/sosy-lab/benchexec) owned by LMU's Software and Computational Systems Lab (SoSy-Lab https://www.sosy-lab.org/), who are kind enough to support our competition with their computing power.

Participants are now required to upload their final solver versions as a Zenodo (https://zenodo.org/) submission that must contain a docker file that compiles the solver. Moreover, we will change our submission process from a google form to a push request to the SMT-COMP GitHub repository (https://github.com/SMT-COMP/smt-comp.github.io/tree/master/submissions). Detailed instructions can be found in the README file there.

The parallel and cloud tracks will again run on AWS, which is kindly supporting them. Participants of these tracks are required to submit their solver via a GitHub repository (which can be private). The repository should contain a docker file that compiles the solver. Detailed instructions for submitting to these tracks are available here (they lift to SMT):

https://github.com/aws-samples/aws-batch-comp-infrastructure-sample

To participate teams must email aws-smtc...@googlegroups.com with the following:

1. name of the solver and a list of the authors

2. your AWS account number

3. the URL of the GitHub repository including the branch

4. the full, 40-character SHA-1 hash of the commit

There are also some potential changes that we are considering for future editions of the competition (so for SMT-COMP 2025 and onwards). These changes would make our lives much easier (= reduce complexity of our scripts and the manual preprocessing from our side), but might cause issues for you. Therefore, we would like to know if any of the following potential changes would cause serious issues for you and why:

1. The preliminary versions of the solvers (and not just the final versions) must be available on zenodo

2. Each team may only submit one archive or, to be more precise, different archives by the same team will be treated as separate submissions/solvers

3. Scripts for command-line options are no longer allowed, i.e., the solvers should be able to analyze the problems and adjust their settings internally with just the name of the track.

4. Each submission may only have one string of command-line options and not separate strings of options for the different divisions/tracks they participate in

The last three changes would have the additional benefit that for users of our tools it becomes much more transparent how to reproduce the competition results without the knowledge where to find the competition scripts/options or that such scripts/options exist at all.

Best,

The organizing team

Martin Bromberger (chair), MPI for Informatics, Germany

François Bobot, CEA List, France

Martin Jonáš, Masaryk University, Czech Republic