Solving Quantified Linear Arithmetic by Counterexample-Guided Instantiation (FMSD 2016 submission)

Andrew Reynolds, Tim King, and Viktor Kuncak.

We provide the following supplementary material for our paper.

Solver

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:

Benchmarks

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.

Results

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:

These jobs contain further configurations not mentioned in the paper. We for instance considered the best version of Vampire (the one from SMT COMP 2016), and only one version of Beagle. Note that the information under solver summary is not accurate, since the postprocessor used by StarExec only counts benchmarks with known statuses as being solved. For more accurate and detailed information, a spreadsheet summarizing the results for the benchmarks considered in this paper can be downloaded here: results-qla.xlsx.