CHC-COMP 2023: Competition Report
Emanuele De Angelis, Hari Govind V K
TL;DR
CHC-COMP 2023 benchmarks and solver evaluations advance the state of constrained Horn clause solving by systematically organizing six tracks around linear and nonlinear CHCs with linear integer arithmetic, arrays, and algebraic data types. The report documents the competition design, benchmark processing, and result-driven evaluation, including a new ADT-LIA-nonlin track and extended CHC formatting to support ADTs. Key outcomes include top performance by Eldarica and Golem across multiple tracks, with Spacer achieving strong results as hors concours, and practical issues (e.g., solver inconsistencies and build delays) addressed through fixes and post-hoc analysis. The work provides actionable guidance for future CHC-COMP editions, including witness formats, status declarations, and parallel track considerations, while offering comprehensive data in StarExec for reproducibility and further study.
Abstract
CHC-COMP 2023 is the sixth edition of the Competition of Solvers for Constrained Horn Clauses. The competition was run in April 2023 and the results were presented at the 10th Workshop on Horn Clauses for Verification and Synthesis held in Paris, France, on April 23, 2023. This edition featured seven solvers (six competing and one hors concours) and six tracks, each of which dealing with a class of clauses. This report describes the organization of CHC-COMP 2023 and presents its results.