Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description
Gergely Kovásznai, Andreas Fröhlich, Armin Biere · 2013
Abstract—This document describes several sets of benchmarks corresponding to quantifier-free bit-vector formulas. A generation script first creates all benchmarks in SMT2 format and then uses Boolector to generate CNF instances in DIMACS format by bit-blasting. I.