Dear all,

this is a good question. The 2022 report states:

"each job was limited to 1800s CPU time, 1800s wall-clock time, and 64GB memory"

Jose ran the benchmarks last year, but I suspect it was with the same limits. I propose we keep the 1800s CPU timelimit, which implies 1800s wall-clock time.

We plan to use this machine type: Intel Xeon E3-1230 v5 @ 3.40 GHz, 4x2 cores with hyperthreading, 33GB of main memory

Please speak up if you disagree with the the reduction in main memory.

Best, Gidon

On 4/17/25 3:11 PM, Florian Frohn wrote:

Dear Gidon,

what will be the time limit (both wall clock and cpu time would be interesting)?

Thanks, Florian

On 4/17/25 10:11, Gidon Ernst wrote:

...

Dear all,

To participate in CHC-COMP 2025, we kindly ask you to register your solver via this form, the earlier the better, so we can check for technical issues, but no later than Friday, April 25:

https://forms.gle/Lh6VmRjRDaknZ4xU9

Submission should include a download link pointing to the tool archive, such as a public release on a code-hosting platform.

Note, you may update your response later, for example in case you want to make a new release between initial submission and submission of the final version for the competition.

Please indicate the desired command line, too, as well as a command line that produces evidence (models, proofs), which can be the same as the main command line.

Please also indicate the categories you wish to be evaluated in. LRA and BV are up to the availability of benchmarks.

If you wish to contribute benchmarks still, please get in touch.

Best,