[SMT-COMP'25] Final Call for Solvers

[Martin Jonáš]

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

 20th International Satisfiability Modulo Theories Competition

                         (SMT-COMP'25)


               FINAL CALL FOR SOLVERS

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


We invite registration of solvers for SMT-COMP 2025.


Solvers are entered into the competition via a pull request to the SMT-COMP
GitHub repository at:

https://github.com/SMT-COMP/smt-comp.github.io/tree/master/submissions

Detailed instructions can be found on the competition website
(https://smt-comp.github.io/2025/solver_submission/) . Note that solver binaries
must be uploaded to a publicly available space and the final version must be a
Zenodo (https://zenodo.org/) submission for reproducibility. Please include a
license file of your choice with your solver binaries.

The submission deadline for (first versions of) solvers is

    ***June 13, 2025***

After the above date, no new entrants will be accepted. However,
submitted solvers may be updated via the pull request until

    ***June 27, 2025***

Note that a short system description of 1-2 pages (see Section 4 of the
competition rules at https://smt-comp.github.io/2025/rules.pdf) is part of the
solver submission and is MANDATORY. The system descriptions can be submitted
until the initial solver deadline on June 13, 2025. Participants are
asked to provide a link to the system description in the submission. The system
description can be updated until June 27, 2025, but it must be
reviewable since the initial solver deadline. The links to the final solver
submission must be provided via the pull request to the organizers by the final
deadline.

As in the previous year, we will run single query, incremental, unsat-core, and
model-validation 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. To be more
precise, the competition will be run on the 168 apollon nodes of the SoSy-Lab
BenchExec cluster (for more details see
https://vcloud.sosy-lab.org/cpachecker/webclient/master/info). It is also
possible to locally emulate and test the computing environment on the
competition machines using the following instructions:
https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines

You are encouraged to run the solvers in the above-mentioned environment for
testing. The submission process contains a continuous integration check that
tests the submitted binaries on a trivial set of input benchmarks for every pull
request. We will also run the first versions of all solvers on a small subset of
benchmarks using shorter timeout and send you the results. However, these checks
do not substitute thorough testing of the submitted solvers.

Your solver can have multiple configurations for different tracks, logics, etc.
These can be specified as part of the solver submission and changed until the
deadline for the final solver. The default configuration is used for all other
tracks.

Due to the lack of suitable infrastructure, Cloud track is not taking place for
SMT-COMP 2025. Parallel track is going to be executed on the same
BenchExec-based infrastructure as the other tracks, only on machines with a
higher number of CPU cores. As a result, there is no special submission process
for the parallel track and the submissions should follow the same process as the
rest of the competition.

Please see the competition rules for further details. Do not hesitate contacting us 

if you have any questions or comments.

Sincerely,

The organizing team
Martin Jonáš (chair) - Masaryk University, Czechia
François Bobot - CEA List, France
David Déharbe - CLEARSY, France
Dominik Winterer - ETH Zurich, Switzerland