Summary of SPARK analysis
=========================

------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                                    Provers   Justified   Unproved
------------------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                                          .           .          .
Flow Dependencies                 .            .                                          .           .          .
Initialization                    .            .                                          .           .          .
Non-Aliasing                      .            .                                          .           .          .
Run-time Checks                 209            .    179 (CVC5 79%, Trivial 20%, altergo 0%)           .         30
Assertions                        2            .                                   2 (CVC5)           .          .
Functional Contracts             64            .                  58 (CVC5 91%, Trivial 9%)           .          6
LSP Verification                  .            .                                          .           .          .
Termination                      73           73                                          .           .          .
Concurrency                       .            .                                          .           .          .
------------------------------------------------------------------------------------------------------------------
Total                           384    109 (28%)                                  239 (62%)           .    36 (9%)


max steps used for successful proof: 9208

Analyzed 25 units

in unit max_pool_pkg, 77 subprograms and packages out of 308 analyzed
  Max_Pool_Pkg at max_pool_pkg.ads:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Max_Pool_Pkg.Max_Pool at max_pool_pkg.ads:38 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 40 checks out of 72 proved