EasyCrypt progressive slowdown involving simplification hints

[alleystoughton]

This EasyCrypt script illustrates a progressive slowdown of EasyCrypt.

Some simplification hints are introduced, and then there is an aborted lemma that is repeated over and over. The lemma actually solves its goal, before the abort.

At first the lemma is proved instantly, but later on it takes much longer. There are points where nothing happens for minutes - probably garbage collection? - but then things start up again, somewhat faster. But the overall trend is a progressive slowdown.

Taking out one of the simplification hints makes the script run fast without any slowdown.

[strub]

Hi. Thank you for the file. I am more & more suspecting matching to be part of the problem. This would explain why pretty printing (that uses matching for printing notations) & your file suffer from this slowdown.