Inlining extraction of Steel.ST code with while_loop to krml blows up

[tahina-pro]

Hi everyone,
I am trying to extract the following Steel.ST code to .krml:
https://github.com/project-everest/everparse/blob/3eba1fba7e63f7710fe03a1441d5df93f4efc9b4/tests/steel/Test.fst#L60
Basically, I have a function, iter_max, using a list fold operator ultimately inlining to Steel.C.Loops.while_loop, to compute the maximum value of a list from its byte representation. Then I call this function from another function, test.
If I mark iter_max as inline_for_extraction, then F* loops with ever-increasing memory consumption. But if I don't, then extraction works fine.
Can anyone please help me there? Where should I start debugging extraction to .krml?
Thank you in advance!

[tahina-pro]

This is now solved by #2668 . Thanks again!