A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds and Jasmin Christian Blanchette

We provide the following supplementary material for our paper. The longer version of our paper can be found here: report.

Solvers

Benchmarks

The benchmarks can be found here. They are divided into four subsections (both, coda, data, and nada), to indicate which theories (codatatypes and/or datatypes) are included in the encoding.

Results

The spreadsheet summarizing the results for the benchmarks considered in this paper can be accessed here: results-cade2015-cdt.xls.

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 accessed by logging into StarExec as a guest (click "Guest" at the bottom of the log in page). The links to the individual jobs are: