Why3 Proof Results for Project "strassen"

Theory "strassen.MatrixMultiplication": fully verified in 124.82 s

ObligationsAlt-Ergo (1.01)CVC4 (1.4)Z3 (4.4.1)
VC for blit0.39------
VC for block0.15------
VC for block_ws0.14------
VC for add0.36------
VC for add_ws0.07------
VC for sub0.56------
VC for sub_ws0.06------
VC for mult_ijk---------
split_goal_wp
  1. precondition0.02------
2. assertion0.06------
3. postcondition0.04------
4. postcondition0.04------
5. postcondition0.04------
6. loop invariant init0.03------
7. loop invariant init0.03------
8. loop invariant preservation0.02------
9. loop invariant preservation0.03------
10. loop invariant init0.02------
11. loop invariant preservation0.02------
12. loop invariant preservation0.08------
13. loop invariant init0.05------
14. index in array bounds0.03------
15. index in array bounds0.07------
16. type invariant0.03------
17. index in array bounds0.04------
18. index in array bounds0.04------
19. loop invariant preservation0.06------
20. loop invariant preservation1.68------
21. loop invariant preservation0.04------
22. loop invariant preservation0.25------
23. loop invariant preservation0.05------
24. loop invariant preservation0.03------
25. assertion0.09------
26. type invariant0.02------
27. postcondition0.03------
28. postcondition0.05------
29. postcondition0.04------
VC for mult_ikj---------
split_goal_wp
  1. precondition0.03------
2. assertion0.07------
3. postcondition0.04------
4. postcondition0.02------
5. postcondition0.02------
6. loop invariant init0.04------
7. loop invariant init0.04------
8. loop invariant preservation0.08------
9. loop invariant preservation0.04------
10. loop invariant init0.04------
11. loop invariant preservation0.03------
12. loop invariant preservation0.04------
13. loop invariant init0.04------
14. index in array bounds0.03------
15. index in array bounds0.04------
16. type invariant0.04------
17. index in array bounds0.04------
18. index in array bounds0.04------
19. loop invariant preservation0.05------
20. loop invariant preservation2.38------
21. loop invariant preservation0.04------
22. loop invariant preservation0.04------
23. loop invariant preservation0.09------
24. loop invariant preservation0.04------
25. assertion0.09------
26. type invariant0.03------
27. postcondition0.05------
28. postcondition0.05------
29. postcondition0.04------
VC for assoc_proof0.25------
VC for mul_naive0.03------
VC for double_block0.12------
VC for padding---------
split_goal_wp
  1. precondition0.03------
2. precondition0.02------
3. precondition0.03------
4. precondition0.03------
5. precondition0.02------
6. assertion------0.62
7. assertion------0.72
8. assertion------0.14
9. postcondition0.05------
10. postcondition0.04------
11. postcondition0.06------
12. postcondition0.10------
13. postcondition0.06------
VC for strassenTimeout (5s)------
split_goal_wp
  1. VC for strassen0.02------
2. assertion0.04------
3. precondition0.02------
4. postcondition0.02------
5. postcondition0.04------
6. VC for strassen0.08------
7. precondition0.04------
8. precondition0.04------
9. precondition0.04------
10. precondition0.02------
11. assertion0.04------
12. variant decrease0.06------
13. precondition0.05------
14. precondition0.04------
15. precondition0.05------
16. precondition0.05------
17. precondition0.04------
18. precondition0.05------
19. precondition0.04------
20. precondition0.06------
21. precondition0.05------
22. precondition0.06------
23. precondition0.04------
24. precondition0.04------
25. precondition0.05------
26. precondition0.05------
27. precondition0.06------
28. precondition0.07------
29. precondition0.06------
30. precondition0.06------
31. precondition0.07------
32. assertion0.09------
33. assertion0.10------
34. precondition0.08------
35. precondition0.07------
36. postcondition---0.38---
37. postcondition0.07------
38. precondition0.04------
39. precondition0.04------
40. precondition0.04------
41. precondition0.04------
42. precondition0.04------
43. precondition0.05------
44. precondition0.05------
45. precondition0.06------
46. precondition0.04------
47. variant decrease0.08------
48. precondition0.10------
49. precondition0.10------
50. precondition0.08------
51. precondition0.10------
52. precondition0.09------
53. postcondition0.17------
54. postcondition0.08------
55. postcondition0.05------
56. precondition0.06------
57. precondition0.06------
58. precondition0.08------
59. precondition0.09------
60. precondition0.09------
61. precondition0.10------
62. precondition0.12------
63. precondition0.11------
64. precondition0.13------
65. precondition0.14------
66. precondition0.12------
67. precondition0.11------
68. precondition0.14------
69. precondition0.14------
70. precondition0.14------
71. precondition0.13------
72. precondition0.14------
73. precondition0.13------
74. precondition0.14------
75. precondition0.13------
76. precondition0.15------
77. precondition0.15------
78. precondition0.15------
79. precondition0.14------
80. assertion0.20------
81. assertion0.20------
82. precondition0.11------
83. precondition0.14------
84. precondition0.17------
85. precondition0.17------
86. precondition0.19------
87. precondition0.19------
88. precondition0.14------
89. precondition0.19------
90. precondition0.22------
91. precondition0.22------
92. precondition0.17------
93. precondition0.21------
94. precondition0.21------
95. precondition0.22------
96. precondition0.18------
97. precondition0.21------
98. precondition0.22------
99. precondition0.22------
100. precondition0.22------
101. precondition0.18------
102. precondition0.22------
103. precondition0.22------
104. precondition0.25------
105. precondition0.24------
106. assertion0.35------
107. assertion0.35------
108. precondition---------
compute_specified
  1. precondition---------
