Experimental data for the paper "Scalable Fine-Grained Proofs for Formula Processing"

<p>We provide here the binary, options and experimental data for our CADE paper and the companion report.</p> <p><strong>Setup</strong></p> <p>The tarball containing the source code of veriT used in our experiments is available here. The command line parameters of veriT used in each of the configurations described in the paper are:</p> <ul> <li>Basic: "--old-processing --disable-sym --disable-simp --disable-unit-simp --disable-unit-subst-simp --disable-ackermann --disable-bclause"</li> <li>Extended: "--old-processing --disable-sym --disable-unit-simp --disable-unit-subst-simp --disable-ackermann --disable-bclause"</li> <li>Complete: "--old-processing"</li> <li>with proofs: "--proof=/dev/null --proof-with-sharing"</li> <li>with new code: remove parameter "--old-processing"</li> </ul> <p>The benchmarks are from the SMT-LIB categories QF_ALIA, QF_AUFLIA, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL, QF_UFLIA, QF_UFLRA, AUFLIA, AUFLIRA, UF, UFIDL, UFLIA, and UFLRA.</p> <p>Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. The time limit was set to 30 s.</p>