goblint
Use SV-COMP time limit for soft exit
SV-COMP and BenchExec can give the task time limit to the tool. Goblint doesn't use this information and just keeps running after the BenchExec soft time limit until it is killed at the hard time limit.
We should use this information to do a soft exit after the given time limit because continuing solving gives us nothing. It just wastes resources and makes benchmarks run longer.
BenchExec should send SIGTERM on soft time limit and Goblint does react to it (and doesn't even override the signal handler), but somehow it doesn't work under BenchExec? SV-COMP 2023 results contain over 1416 instances of Goblint TIMEOUT with 960s CPU time.
I couldn't reproduce this with runexec nor under BenchExec. Even with SV-COMP 2023 setup: BenchExec 3.16 and Goblint svcomp23.
It still happens in Dirk's preruns though.
It might depend on what exactly Goblint is doing at the time it gets the signal. OCaml's signal handling isn't necessarily immediate. If a signal is received, the signal handler just marks it as received but doesn't do anything else. Only at certain points in the OCaml runtime is this signal flag checked and handlers executed.
SV-COMP 2025 prerun results contain 1298 instances of Goblint TIMEOUT with 960s CPU time, so the issue still remains after the catch-all exception handler fixes.
In SV-COMP 2026 preruns there are no results with CPU time over 900s. I have no idea when or why this might've changed then.
I was also afraid of how it behaves with the portfolio runner now, but that doesn't seem to be an issue.