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

------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                        Provers   Justified    Unproved
------------------------------------------------------------------------------------------------------
Data Dependencies                24          24                              .           .           .
Flow Dependencies                 .           .                              .           .           .
Initialization                    .           .                              .           .           .
Non-Aliasing                      .           .                              .           .           .
Run-time Checks                 201           .    148 (CVC5 76%, Trivial 24%)           .          53
Assertions                      108           .                     108 (CVC5)           .           .
Functional Contracts             64           .     38 (CVC5 90%, Trivial 10%)           .          26
LSP Verification                  .           .                              .           .           .
Termination                      52          52                              .           .           .
Concurrency                       .           .                              .           .           .
------------------------------------------------------------------------------------------------------
Total                           449    76 (17%)                      294 (65%)           .    79 (18%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit dgemm_pkg, 52 subprograms and packages out of 206 analyzed
  Dgemm_Pkg at dgemm_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgemm_Pkg.Double_General_Matrix_Multiply at dgemm_pkg.ads:28 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 133 checks out of 208 proved