Call for Benchmarks 2026

[Hans-Joerg Schurr]

Hello SMT community!

# Call for Benchmarks

As every year, we are again collecting benchmarks for the SMT-LIB benchmark
collection.  A rich collection of relevant benchmarks is essential to move
SMT research forward, and to evaluate SMT solvers at the yearly SMT competition.

Together with the SMT-COMP organizers, we decided to decouple the benchmark
submission deadline from the competition deadline. The rationale was that
SMT-COMP participants do not have sufficient time to improve on new benchmarks
between the submission and competition deadline (usually about one month).
Decoupling of those two deadlines (1) makes it easier for the SMT-LIB
maintainers to organize the submission and editing process, and (2) ensures
that new benchmarks are available well in advance for competition participants.

From now on, we aim for a new SMT-LIB release close to the SMT workshop.
In the future we will also publish a separate call for benchmarks, but in
general, submission of new benchmarks is always appreciated throughout the year!

For the 2026 SMT-LIB release the deadline for benchmark submission is
** June 25 **

Like in previous years, benchmarks can be submitted by opening a pull request
to this Github repository: https://github.com/SMT-LIB/benchmark-submission
See the README file for instructions on how to structure your benchmarks.

If there are any difficulties with preparing the benchmarks, do not hesitate
to reach out to us.

# Request for Comments

Currently, we only collect benchmarks that use the subset of SMT-LIB features
that is used by the SMT competition.  However, we occasionally get submissions
that make use of a larger set of SMT-LIB commands.
A common example are benchmarks that activate model generation and request a
model using `(get-model)`.  This often impacts solver performance.

Until now such commands were removed from the original benchmarks during the
submission process. However, by removing these commands the benchmarks may not
reflect the actual use case of the user's application anymore.

It could be argued that such commands could easily be removed by the
competition or by users that are not interested in them.  However, this
is not always the case.  For example, the standard, but uncommon, option
`(set-option :global-declarations true)` changes the semantics of `push`
and `pop`.

We would like to hear the perspective of the community regarding expanding
the set of allowed commands.  Whether this would be useful, and if so
whether we should design an expanded subset of commands, or even accept
all valid SMT-LIB files.

Best,
 Hans-Jörg Schurr
and the SMT-LIB maintainers

    Mathias Preiner pre...@cs.stanford.edu
    Clark Barrett bar...@cs.stanford.edu
    Pascal Fontaine pascal....@uliege.be
    Aina Niemetz nie...@cs.stanford.edu
    Cesare Tinelli cesare-...@uiowa.edu