analyzer
analyzer copied to clipboard
Spurious out of memory on SV-COMP Intel TDX tasks
The knightly runs always have some Intel TDX tasks from sv-benchmarks where the result spuriously flips between unknown and OUT OF MEMORY (in either direction). I find this suspicious.
It's important to note that this is unlike spurious TIMEOUT result flips which can happen due to unpredictable CPU behavior (automated frequency adjustment) and overall load on the system. How much memory we allocate should not be affected by such factors.
I don't know why this could be happening but there are some quite extreme cases: OUT OF MEMORY in 42s flipping to unknown in 104s (or vice versa).