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

-----------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                        Provers   Justified   Unproved
-----------------------------------------------------------------------------------------------------
Data Dependencies                24          24                              .           .          .
Flow Dependencies                 .           .                              .           .          .
Initialization                    2           2                              .           .          .
Non-Aliasing                      .           .                              .           .          .
Run-time Checks                 127           .    123 (CVC5 68%, Trivial 32%)           .          4
Assertions                        6           .                       4 (CVC5)           .          2
Functional Contracts             50           .      41 (CVC5 92%, Trivial 8%)           .          9
LSP Verification                  .           .                              .           .          .
Termination                      52          52                              .           .          .
Concurrency                       .           .                              .           .          .
-----------------------------------------------------------------------------------------------------
Total                           261    78 (30%)                      168 (64%)           .    15 (6%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit relu_pkg, 52 subprograms and packages out of 206 analyzed
  Relu_Pkg at relu_pkg.ads:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Relu_Pkg.Apply_Relu at relu_pkg.ads:25 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 18 proved