New Release: SMT-LIB Benchmark Metadata as SQLite Database

[Hans-Joerg Schurr]

Hello SMT-LIB Community,

we are happy to announce the release of a new component related to the SMT-LIB
benchmarks: a SQLite database of benchmark metadata.

https://zenodo.org/records/16290040

The database contains metadata extracted from the benchmarks in the current
release, and the performance of SMT solvers on the benchmarks at all SMT
competitions.

The database can be used to select benchmarks with certain properties,
or to find benchmarks that are hard (or easy) to solve.

Since the database is a standard SQLite file, you should be able to query it
using the sqlite3 command line tool or the Python library. The artifact
contains a README that describes the database schema.
We will also present the catalog at this years SMT workshop, and a draft
paper that describes the big picture is available at my webpage[1].

In the future, we plan to release an updated version together with the annual
benchmark release. Please let us know if you have any requests for additional
fields we could include.
Since this is the first release there might also be errors and inconsistencies,
and we would be happy receive bug-reports.

For the SMT-LIB maintainers,
Hans-Jörg Schurr

[1] https://schurr.io/pubs/smt2025.pdf

[BOBOT François]

Hi Hans-Joerg,

On Tue, 2025-08-05 at 05:39 -0500, Hans-Joerg Schurr wrote:

we are happy to announce the release of a new component related to the SMT-LIB

benchmarks: a SQLite database of benchmark metadata.

https://zenodo.org/records/16290040

The database contains metadata extracted from the benchmarks in the current
release, and the performance of SMT solvers on the benchmarks at all SMT
competitions.

Thank you a lot,

It will be very useful. For the competition, just computing the status and the number of check-sat of the benchmarks take a non-trivial download time, disk space and computing time each year.

I'm eager to see soon your presentation, 

Best,

-- 

François