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

-------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                                           Provers   Justified   Unproved
-------------------------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                                                 .           .          .
Flow Dependencies                 .            .                                                 .           .          .
Initialization                   13           13                                                 .           .          .
Non-Aliasing                      .            .                                                 .           .          .
Run-time Checks                 185            .    163 (CVC5 72%, Trivial 26%, Z3 0%, altergo 2%)           .         22
Assertions                       22            .                              22 (CVC5 91%, Z3 9%)           .          .
Functional Contracts             76            .      75 (CVC5 86%, Trivial 5%, Z3 7%, altergo 3%)           .          1
LSP Verification                  .            .                                                 .           .          .
Termination                      73           73                                                 .           .          .
Concurrency                       .            .                                                 .           .          .
-------------------------------------------------------------------------------------------------------------------------
Total                           405    122 (30%)                                         260 (64%)           .    23 (6%)


max steps used for successful proof: 39596

Analyzed 25 units

in unit layernorm_pkg, 80 subprograms and packages out of 341 analyzed
  Layernorm_Pkg at layernorm_pkg.ads:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Layernorm_Pkg.LN_Mean at layernorm_pkg.ads:35 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 8 proved
  Layernorm_Pkg.LN_Normalised_Element at layernorm_pkg.ads:55 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 12 proved
  Layernorm_Pkg.LN_Variance at layernorm_pkg.ads:44 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 10 checks out of 13 proved
  Layernorm_Pkg.Layer_Normalise at layernorm_pkg.ads:74 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 37 checks out of 47 proved