Stainless non-terminating behaviour with timeout

[Sporarum]

When running stainless --watch --compact --timeout={1|20} {|--functions=leftDistributivity} */*.scala, stainless doesn't terminate[^1] ({a|b} meaning with either a or b) The function is run from the root of the folder, and the behavior is normal[^2] if this line is uncommented: https://gitlab.epfl.ch/bernet/transfinite-lists-for-stainless/-/blob/non-terminating/lemmas/mult.scala#L267

In the case where the --functions=... is not there, stainless behaves normally until reaching Verified 6xx/xxx and then stays there (the xs are always the same), in case where it is, it stays at Verified 0/0 forever

As stainless doesn't crash, there is no stack trace

[^1]: Or more accurately, doesn't terminate even after giving it way more than it's timeout [^2]: There are some timeouts since part of the proof is missing, but everything gets proven as expected

[sfiruch]

Does this happen as well when you use an external solver? I think it's a known issue that internal solvers don't respect the timeout in all cases.

[vkuncak]

Another source can be termination checks, which diverge in some cases.