search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.15k stars 50 forks source link

Stabilize list_reversal_lasso. #1112

Closed jhjourdan closed 1 month ago

jhjourdan commented 1 month ago

There is really a big difference between the timing I can observe on my machine and those seen on CI. Is this related to the problem we have with reproducibility of step counts?

xldenis commented 1 month ago

Not sure what you mean?

jhjourdan commented 1 month ago

I mean that clearly the SMT solvers do not have the same behavior depending on the machine, and apparently this is true for both Altergo and CVC5. Hence this is indicating that Why3 non-deterministically generate different SMT files, depending on something from the environment. This would explain the instabilities we are observing here, and the step count problems.

xldenis commented 1 month ago

Interesting hypothesis. That seems like highly possible, but I will note that the steps fail locally on your machine if you try replaying a proof twice.