@InProceedings{10.1007/978-3-032-22752-2_8,
author="Schurr, Hans-J{\"o}rg
and Bobot, Fran{\c{c}}ois
and Preiner, Mathias
and Niemetz, Aina
and Barrett, Clark
and Fontaine, Pascal
and Tinelli, Cesare",
editor="Junges, Sebastian
and Katz, Guy",
title="Exploring the SMT-LIB Benchmark Library",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2026",
publisher="Springer Nature Switzerland",
address="Cham",
pages="150--169",
abstract="The SMT-LIB benchmark collection is a large set of problems for SMT solvers. It has been continuously maintained and expanded since its creation in the early 2000s by the SMT-LIB initiative. It has been used since 2005 by the annual SMT solver competition to compare the performance of SMT solvers, and by researchers to study novel solving techniques. Effective use of the collection often requires access to benchmark metadata (e.g., date, source, satisfiability status, theory symbol count, and so on). Furthermore, this metadata and the past competition results contain a wealth of historical information about the development of SMT solving. In this paper, we report on our efforts to collect and curate all metadata from the SMT-LIB benchmarks together with the results of all past SMT-COMP competitions in a single SQLite database. We also present tools to explore this database and extract relevant insights. Since APIs for SQLite databases are available for all major programming languages, the database makes it easy to add features using SMT benchmark metadata to SMT development tools. To illustrate the structure of the collected data we perform multiple case studies. In particular, we present a comparison of SMT solvers that is independent of the changing hardware and benchmarks used by the competition. The database is released annually on Zenodo, and serves as an archive of the state of SMT-LIB and, by extension, of the state of the art in SMT.",
isbn="978-3-032-22752-2"
}