Revisiting Enumerative Instantiation

Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine

We provide here the experimental data used in our paper. A version of the paper with corrected typos is available here.

Solvers

The .zip containing the binary of CVC4 used in our experiments can be downloaded here: cvc4. The latest version of CVC4 can be downloaded here: CVC4. The .tgz containing the binary of Z3 used in our experiments can be downloaded here: z3.

To enable individual configurations of CVC4:

To enable individual configurations of Z3:

Benchmarks

Results

Our evaluation used the StarExec cluster for evaluation https://www.starexec.org. The experiments on SMT-LIB can be found here and on TPTP here. We provide a spreadsheet containing detailed results of the experiments.