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(a)software.imdea.org> Sent: 23 April 2026 21:25 To: chc-comp(a)software.imdea.org <chc-comp(a)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