Dear CHC-COMP Community,

I have finished executing the experiments, and a preliminary result page is available under https://chc-comp.github.io/chc-comp-2026/

For certifying the results (i.e., no misconfiguration or other issue happened on the infrastructure part), please fill out the following form: https://forms.gle/QZwfGFH2Tnz5WVjK9. Deadline is 1 week from now (22nd of May), at which point, I will assume positive answers for tools that have not yet filled out the form.

Some technical details and interesting information:

* there were 8 participating solvers this year, and an hors concours spacer as the 9th * Unless there are drastic uncovered issues, Eldarica comfortably won the overall category - Congratulations! * there is now a stable model-generation track, where SMT solvers independently certify the models of CHC solvers * there are around 20 tasks that solvers don't seem to agree on (same amount of sat and unsat unswers — see https://github.com/chc-comp/chc-comp26-benchmarks/issues/4) * there were some last-minute changes to the benchmarks, these were ignored in the score calculation (if there are more issues, I'd be happy to re-run these as well) * we used 47996400 seconds of CPU time (around 1.5 years) for the whole competition

Thank you everyone for the submissions, please fill out the form, and let us know if there are any issues (primarily via the form, or via email)!

Best regards, The organizers of CHC-COMP'26 Levente and Konstantin

-- Levente Bajczi

PhD Student Critical Systems Research Group BME-MIT ________________________________ From: Bajczi Levente levente.bajczi@edu.bme.hu Sent: 27 April 2026 17:29 To: chc-comp@software.imdea.org chc-comp@software.imdea.org Subject: Re: CHC Competition 2026 Submission Procedure

Dear CHC-COMP Community,

The first rounds of smoke tests have been executed; the up-to-date results are available under https://chc-comp.github.io/chc-comp-2026/tables/. Note that we only executed a randomly selected subset of the tasks per category (at most 10 tasks, with a mix of sat and unsat verdicts), with half a minute of timeout and a very small resource allocation.

Each link in the table goes to a different BenchExec table, where the logs and results are available. The input tasks are unfortunately not clickable (yet), but based on name, the https://github.com/chc-comp/chc-comp26-benchmarks repository should help find them.

For the model validation track (lower table), each cell also includes information on the model validation status. Here, only the green "true" values are counted as correct, which means the model (visible in the log file) has been validated by at least one SMT solver. Blue "true" values are unconfirmed, which means no SMT solver was able to validate the model.

Please inspect these preliminary results and let me know if there are any issues. I would also like an answer if you did not find any issues, from the following solvers' submitters (which are already merged):

* Eldarica * ChocoCatalia * LoAT (results will be published in ~30 minutes) * Golem * Theta

With all potential issues, please include the input filename, not just the category name, because once a new smoke test run will be completed, the tables will have been overwritten.

There are 2 tools (MuCyC, PCSat) where further work is necessary for the submission. I will definitely run at least one more smoke test once these tools get merged. For everyone else, feel free to submit a new PR, either to enter another solver, or to make an update to an existing one. I can promise at least one further test for each submission until the deadline (2nd of May).

Best regards, Levente Bajczi (in the name of the CHC-COMP organizers)

-- Levente Bajczi

PhD Student Critical Systems Research Group BME-MIT ________________________________ From: konstantin.britikov--- via chc-comp chc-comp@software.imdea.org Sent: 23 April 2026 21:25 To: chc-comp@software.imdea.org chc-comp@software.imdea.org Subject: [chc-comp] CHC Competition 2026 Submission Procedure

Dear CHC Competition Community,

We would like to explain the procedure for solver submission for the CHC Competition this year. To reiterate, we will start the smoke tests on April 25th, and the hard submission deadline is May 2nd.

To submit a CHC solver, please submit a pull request to the chc-comp-2026 repository: https://github.com/chc-comp/chc-comp-2026

Instructions on submission are provided in the README file of the repository. You can also find a sample tool submission for reference here: https://github.com/chc-comp/chc-comp-2026/pull/5

In case of any questions, don't hesitate to ask us!

We would also like to announce that the Golem and Theta CHC solvers will participate in this year's competition. While the organisers have contributed to both of these solvers, we would like to clarify that this does not present a conflict of interest: as in last year’s competition, all solvers will be evaluated on the complete set of available benchmarks without exception, ensuring a fully fair and transparent competition for all participants.

Also, to answer Philip's question, there will be a BV track this year. We've added the information on the webpage.

Best regards, Levente Bajzi and Konstantin Britikov