simplify_trivial_quantification_in_goal
  1. precondition---------
compute_specified
  1. precondition---------
introduce_premises
  1. precondition---------
compute_specified
  1. precondition0.10------
109. precondition0.34------
110. precondition---------
compute_specified
  1. precondition---------
simplify_trivial_quantification_in_goal
  1. precondition---------
compute_specified
  1. precondition---------
introduce_premises
  1. precondition---------
compute_specified
  1. precondition0.12------
111. precondition0.30------
112. precondition0.28------
113. precondition0.24------
114. precondition---------
compute_specified
  1. precondition---------
simplify_trivial_quantification_in_goal
  1. precondition---------
compute_specified
  1. precondition---------
introduce_premises
  1. precondition---------
compute_specified
  1. precondition0.17------
115. precondition0.40------
116. precondition---------
compute_specified
  1. precondition---------
simplify_trivial_quantification_in_goal
  1. precondition---------
compute_specified
  1. precondition---------
introduce_premises
  1. precondition---------
compute_specified
  1. precondition0.17------
117. precondition0.44------
118. precondition0.47------
119. precondition0.28------
120. precondition0.28------
121. precondition0.52------
122. precondition---------
compute_specified
  1. precondition---------
simplify_trivial_quantification_in_goal
  1. precondition---------
compute_specified
  1. precondition---------
introduce_premises
  1. precondition---------
compute_specified
  1. precondition0.16------
123. precondition0.63------
124. precondition0.52------
125. precondition0.31------
126. precondition0.33------
127. precondition0.50------
128. precondition0.32------
129. precondition0.58------
130. precondition0.64------
131. precondition0.34------
132. assertion---0.61---
133. assertion---0.59---
134. precondition0.64------
135. precondition0.34------
136. precondition0.67------
137. precondition0.36------
138. precondition0.37------
139. precondition1.41------
140. precondition0.75------
141. precondition0.40------
142. precondition0.39------
143. precondition0.83------
144. precondition0.86------
145. precondition0.44------
146. precondition0.45------
147. precondition1.72------
148. precondition0.87------
149. precondition0.45------
150. precondition0.41------
151. precondition1.91------
152. precondition0.77------
153. precondition0.46------
154. precondition0.49------
155. precondition0.92------
156. precondition1.06------
157. precondition0.52------
158. precondition1.06------
159. precondition0.54------
160. precondition0.55------
161. precondition2.35------
162. precondition1.12------
163. precondition0.53------
164. precondition1.03------
165. precondition0.55------
166. precondition0.58------
167. precondition2.90------
168. precondition1.24------
169. precondition0.58------
170. precondition1.10------
171. precondition0.60------
172. precondition1.34------
173. precondition0.63------
174. precondition1.31------
175. precondition0.69------
176. precondition1.64------
177. precondition0.69------
178. precondition1.26------
179. precondition0.70------
180. precondition1.41------
181. precondition0.69------
182. precondition1.28------
183. precondition0.60------
184. assertion---------
compute_specified
  1. assertion---------
simplify_trivial_quantification_in_goal
  1. assertion---------
compute_specified
  
185. VC for strassen3.22------
186. precondition0.06------
187. precondition0.53------
188. precondition0.52------
189. precondition0.54------
190. precondition0.54------
191. precondition0.62------
192. precondition0.60------
193. precondition0.07------
194. precondition0.58------
195. precondition0.69------
196. precondition0.66------
197. precondition0.69------
198. precondition0.08------
199. precondition0.77------
200. precondition0.64------
201. precondition0.06------
202. precondition0.06------
203. assertion---------
split_goal_wp
  1. VC for strassen11.91------
2. VC for strassen2.22------
3. VC for strassen7.21------
4. VC for strassen4.28------
5. VC for strassen10.58------
6. VC for strassen0.51------
204. postcondition0.12------
205. postcondition0.07------