SMT Bit-Vector Benchmarks
This page provides benchmarks out of quantifier-free bit-vector
(QF_BV) verification problems. These benchmarks can be divided into
- 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
- 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,
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