# Reconstruction of Z3's Bit-Vector Proofs in HOL4
and Isabelle/HOL

**Sascha Böhme, Anthony Fox, Thomas
Sewell and Tjark Weber**

We present accompanying benchmarks and log files discussed in
Section 7 (Experimental Results) of our
paper Reconstruction
of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.

### Unsatisfiable SMT-LIB Bit-Vector Benchmarks

We extracted this set of 4974 unsatisfiable SMT-LIB bit-vector
benchmarks from SMT-Exec on June 13, 2011, using
query `logic~BV & status=unsat`. (SMT-Exec has since been
superseded by Star-Exec.)

### Proof Generation with Z3

We
applied Z3
2.19 to the above SMT-LIB benchmarks, using
option `PROOF_MODE=2` and a timeout of 120 s per
benchmark, to generate unsatisfiability proofs. The following archive
contains the generated proofs, as well as log files, statistical data,
and details of our evaluation hardware.

- smtlib-20110613-proofs-120.tar.gz (4.8 GB)

For space reasons, this file is not currently available for
download. Please contact us if you want to receive a
copy.

### Bit-Blasting in HOL4

We applied
HOL4's bit-blasting decision
procedure `BBLAST` to the above SMT-LIB benchmarks, using a
timeout of 300 s per benchmark. We used
revision 9131
of HOL4, running on top
of Poly/ML 5.4.1.

For every SMT-LIB bit-vector logic, we present an archive that
contains a log file, statistical data, and profiling information.

### Proof Reconstruction in HOL4

We applied our implementation of Z3 proof reconstruction in HOL4 to
the above proofs generated by Z3, using a timeout of 300 s per
benchmark. We again used
revision 9131
of HOL4, running on top
of Poly/ML 5.4.1.

For every SMT-LIB bit-vector logic, we present an archive that
contains a log file, statistical data, and profiling information.

Last modified: 2014-05-06