Constrained Horn Clauses (CHC) is a fragment of First Order Logic (FOL) that is sufficiently expressive to describe many verification, inference, and synthesis problems including inductive invariant inference, model checking of safety properties, inference of procedure summaries, regression verification, and sequential equivalence. The CHC competition (CHC-COMP) will compare state-of-the-art tools for CHC solving with respect to performance and effectiveness on a set of publicly available benchmarks. The winners among participating solvers are recognized by measuring the number of correctly solved benchmarks as well as the runtime. CHC-COMP 2025 was associated with the Workshop on Horn-Clause Verification and Synthesis (HCVS 2025).

Competition Results from 2025

• Extended report as presented at HCVS 2025 (adds details and model validation)
• Report as presented at SPIN 2025 (with a minor update in LIA-Lin-Arrays)
• The full list of benchmarks is available here: chc-comp25-benchmarks
• Scripts for running the competition are here: chc-comp25-scripts

Notes on result tables and plots:

• Plots are "quantile plots", aggregating points over results sorted by the CPU time it took to produce them (lower is faster, overall score corresponds to the rightmost value)
• Click on category names for aggregate table including all tools
• Click on the tool names to see table of individual results
• Click on plots to enlarge them
• The linked tables were generated by benchexec

Disclaimer: Results that are inconsistent across tools are currently omitted. This means that some tools miss out on some correct points and some are not punished for giving wrong results, but it is not always clear what is the ground truth, which we will fix in the future.

Participants (Tool, Submitter)

• CHC2C 1.0 (Mihály Dobos-Kovács, Levente Bajczi, András Vörös), Note: meta-solver
• ChocoCatalia (Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato)
• Eldarica 2.2 (Hossein Hojjat, Philipp Ruemmer)
• Golem 0.7.1 (Martin Blicha)
• LoAT (Florian Frohn, Jürgen Giesl)
• MuCyc (Kazuki Uehara, Hiroshi Unno)
• PCSat (Takuma Monma, Hiroshi Unno)
• ThetaCHC 6.13.2 (Levente Bajczi, Mihály Dobos-Kovács, Márk Somorjai, András Vörös)
• Ultimate Tree Automizer (Matthias Heizmann, Max Barth, Daniel Dietsch, Dominik Klumpp)
• Ultimate Unihorn (Matthias Heizmann, Max Barth, Daniel Dietsch, Dominik Klumpp)

LIA-Lin (⇒ compare results)

LIA (⇒ compare results)

LIA-Lin-Arrays (⇒ compare results)

LIA-Arrays (⇒ compare results)

ADT-LIA (⇒ compare results)

ADT-LIA-Arrays (⇒ compare results)

BV (⇒ compare results)

LRA-Lin (⇒ compare results)

Schedule

• April 25: solver submission deadline
• April 25: benchmark submission deadline
• May 8: presentation of results at SPIN 2025, co-located with ETAPS 2025, Hamilton, Canada

Benchmarks

The competition benchmarks were selected among the benchmarks available on Github. The format of the benchmarks is described here; a detailed description of the benchmark selection process can be found in CHC-COMP 2022: Competition Report.

The following tracks were evaluated at CHC-COMP 2025:

	LIA-Lin:		Linear Integer Arithmetic, linear clauses
	LIA-Nonlin:		Linear Integer Arithmetic, nonlinear clauses
	LIA-Lin-Arrays:		Linear Integer Arithmetic + Arrays, linear clauses
	LIA-Nonlin-Arrays:		Linear Integer Arithmetic + Arrays, nonlinear clauses
	ADT-LIA:		Linear Integer Arithmetic + non-recursive Algebraic data-types, nonlinear clauses
	ADT-LIA-Arrays:		Algebraic data-types + Arrays + Linear Integer Arithmetic, nonlinear clauses
	LRA:		Linear Real Arithmetic
	BV:		Bitvectors

In addition to the theories listed in the track names, benchmarks can also use the Bool theory.

Novel features of CHC-COMP in 2025

• Model Validation: A model validation demo track was introduced. Participants could opt-in to have their sat models checked independently.
• Infrastructure: Evaluations ran on the SV-COMP infrastructure at LMU Munich.

Organizers

• Gidon Ernst, LMU Munich, Germany

• Jose F. Morales, IMDEA Software Institute, Spain

Big thanks to

• Dirk Beyer, Po-Chun Chien, Matthias Kettl for support with the experimental setup in 2025
• SoSy-Lab at LMU Munich for sponsoring computing resources in 2025
• Everybody who organized and helped with the competition infrastructure over the last years:
  Nikolaj Bjørner, Adrien Champion, Emanuele De Angelis, Grigory Fedyukovich, Hari Govind V K, Arie Gurfinkel, Dejan Jovanovic, and Philipp Ruemmer
• Aaron Stump and StarExec for computing resources in past years

Previous editions of CHC-COMP

• 2024
• 2023
• 2022
• 2021
• 2020
• 2019
• 2018

Last updated: 2026-03-25 16:24:53 +0000