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.
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.)
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.
For space reasons, this file is not currently available for download. Please contact us if you want to receive a copy.
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.
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.
