Dear Marcel, I see, but according to the rule, tools should output MAYBE rather than nothing. I think disabling the custom timeout will be the easiest. Best, Akihisa On 2021/07/05 16:55, Marcel Hark wrote:
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
Am 05.07.21 um 04:45 schrieb YAMADA, Akihisa:
- 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"? --
Marcel Hark Research Group Computer Science 2 RWTH Aachen University Ahornstr. 55 52074 Aachen Germany
E-Mail: marcel.hark@cs.rwth-aachen.de" Phone: +49-241/80-21218 Fax: +49-241/80-22217 Room: 4208