[SMT-COMP'25] Call for Comments, Call for Benchmarks, Preliminary Call for Solvers

[Martin Jonáš]

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

   20th International Satisfiability Modulo Theories Competition
                           (SMT-COMP'25)

                         August 10-11, 2025
                            Glasgow, UK

                         CALL FOR COMMENTS
                        CALL FOR BENCHMARKS
                    PRELIMINARY CALL FOR SOLVERS

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


We are pleased to announce the 2025 edition of SMT-COMP.

SMT-COMP is the annual competition among Satisfiability Modulo
Theories (SMT) solvers.

The goals of SMT-COMP'25 are to encourage scientific advances in the
power and scope of solvers, to stimulate the community to explore and
discuss shared challenges, to promote tools and their usage, to engage
and include new members of the community (in a fun environment), and to
support the SMT-LIB project in its efforts to promote and develop the
SMT-LIB format and collect and collate relevant benchmarks.

The results of SMT-COMP'25 will be announced at the SMT Workshop
(August 10–11, 2025), which is affiliated with SAT 2025.

SMT-COMP'25 is organized under the direction of the SMT Steering
committee. The organizing team for SMT-COMP'25 is:

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

This is a call for three things:


CALL FOR COMMENTS:

The organizing team has prepared the schedule and preliminary rules for 2025.
To further the above goals, we propose to make several changes to the
format of SMT-COMP'25. The changes concern derived tools,
unsat core track scoring, best overall ranking, and cloud and
parallel tracks. All the changes are summarized in Introduction
section of the proposal of the rules:
https://smt-comp.github.io/2025/rules.pdf

Any comments you may have on these proposed changes, on how to improve
the competition, or to redirect its focus are welcome and will be
considered by the team. We particularly appreciate comments received
before * March 9th, 2025 *.


CALL FOR BENCHMARKS:

Have interesting or hard benchmarks that can be made public? Want the
world's best SMT solvers to compete to solve *your* problems? Submit
your benchmarks to SMT-LIB and SMT-COMP!

Please let us know as soon as possible if you are considering
submitting benchmarks, even if the material is not quite ready. We
will work in close cooperation with the SMT-LIB maintainers to
integrate such benchmarks into SMT-LIB. The deadline for submission of
new benchmarks to be used in the 2025 competition is April 12.

We would also like to extend our call for benchmarks to include
benchmarks with some additional information:

1. For the Industrial Challenge Track we would like to receive
   difficult benchmarks that are important to you and either unsolved,
   or unsolved within some reasonable time limit. We would
   particularly like benchmarks that come with a description of why
   they are difficult/important. Of course, if this is not possible
   then new challenging benchmarks are always appreciated.

2. We would appreciate receiving benchmarks that you want solved
   quickly (e.g.  in under 24 seconds) but currently struggle to.
   Please add the required solution time as a comment to the
   benchmark. If we receive many benchmarks of this kind we may
   consider a new track in the future that specifically focuses on
   benchmarks requiring short time limits.


PRELIMINARY CALL FOR SOLVERS:

The submission deadline for solvers is June 13th, 2025.  However, it is
useful to 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, we ask that
you let us know at your earliest convenience if you think you may be
submitting one or more solvers to SMT-COMP'25.


COMMUNICATION:

The competition website is at
https://smt-comp.github.io/2025/

The SMT-COMP repository is at
https://github.com/smt-comp.github.io.

Public email regarding the competition may be sent to
smt-an...@googlegroups.com .

Announcements will be sent to smt-an...@googlegroups.com .


Sincerely,

The organizing team