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

[Tjark Weber]

On Tue, 2026-05-05 at 19:29 +0200, Hans-Joerg Schurr wrote:

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.

One of the SMT community's key strengths is the availability of a large benchmark suite (SMT-LIB) that reflects real application needs. These benchmarks sustain a virtuous cycle: they drive solver development, which in turn enables new applications, leading to additional benchmarks. Restricting or disallowing certain commands risks disrupting this cycle, so it is advisable to be permissive about what is admitted into SMT-LIB.

What is included in the SMT Competition, however, is a separate matter and is more strongly constrained by current solver capabilities. In that context, it may be reasonable to remove certain commands or to introduce dedicated tracks.

Best,

Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy