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

-------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                        Provers   Justified    Unproved
-------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                              .           .           .
Flow Dependencies                 .            .                              .           .           .
Initialization                    6            6                              .           .           .
Non-Aliasing                      .            .                              .           .           .
Run-time Checks                 249            .    207 (CVC5 83%, Trivial 17%)           .          42
Assertions                       24            .                      24 (CVC5)           .           .
Functional Contracts             65            .      58 (CVC5 92%, Trivial 8%)           .           7
LSP Verification                  .            .                              .           .           .
Termination                      73           73                              .           .           .
Concurrency                       .            .                              .           .           .
-------------------------------------------------------------------------------------------------------
Total                           453    115 (25%)                      289 (64%)           .    49 (11%)


max steps used for successful proof: 17110

Analyzed 25 units

in unit conv2d_fp64_pkg, 78 subprograms and packages out of 309 analyzed
  Conv2d_Fp64_Pkg at conv2d_fp64_pkg.ads:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Conv2d_Fp64_Pkg.Convolution_Sum_FP64 at conv2d_fp64_pkg.ads:40 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 10 checks out of 27 proved
  Conv2d_Fp64_Pkg.Convolve_2d_Fp64 at conv2d_fp64_pkg.ads:67 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 80 checks out of 108 proved