Klever

A long ago we introduced lightweight verification results primarily to meet the challenge with performance overheads for different actions. Besides, they helped to keep a disk space quite considerably.

Indeed, lightweight verification results are primary verification results that Klever users would like to obtain. For the production mode this is the default setting. That's why this conception is very important. It should not just speed up some actions. It should represent verification results easier when most intermediate details are omitted. In addition, to omitting these details in representation, they should be removed (or not stored at all) to serve original purposes.

Perhaps, the only difference of lightweight verification results from full-weight verification results is absence of component trees. Just some statistics about operation of components (consumed computational resources, the number of instances) should be remained. Of course, all meaningful verification results (unsafes, safes, unknowns and code coverage) should be presented always. In addition, there can be some very useful data, like input files of verifiers that should be stored in both modes if required.

Please, do not suggest brilliant ideas how to simplify representation of verification results further within this issue. This is a scope of other issues.