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:

  1. 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.
  2. 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).

Related Publications