SPAT will only work as intended after a run from scratch of GNATprove, not on a subsequent run. Indeed, on subsequent runs, GNATprove will regenerate .spark files but spend no time on checks that were already proved, or even in some cases no time on any checks (if switch --output-msg-only is used). As a result, the time info for most check is just "0.0 s".
This should be described in the README, so that users are not surprised.
The underlying reason for that behavior of GNATprove is that the Why3 session files are where all the history of prover runs and current state is stored. A reasonable solution to improve the connection between GNATprove and SPAT would be to regenerate the timing information in .spark files from the info read in the Why3 session files. Feel free to open an Issue on spark2014 repo if you'd like us to investigate it!
SPAT will only work as intended after a run from scratch of GNATprove, not on a subsequent run. Indeed, on subsequent runs, GNATprove will regenerate .spark files but spend no time on checks that were already proved, or even in some cases no time on any checks (if switch --output-msg-only is used). As a result, the time info for most check is just "0.0 s".
This should be described in the README, so that users are not surprised.
The underlying reason for that behavior of GNATprove is that the Why3 session files are where all the history of prover runs and current state is stored. A reasonable solution to improve the connection between GNATprove and SPAT would be to regenerate the timing information in .spark files from the info read in the Why3 session files. Feel free to open an Issue on spark2014 repo if you'd like us to investigate it!