Dear Akihisa,

I checked this example. The configuration "certified" of AProVE was chosen in such a way, that as many interruptions of benchexec or the postprocessor as possible can be avoided. Thus, if the run of AProVE does not lead to "YES + Proof", "NO + Proof" or "WORST_CASE + Proof" the underlying starexec runscript does not output anything at all.

In the given example, the following happens: We set the timeout of AProVE to the timeout of starexec minus 10s (to have some time for printing the proof etc.). Thus, AProVE internally kills the process after 290s. Without our runscript for the certified categories it outputs "KILLED" as it cannot (dis)prove termination within 90s.

The configuration "standard" of AProVE does not call AProVE with a timeout, i.e., here it can indeed happen that benchexec kills AProVE and notes a timeout.

Best,

Marcel

- AProVE certified: https://www.starexec.org/starexec/secure/details/pair.jsp?id=516304215
No idea, but time is almost up. Is there some pre-timeout process that doesn't write even "TIMEOUT"?