Why3 Proof Results for Project "naive"

Theory "naive.MatrixMultiplication": fully verified in 0.47 s

ObligationsAlt-Ergo (1.01)
VC for mult_naive---
split_goal_wp
  1. precondition0.01
2. postcondition0.01
3. postcondition0.01
4. loop invariant init0.01
5. loop invariant init0.01
6. loop invariant preservation0.01
7. loop invariant preservation0.01
8. loop invariant init0.01
9. loop invariant preservation0.01
10. loop invariant preservation0.01
11. loop invariant init0.01
12. index in array bounds0.01
13. index in array bounds0.01
14. type invariant0.01
15. index in array bounds0.01
16. index in array bounds0.01
17. loop invariant preservation0.03
18. loop invariant preservation0.19
19. loop invariant preservation0.02
20. loop invariant preservation0.01
21. loop invariant preservation0.01
22. loop invariant preservation0.03
23. type invariant0.01
24. postcondition0.00
25. postcondition0.01