Revisiting Enumerative Instantiation - Artifact

This artifact contains the binaries of the SMT solvers CVC4 and Z3, the benchmarks on which they were evaluated, and the running scripts for each configuration evaluated. An overview of the results obtained from this evaluation in the StarExec cluster is presented in Section 5 of the TACAS 2018 proceedings paper:<br><i>Revisiting Enumerative Instantiation</i>Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). Thessaloniki, Grécia.<br>The related paper presents a strengthened version of the Herbrand theorem, designed as an better-suited basis for the instantiation loop used in SMT solvers. The experimental evaluation code employs different strategies of effectively combining enumerative instantiation with other instantiation techniques.<br>The subdirectory <b>benchmarks </b>contains a bash shell script (.sh) to be used in conjunction with the TPTP benchmarks accessible via http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v7.0.0.tgz see <b>readme.txt</b> for more detailed instructions on how to use the artifact.<br>The subdirectory <b>solvers </b>contains archived CVC4 and Z3 solvers; corresponding to the experimental evaluation of different enumerative instantiation strategies. All results were produced on <b>StarExec</b>, a public execution service for running comparative evaluations of solvers, with a timeout of 300 seconds.<br>All files are in openly-accessible text format holding bash shell scripts or documentation such as READMEs.