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

-------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                               Provers   Justified   Unproved
-------------------------------------------------------------------------------------------------------------
Data Dependencies                56           56                                     .           .          .
Flow Dependencies                 .            .                                     .           .          .
Initialization                    4            4                                     .           .          .
Non-Aliasing                      .            .                                     .           .          .
Run-time Checks                 193            .    176 (CVC5 79%, Trivial 19%, Z3 2%)           .         17
Assertions                       26            .                             26 (CVC5)           .          .
Functional Contracts            174            .           168 (CVC5 87%, Trivial 13%)           .          6
LSP Verification                  .            .                                     .           .          .
Termination                     106          105                                     .           .          1
Concurrency                       .            .                                     .           .          .
-------------------------------------------------------------------------------------------------------------
Total                           559    165 (30%)                             370 (66%)           .    24 (4%)


max steps used for successful proof: 12903

============================
Most difficult proved checks
============================

spark-lemmas-floating_point_arithmetic.ads:209:33: range check proved in max 1 seconds
int8_matmul_pkg.adb:56:35: overflow check proved in max 1 seconds

========================
Detailed analysis report
========================

Analyzed 70 units

in unit int8_matmul_pkg, 119 subprograms and packages out of 443 analyzed
  Int8_Matmul_Pkg at int8_matmul_pkg.ads:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Int8_Matmul_Pkg.Int8_Matmul at int8_matmul_pkg.ads:67 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 46 checks out of 59 proved
  Int8_Matmul_Pkg.Sum_Of_Products at int8_matmul_pkg.ads:44 flow analyzed (0 errors, 1 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 15 proved