Extending SMT solvers to Higher-Order Logic

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett

We provide here the experimental data used in our paper.


The tarballs containing the binaries of the solvers used in our experiments: CVC4, veriT, Ehoh, Leo-III, Satallax

To enable individual configurations of CVC4:

To enable individual configurations of veriT: To enable individual configurations of Ehoh:


The TPTP THF benchmarks can be downloaded from the official TPTP website. We list below the benchmarks that correspond to the subsets we used in our evaluation: The remaining benchmarks are given in the tarballs below: The HOMST equivalent of the above benchmarks in which veriT was evaluated are available here:


According to the naming conventions of the benchmark sets as per the tarballs and problem lists above and with the solver configurations being identified in the CSVs according to the mapping:

Name on paper Name on CSVs
@cvc cvc4-hoelim
@cvc-sax cvc4-hoelim-storeax-agg
@cvc-ui cvc4-hoelim-fsi
@cvc-ui-sax cvc4-hoelim-fsi-storeax-agg
@cvc-fmf-sax cvc4-hoelim-fmf-storeax-agg
cvc cvc4-nhom
cvc-sax cvc4-nhom-storeax-agg
cvc-ui cvc4-nhom-fsi
cvc-ui-sax cvc4-nhom-fsi-storeax-agg
cvc-fmf cvc4-fmf
@vt verit-cib-hoelim
vt verit-cib
the CSV files with the results are available below: