SMT Bit-Vector Benchmarks

This page provides benchmarks out of quantifier-free bit-vector (QF_BV) verification problems. These benchmarks can be divided into two classes:

Benchmarks about verifying the soundness of translating certain bit-vector operations (e.g. addition, multiplication, shifts etc.) to a small set of operations which we consider as base operations. Base operations are: bitwise operations, equality, and slicing.
Benchmarks contained by the PSPACE-complete fragment of QF_BV, by using only the following restricted set of operations: bitwise operations, equality, shift by one, addition, subtraction, unary minus, relational operations, and indexing.

Generator scripts. See also the README file that is part of the package.
SMT2 files generated by executing make generate.
AIG files (67 MB) generated by bit-blasting the SMT2 instances, except for the ones that belong to the benchmark families bvneg, binmagic_by_bw_shl1, bvlshr_const_by_bvmul, bvshl_const_by_bvmul, power2bit, and power2eq, since those produce huge AIGs and seem not really challenging. Bit-blasting was done by Boolector.
CNF files (516 MB) generated from the AIG instances (by using aigtocnf that is part of the AIGER distribution).

A. Fröhlich, G. Kovásznai, A. Biere. Efficiently Solving Bit-Vector Problems Using Model Checkers.
A. Fröhlich, G. Kovásznai, A. Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. In Proc. 15th Intl. Computer Science Symposium in Russia (CSR'13), Ekaterinburg, Russia, 2013 (to appear).