Dear all,
thanks again for participating in CHC-COMP 2025.
While the competition was generally successful, not everything went perfectly, and the model validation track is still in preparation.
1. Expected Verdicts:
There was disagreement among the solvers on some benchmarks. Martin Blicha has kindly looked into this and prepared pull requests to determine the ground truth which include justifications for the change. If you have stakes in this, please review the pull requests and comment, so that we can merge these: https://github.com/chc-comp/chc-comp25-benchmarks/pulls
The community should also agree on how to deal with tools that produce wrong results. SV-COMP has a scoring scheme with heavy penalties but there are other options. At least, we should mark wrong results in the tables prominently.
2. Missing logfiles
I am aware that logfiles are currently not linked correctly in the result table, however, you can access them by manually specifying the URL, as in https://www.cip.ifi.lmu.de/~ernstg/chc-comp2025/golem-x64-linux/test/results... I'm not sure what the problem is but I'll figure it out sometime.
3. Missing results and Tool updates
Due to an oversight, MuCyc was not considered in LIA. Many apologies to the tool authors, it appears the omission had been introduced (by me) only after having the final results checked. I will add the results from the existing evaluation, which means, potentially the ranking will change.
Moreover, some tool authors have submitted updated tool archives in response to results from the competition. I'd therefore like to offer *all* tool authors the chance to update their archives. Moreover, please consider uploading your tool to Zenodo, in which case we can link it on the competition website.
4. Tool versions
Some tools currently lack version information or output dummy versions. You can see this in the benchmark tables resp. the absence of version information on the main CHC-COMP page. It would be great if this can be fixed, in particular for re-submissions, by including a flag "--version" or similar.
5. Model validation (yay)!
Until HCVS we really want to have a model validation track ready. The following script takes as first argument the benchmark file and reads from stdin the solver output ("sat/unsat" followed by a model). Output of the script is an SMT-LIB file with a single assertion and expected status "unsat" in which case the model is confirmed. https://github.com/chc-comp/chc-comp25-scripts/blob/main/validate-model.py
Currently, only Eldarica and Golem have indicated that they can produce models. It would be great if some more participants can participate! In that case, please confirm that your tool outputs a model that can be parsed by the script above (there are already some variations across Z3, Golem, Eldarica!). We plan to cross-check the models with at least Z3 and CVC5.
6. Proof validation (nay!)
Probably not this year. I don't feel confident on making a proposal for a common format. Martin, Philipp, any thoughts?
Best,