2025 | Format | Rules | Github |

Organizers

• Gidon Ernst, LMU Munich, Germany
• Jose F. Morales, IMDEA Software Institute, Spain

Mailing List

Please register here https://software.imdea.org/mailman3/postorius/lists/chc-comp.software.imdea.org to receive updates and to participate in the discussion

Note, there is also the ealier Gitter chatroom, but this seemed to have little popularity. Please be aware that we will not necessarily be responsive over there.

New: Benchmarks and Results

• CHC-COMP 2025 report as presented at SPIN 2025 (with a minor update in LIA-Lin- Arrays)
• the full list of benchmarks is available here: https://github.com/chc-comp/chc-comp25-benchmarks
• scripts for running the competition are here: https://github.com/chc-comp/chc-comp25-scripts, making use of some of the other repositories, too
• 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.

Tools

• 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)

Participation and Schedule (updated!)

• April 25: solver submission deadline.
  Participate here https://forms.gle/Lh6VmRjRDaknZ4xU9.
  We aim to do some pre-runs to check for technical issues.

• April 25: benchmark submission deadline.
  Benchmarks can be contributed by sending is the link to some Github repository.
  We will then fork it in the CHC-COMP Github organization.
  Benchmark contributions can be updated via pull requests.

• May 8: presentation of results at SPIN 2025, co-located with ETAPS 2025, Hamilton, Canada.

Infrastructure

The key difference to earlier years will be that evaluations will run on the SV-COMP infrastructure at the LMU Munich.

• You can already test your solver in the competition environment, which is provided as a Docker file. It is based on standard Ubuntu 24.04.
• If you are missing a standard software package from the list provided there, you may consider submitting a pull requests, but we do not guarantee that this will be honored.
• Please otherwise package all additional dependencies with your solver submission.
• We aim to keep the overhead on the side of participants low. This means we will offer a standard way to integrate, similar to the one on StarExec. Typical SV-COMP participation steps, like submitting a toolinfo module or benchmark definitions are not necessary for CHC-COMP.
• We will likely use this type of machine: Intel Xeon E3-1230 v5 @ 3.40 GHz, 4x2 cores with hyperthreading, 33GB of main memory. Results will be reported by wall-time and by CPU time to illustrate the benefits of solvers that can run parallel threads.

Benchmarks

The competition benchmarks will be selected among the benchmarks available on GitHub. If you have benchmarks of any kind that can be made public, and that are not yet on Github, please upload! 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 final list of benchmarks used in the competition will be made public, together with the competition results.

The following tracks are planned for 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: Linar Real Arithmetic (tentative)
• BV: Bitvectors (tentative)

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: We introduce a model validation demo track. Participants can opt-in to have their sat models checked independently. We will report these results separately from the main standings. Details and format are being clarified at the moment.
• Massively Parallel Track: We may run selected evaluations with on a machine with 256 cores. Please get in touch if you think your solver may be able to make use of this.

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, notably:
  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

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

Last updated: 2025-05-12 15:35:04 +0000