Bogomips
When replaying a proof, Why3 multiplies the previous running time by 2 when setting the time limit. This allows for some variance in the execution of provers or in the load of the computer. Unfortunately, this is too large a variance when replaying a proof on the same computer, and this is too small when replaying on a computer with vastly different specifications. Moreover, for provers that use the time limit to guide their heuristics, this can completely change their behavior.
Suggestion: Run a bogomips-like test at why3 config
time and store the result into why3.conf
. Store the value inside proof sessions. Compare the session-stored and configuration-stored values when replaying a session to better choose the allowed variance in running time.