[BUG] Lemmas marked as timed out way before reaching the time limit

[racoucho1u]

When running a recipe with several lemmas (eg spdm121_composition_fix.spthy from https://github.com/ComprehensiveSPDM/TamarinSPDMAnalysis) some lemmas in the results are marked as timed out even though the displayed runtime for the lemma is inferior to the timeout specified for the task. Rerunning the lemmas often correct the problem. I also noted the peak memory used in these cases is always 0Mb which is already suspicious.

To Reproduce
Create and run a recipe for the file spdm121_composition_fix.spthy from https://github.com/ComprehensiveSPDM/TamarinSPDMAnalysis. I used 6 different versions of Tamarin and all were affected on different lemmas. For reference I used a limit of 4 cores and 40Gb limit per lemma and a total limit of 20 cores and 200Gb. I used the Tamarin options "-d0" and the preprocess flags "secrecy attestation authentication Sanity".

Expected behavior
Lemmas should not timeout before reaching the specified time limit.

Screenshots
An snippet of a report with two problematic lemmas.

[lmandrelli]

Hi Maïwenn, could you try to use the run command with the debug mode and tell me what was the return code when a task is considered as time out under these conditions ? I detect time out based on return code, it could be that the machine you are running batch-tamarin does unexpected return with the processes.