SMT-LIB release 2025 (incremental benchmarks)

Mathias Preiner; Hans-Jörg Schurr; Clark Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli

doi:10.5281/zenodo.15493095

Back

SMT-LIB release 2025 (incremental benchmarks)

Dataset

Open access

SMT-LIB release 2025 (incremental benchmarks)

Mathias Preiner, Hans-Jörg Schurr, Clark Barrett, Pascal Fontaine, Aina Niemetz and Cesare Tinelli

Zenodo

05/22/2025

DOI: 10.5281/zenodo.15493095

Files and links (1)

url

https://doi.org/10.5281/zenodo.15493095View

Open Access

Abstract

This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at https://smt-lib.org. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file. This collection contains the incremental benchmarks. Benchmarks are grouped by logic and compressed with the zstd compression algorithm using the tar --zstd. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.

Details

Title: Subtitle: SMT-LIB release 2025 (incremental benchmarks)
Creators: Mathias Preiner - Stanford University
Hans-Jörg Schurr - University of Iowa
Clark Barrett - Stanford University
Pascal Fontaine - University of Liège
Aina Niemetz - Stanford University
Cesare Tinelli - University of Iowa
Resource Type: Dataset
DOI: 10.5281/zenodo.15493095
Publisher: Zenodo
Language: English
Date published: 05/22/2025
Academic Unit: Computer Science
Record Identifier: 9984825526202771

Metrics

113 Record Views