Mentions légales du service

Skip to content

Stepslimit for CE bench to stabilize the CI

Benedikt Becker requested to merge stepslimit-for-ce-bench into master

The consistency of the results in the CE bench seem to have deteriorated recently, breaking the CI with differing results. (Before, retrying the job in the CI helped, but not anymore. There were no related changes in the CE generation. Maybe a change in the hardware of the CI machine?)

One issue may be that counterexamples have been requested sofar using a timelimit, which results of course in different CEs depending on the CPU speed. This MR implements a step limit for why3 prove and uses an estimated steplimit in the CE benches to reduce inconsistencies.

Merge request reports