The International Satisfiability Modulo Theories (SMT) Competition.
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:
This is a call for three things:
The organizing team has prepared the schedule and prelimiary 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 the 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 _.
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:
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.
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.
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.
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-announce@googlegroups.com .
Announcements will be sent to smt-announce@googlegroups.com .
Sincerely,
The organizing team