We provide the following supplementary material for this paper.

The zip archive containing the binary of CVC4 used in our experiments can be found here: cvc4-sygus.zip

• Configuration cvc4+sg from the paper is enabled by command line parameters “–cegqi –dump-synth”.
• Configuration cvc4+si-r is enabled by “–cegqi-si –dump-synth –no-cegqi-si-reconstruct”
• Configuration cvc4+si is enabled by “–cegqi-si –dump-synth”

The spreadsheet summarizing the results for the benchmarks considered in this paper can be accessed here: results-cav2015-synth.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:

For ESolver:

https://www.starexec.org/starexec/secure/details/job.jsp?id=6440.

For all three configurations of CVC4:

https://www.starexec.org/starexec/secure/details/job.jsp?id=6561

We provide the following supplementary material for this paper.

The zip archive containing the binary of CVC4 used in our experiments can be found here: cvc4-sygus.zip

• Configuration cvc4+sg from the paper is enabled by command line parameters “–cegqi –dump-synth”.
• Configuration cvc4+si-r is enabled by “–cegqi-si –dump-synth –no-cegqi-si-reconstruct”
• Configuration cvc4+si is enabled by “–cegqi-si –dump-synth”

The spreadsheet summarizing the results for the benchmarks considered in this paper can be accessed here. For benchmarks with syntactic restrictions (Fig 9 and Fig 11): results-general-fmsd.xls. For the max family of benchmarks (Fig 10): results-max-fmsd.xls. For benchmarks without syntactic restrictions (Fig 12): results-clia-fmsd.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 below, which include additional configurations not mention in this paper.

For all solvers, except the latest version of CVC4, on benchmarks with syntactic restrictions:

https://www.starexec.org/starexec/secure/details/job.jsp?id=10526

For all configurations of CVC4 on benchmarks with syntactic restrictions:

https://www.starexec.org/starexec/secure/details/job.jsp?id=10575

For all solvers on the max family of benchmarks:

https://www.starexec.org/starexec/secure/details/job.jsp?id=11076

For all solvers, except the latest version of CVC4, on benchmarks without syntactic restrictions:

https://www.starexec.org/starexec/secure/details/job.jsp?id=10556

For CVC4 on benchmarks without syntactic restrictions:

https://www.starexec.org/starexec/secure/details/job.jsp?id=10597