This is the empirical evaluation of the paper ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses.

Moreover, we refer to the general LoAT website for further information.

Getting LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Moreover, you can find the source code of LoAT at GitHub.

Evaluation

Examples

Here you can find a zip file containing all examples that we used for our evaluation. It contains the 427 examples from the category LIA-Lin of the benchmark collection from the CHC-Comp '22 that do not use the operators div or mod. Here you can find a zip file containing those examples that also do not use Boolean variables.

Results

Below we provide tables with the detailed results of our benchmarks:

• Examples with integers and Booleans
• LoAT
• invocation: loat-static --mode reachability --format horn $INPUT
• Spacer
• invocation: z3 fp.engine=spacer $INPUT
• Z3 BMC
• invocation: z3 fp.engine=bmc $INPUT
• Golem TPA
• invocation: golem -l QF_LIA -e tpa $INPUT
• Eldarica
• invocation: eld $INPUT
• Eldarica with acceleration as pre-processing
• invocation: eld -stac $INPUT
• Examples with integers only
• LoAT
• Spacer
• Z3 BMC
• Golem TPA
• Eldarica
• Eldarica with acceleration as pre-processing