Obligations | Alt-Ergo (1.01) | CVC4 (1.4) | Z3 (4.4.1) |
VC for blit | 0.39 | --- | --- |
VC for block | 0.15 | --- | --- |
VC for block_ws | 0.14 | --- | --- |
VC for add | 0.36 | --- | --- |
VC for add_ws | 0.07 | --- | --- |
VC for sub | 0.56 | --- | --- |
VC for sub_ws | 0.06 | --- | --- |
VC for mult_ijk | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 0.02 | --- | --- |
2. assertion | 0.06 | --- | --- |
3. postcondition | 0.04 | --- | --- |
4. postcondition | 0.04 | --- | --- |
5. postcondition | 0.04 | --- | --- |
6. loop invariant init | 0.03 | --- | --- |
7. loop invariant init | 0.03 | --- | --- |
8. loop invariant preservation | 0.02 | --- | --- |
9. loop invariant preservation | 0.03 | --- | --- |
10. loop invariant init | 0.02 | --- | --- |
11. loop invariant preservation | 0.02 | --- | --- |
12. loop invariant preservation | 0.08 | --- | --- |
13. loop invariant init | 0.05 | --- | --- |
14. index in array bounds | 0.03 | --- | --- |
15. index in array bounds | 0.07 | --- | --- |
16. type invariant | 0.03 | --- | --- |
17. index in array bounds | 0.04 | --- | --- |
18. index in array bounds | 0.04 | --- | --- |
19. loop invariant preservation | 0.06 | --- | --- |
20. loop invariant preservation | 1.68 | --- | --- |
21. loop invariant preservation | 0.04 | --- | --- |
22. loop invariant preservation | 0.25 | --- | --- |
23. loop invariant preservation | 0.05 | --- | --- |
24. loop invariant preservation | 0.03 | --- | --- |
25. assertion | 0.09 | --- | --- |
26. type invariant | 0.02 | --- | --- |
27. postcondition | 0.03 | --- | --- |
28. postcondition | 0.05 | --- | --- |
29. postcondition | 0.04 | --- | --- |
VC for mult_ikj | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 0.03 | --- | --- |
2. assertion | 0.07 | --- | --- |
3. postcondition | 0.04 | --- | --- |
4. postcondition | 0.02 | --- | --- |
5. postcondition | 0.02 | --- | --- |
6. loop invariant init | 0.04 | --- | --- |
7. loop invariant init | 0.04 | --- | --- |
8. loop invariant preservation | 0.08 | --- | --- |
9. loop invariant preservation | 0.04 | --- | --- |
10. loop invariant init | 0.04 | --- | --- |
11. loop invariant preservation | 0.03 | --- | --- |
12. loop invariant preservation | 0.04 | --- | --- |
13. loop invariant init | 0.04 | --- | --- |
14. index in array bounds | 0.03 | --- | --- |
15. index in array bounds | 0.04 | --- | --- |
16. type invariant | 0.04 | --- | --- |
17. index in array bounds | 0.04 | --- | --- |
18. index in array bounds | 0.04 | --- | --- |
19. loop invariant preservation | 0.05 | --- | --- |
20. loop invariant preservation | 2.38 | --- | --- |
21. loop invariant preservation | 0.04 | --- | --- |
22. loop invariant preservation | 0.04 | --- | --- |
23. loop invariant preservation | 0.09 | --- | --- |
24. loop invariant preservation | 0.04 | --- | --- |
25. assertion | 0.09 | --- | --- |
26. type invariant | 0.03 | --- | --- |
27. postcondition | 0.05 | --- | --- |
28. postcondition | 0.05 | --- | --- |
29. postcondition | 0.04 | --- | --- |
VC for assoc_proof | 0.25 | --- | --- |
VC for mul_naive | 0.03 | --- | --- |
VC for double_block | 0.12 | --- | --- |
VC for padding | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 0.03 | --- | --- |
2. precondition | 0.02 | --- | --- |
3. precondition | 0.03 | --- | --- |
4. precondition | 0.03 | --- | --- |
5. precondition | 0.02 | --- | --- |
6. assertion | --- | --- | 0.62 |
7. assertion | --- | --- | 0.72 |
8. assertion | --- | --- | 0.14 |
9. postcondition | 0.05 | --- | --- |
10. postcondition | 0.04 | --- | --- |
11. postcondition | 0.06 | --- | --- |
12. postcondition | 0.10 | --- | --- |
13. postcondition | 0.06 | --- | --- |
VC for strassen | Timeout (5s) | --- | --- |
split_goal_wp | | | |
| 1. VC for strassen | 0.02 | --- | --- |
2. assertion | 0.04 | --- | --- |
3. precondition | 0.02 | --- | --- |
4. postcondition | 0.02 | --- | --- |
5. postcondition | 0.04 | --- | --- |
6. VC for strassen | 0.08 | --- | --- |
7. precondition | 0.04 | --- | --- |
8. precondition | 0.04 | --- | --- |
9. precondition | 0.04 | --- | --- |
10. precondition | 0.02 | --- | --- |
11. assertion | 0.04 | --- | --- |
12. variant decrease | 0.06 | --- | --- |
13. precondition | 0.05 | --- | --- |
14. precondition | 0.04 | --- | --- |
15. precondition | 0.05 | --- | --- |
16. precondition | 0.05 | --- | --- |
17. precondition | 0.04 | --- | --- |
18. precondition | 0.05 | --- | --- |
19. precondition | 0.04 | --- | --- |
20. precondition | 0.06 | --- | --- |
21. precondition | 0.05 | --- | --- |
22. precondition | 0.06 | --- | --- |
23. precondition | 0.04 | --- | --- |
24. precondition | 0.04 | --- | --- |
25. precondition | 0.05 | --- | --- |
26. precondition | 0.05 | --- | --- |
27. precondition | 0.06 | --- | --- |
28. precondition | 0.07 | --- | --- |
29. precondition | 0.06 | --- | --- |
30. precondition | 0.06 | --- | --- |
31. precondition | 0.07 | --- | --- |
32. assertion | 0.09 | --- | --- |
33. assertion | 0.10 | --- | --- |
34. precondition | 0.08 | --- | --- |
35. precondition | 0.07 | --- | --- |
36. postcondition | --- | 0.38 | --- |
37. postcondition | 0.07 | --- | --- |
38. precondition | 0.04 | --- | --- |
39. precondition | 0.04 | --- | --- |
40. precondition | 0.04 | --- | --- |
41. precondition | 0.04 | --- | --- |
42. precondition | 0.04 | --- | --- |
43. precondition | 0.05 | --- | --- |
44. precondition | 0.05 | --- | --- |
45. precondition | 0.06 | --- | --- |
46. precondition | 0.04 | --- | --- |
47. variant decrease | 0.08 | --- | --- |
48. precondition | 0.10 | --- | --- |
49. precondition | 0.10 | --- | --- |
50. precondition | 0.08 | --- | --- |
51. precondition | 0.10 | --- | --- |
52. precondition | 0.09 | --- | --- |
53. postcondition | 0.17 | --- | --- |
54. postcondition | 0.08 | --- | --- |
55. postcondition | 0.05 | --- | --- |
56. precondition | 0.06 | --- | --- |
57. precondition | 0.06 | --- | --- |
58. precondition | 0.08 | --- | --- |
59. precondition | 0.09 | --- | --- |
60. precondition | 0.09 | --- | --- |
61. precondition | 0.10 | --- | --- |
62. precondition | 0.12 | --- | --- |
63. precondition | 0.11 | --- | --- |
64. precondition | 0.13 | --- | --- |
65. precondition | 0.14 | --- | --- |
66. precondition | 0.12 | --- | --- |
67. precondition | 0.11 | --- | --- |
68. precondition | 0.14 | --- | --- |
69. precondition | 0.14 | --- | --- |
70. precondition | 0.14 | --- | --- |
71. precondition | 0.13 | --- | --- |
72. precondition | 0.14 | --- | --- |
73. precondition | 0.13 | --- | --- |
74. precondition | 0.14 | --- | --- |
75. precondition | 0.13 | --- | --- |
76. precondition | 0.15 | --- | --- |
77. precondition | 0.15 | --- | --- |
78. precondition | 0.15 | --- | --- |
79. precondition | 0.14 | --- | --- |
80. assertion | 0.20 | --- | --- |
81. assertion | 0.20 | --- | --- |
82. precondition | 0.11 | --- | --- |
83. precondition | 0.14 | --- | --- |
84. precondition | 0.17 | --- | --- |
85. precondition | 0.17 | --- | --- |
86. precondition | 0.19 | --- | --- |
87. precondition | 0.19 | --- | --- |
88. precondition | 0.14 | --- | --- |
89. precondition | 0.19 | --- | --- |
90. precondition | 0.22 | --- | --- |
91. precondition | 0.22 | --- | --- |
92. precondition | 0.17 | --- | --- |
93. precondition | 0.21 | --- | --- |
94. precondition | 0.21 | --- | --- |
95. precondition | 0.22 | --- | --- |
96. precondition | 0.18 | --- | --- |
97. precondition | 0.21 | --- | --- |
98. precondition | 0.22 | --- | --- |
99. precondition | 0.22 | --- | --- |
100. precondition | 0.22 | --- | --- |
101. precondition | 0.18 | --- | --- |
102. precondition | 0.22 | --- | --- |
103. precondition | 0.22 | --- | --- |
104. precondition | 0.25 | --- | --- |
105. precondition | 0.24 | --- | --- |
106. assertion | 0.35 | --- | --- |
107. assertion | 0.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. precondition | 0.10 | --- | --- |
109. precondition | 0.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. precondition | 0.12 | --- | --- |
111. precondition | 0.30 | --- | --- |
112. precondition | 0.28 | --- | --- |
113. precondition | 0.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. precondition | 0.17 | --- | --- |
115. precondition | 0.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. precondition | 0.17 | --- | --- |
117. precondition | 0.44 | --- | --- |
118. precondition | 0.47 | --- | --- |
119. precondition | 0.28 | --- | --- |
120. precondition | 0.28 | --- | --- |
121. precondition | 0.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. precondition | 0.16 | --- | --- |
123. precondition | 0.63 | --- | --- |
124. precondition | 0.52 | --- | --- |
125. precondition | 0.31 | --- | --- |
126. precondition | 0.33 | --- | --- |
127. precondition | 0.50 | --- | --- |
128. precondition | 0.32 | --- | --- |
129. precondition | 0.58 | --- | --- |
130. precondition | 0.64 | --- | --- |
131. precondition | 0.34 | --- | --- |
132. assertion | --- | 0.61 | --- |
133. assertion | --- | 0.59 | --- |
134. precondition | 0.64 | --- | --- |
135. precondition | 0.34 | --- | --- |
136. precondition | 0.67 | --- | --- |
137. precondition | 0.36 | --- | --- |
138. precondition | 0.37 | --- | --- |
139. precondition | 1.41 | --- | --- |
140. precondition | 0.75 | --- | --- |
141. precondition | 0.40 | --- | --- |
142. precondition | 0.39 | --- | --- |
143. precondition | 0.83 | --- | --- |
144. precondition | 0.86 | --- | --- |
145. precondition | 0.44 | --- | --- |
146. precondition | 0.45 | --- | --- |
147. precondition | 1.72 | --- | --- |
148. precondition | 0.87 | --- | --- |
149. precondition | 0.45 | --- | --- |
150. precondition | 0.41 | --- | --- |
151. precondition | 1.91 | --- | --- |
152. precondition | 0.77 | --- | --- |
153. precondition | 0.46 | --- | --- |
154. precondition | 0.49 | --- | --- |
155. precondition | 0.92 | --- | --- |
156. precondition | 1.06 | --- | --- |
157. precondition | 0.52 | --- | --- |
158. precondition | 1.06 | --- | --- |
159. precondition | 0.54 | --- | --- |
160. precondition | 0.55 | --- | --- |
161. precondition | 2.35 | --- | --- |
162. precondition | 1.12 | --- | --- |
163. precondition | 0.53 | --- | --- |
164. precondition | 1.03 | --- | --- |
165. precondition | 0.55 | --- | --- |
166. precondition | 0.58 | --- | --- |
167. precondition | 2.90 | --- | --- |
168. precondition | 1.24 | --- | --- |
169. precondition | 0.58 | --- | --- |
170. precondition | 1.10 | --- | --- |
171. precondition | 0.60 | --- | --- |
172. precondition | 1.34 | --- | --- |
173. precondition | 0.63 | --- | --- |
174. precondition | 1.31 | --- | --- |
175. precondition | 0.69 | --- | --- |
176. precondition | 1.64 | --- | --- |
177. precondition | 0.69 | --- | --- |
178. precondition | 1.26 | --- | --- |
179. precondition | 0.70 | --- | --- |
180. precondition | 1.41 | --- | --- |
181. precondition | 0.69 | --- | --- |
182. precondition | 1.28 | --- | --- |
183. precondition | 0.60 | --- | --- |
184. assertion | --- | --- | --- |
compute_specified | | | |
| 1. assertion | --- | --- | --- |
simplify_trivial_quantification_in_goal | | | |
| 1. assertion | --- | --- | --- |
compute_specified | | | |
| 185. VC for strassen | 3.22 | --- | --- |
186. precondition | 0.06 | --- | --- |
187. precondition | 0.53 | --- | --- |
188. precondition | 0.52 | --- | --- |
189. precondition | 0.54 | --- | --- |
190. precondition | 0.54 | --- | --- |
191. precondition | 0.62 | --- | --- |
192. precondition | 0.60 | --- | --- |
193. precondition | 0.07 | --- | --- |
194. precondition | 0.58 | --- | --- |
195. precondition | 0.69 | --- | --- |
196. precondition | 0.66 | --- | --- |
197. precondition | 0.69 | --- | --- |
198. precondition | 0.08 | --- | --- |
199. precondition | 0.77 | --- | --- |
200. precondition | 0.64 | --- | --- |
201. precondition | 0.06 | --- | --- |
202. precondition | 0.06 | --- | --- |
203. assertion | --- | --- | --- |
split_goal_wp | | | |
| 1. VC for strassen | 11.91 | --- | --- |
2. VC for strassen | 2.22 | --- | --- |
3. VC for strassen | 7.21 | --- | --- |
4. VC for strassen | 4.28 | --- | --- |
5. VC for strassen | 10.58 | --- | --- |
6. VC for strassen | 0.51 | --- | --- |
204. postcondition | 0.12 | --- | --- |
205. postcondition | 0.07 | --- | --- |