We provide the following supplementary material for our paper.
The .tgz containing the binary of CVC4 used in our experiments can be downloaded here: cvc4.zip.
The latest version of CVC4 can be downloaded here: CVC4.
Note: The new instantiation techniques work when the logic is set to LIA or LRA using the SMT version 2 command (set-logic LRA) or (set-logic LIA),
or can be enabled by the command line option --cbqi.
The techniques from Section 6 are enabled by the command line option --cbqi-nested-qe.
To enable individual configurations of CVC4:
We considered all benchmarks in the LIA and LRA logics of SMTLIB, which include benchmarks from the TPTP library. We also considered a set of 71 benchmarks corresponding to the first-order formulation of single-invocation synthesis conjectures taken from the 2015 Sygus competition. The benchmarks are avaiable in both *.smt2 and *.p formats below.
Our evaluation used the StarExec cluster for evaluation https://www.starexec.org. The jobs we ran in our evaluation are publicly available, and can be viewed by logging into StarExec as a guest (click "Guest" at the bottom of the log in page). The links to the individual jobs are: