Obligations | Alt-Ergo (2.2.0) | CVC3 (2.4.1) | CVC4 (1.5) | CVC4 (1.5-prerelease) | Coq (8.7.2) | Eprover (1.9) | Spass (3.5) | Z3 (4.6.2) |
lmem_dec | 0.00 | --- | --- | --- | --- | --- | --- | --- |
list_simpl_r | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| list_simpl_r.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| list_simpl_r.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
list_simpl_r.1.2 | --- | --- | --- | 0.08 | --- | --- | --- | --- |
list_assoc_cons | --- | --- | --- | 0.06 | --- | --- | --- | --- |
rank_not_mem | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| rank_not_mem.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| rank_not_mem.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_not_mem.1.2 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_range | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| rank_range.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| rank_range.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_range.1.2 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_range.1.3 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_range.1.4 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_min | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| rank_min.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| rank_min.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_min.1.2 | --- | --- | --- | 2.32 | --- | --- | --- | --- |
rank_app_l | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| rank_app_l.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| rank_app_l.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_app_l.1.2 | 0.10 | --- | --- | --- | --- | --- | --- | --- |
rank_app_r | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| rank_app_r.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| rank_app_r.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
rank_app_r.1.2 | 0.04 | --- | --- | --- | --- | --- | --- | --- |
simplelist_tl | --- | --- | --- | 0.10 | --- | --- | --- | --- |
simplelist_split | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_split.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_split.1.1 | --- | --- | 0.10 | --- | --- | --- | --- | --- |
simplelist_split.1.2 | --- | --- | 0.11 | --- | --- | --- | --- | --- |
simplelist_split.1.3 | --- | --- | --- | 0.64 | --- | --- | --- | --- |
simplelist_split.1.4 | --- | --- | --- | 0.57 | --- | --- | --- | --- |
simplelist_hd_max_rank | 0.02 | --- | --- | --- | --- | --- | --- | --- |
rank_before_suffix | 0.18 | --- | --- | --- | --- | --- | --- | --- |
inter_com | --- | 0.04 | --- | --- | --- | --- | --- | --- |
inter_add | 0.03 | --- | --- | --- | --- | --- | --- | --- |
set_elt | 0.04 | --- | --- | --- | --- | --- | --- | --- |
set_mem | --- | --- | --- | --- | --- | 0.03 | --- | --- |
inter_subset_inter | --- | --- | --- | --- | --- | 0.15 | --- | --- |
subset_add | 0.04 | --- | --- | --- | --- | --- | --- | --- |
union_add_l | 0.01 | --- | --- | --- | --- | --- | --- | --- |
union_add_r | 0.01 | --- | --- | --- | --- | --- | --- | --- |
elts_cons | 0.03 | --- | --- | --- | --- | --- | --- | --- |
elts_app | 0.02 | --- | --- | --- | --- | --- | --- | --- |
simplelist_app_inter | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_app_inter.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_app_inter.1.1 | --- | --- | --- | --- | --- | 0.06 | --- | --- |
simplelist_app_inter.1.2 | --- | --- | 1.41 | --- | --- | --- | --- | --- |
simplelist_length | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_length.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_length.1.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
simplelist_length.1.2 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
set_of_elt | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| set_of_elt.1 | 0.02 | --- | --- | --- | --- | --- | --- | --- |
set_of_elt.2 | --- | --- | --- | --- | --- | --- | 0.73 | --- |
elt_set_of | --- | --- | --- | --- | --- | 0.34 | --- | --- |
subset_set_of | 0.04 | --- | --- | --- | --- | --- | --- | --- |
reachable_trans | --- | 0.19 | --- | --- | --- | --- | --- | --- |
xset_path_xedge | --- | --- | --- | --- | --- | --- | --- | --- |
induction_pr | | | | | | | | |
| xset_path_xedge.1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
xset_path_xedge.2 | --- | --- | --- | --- | --- | 0.04 | --- | --- |
same_scc_refl | --- | --- | --- | --- | --- | 0.07 | --- | --- |
same_scc_sym | 0.01 | --- | --- | --- | --- | --- | --- | --- |
same_scc_trans | 0.02 | --- | --- | --- | --- | --- | --- | --- |
subscc_add | 0.04 | --- | --- | --- | --- | --- | --- | --- |
scc_max | --- | --- | --- | 0.22 | --- | --- | --- | --- |
subscc_after_last_gray | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| subscc_after_last_gray.1 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| subscc_after_last_gray.1.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| subscc_after_last_gray.1.1.1 | 0.16 | --- | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.1.1.2 | 0.06 | --- | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.2 | 2.58 | --- | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.3 | --- | --- | --- | 1.08 | --- | --- | --- | --- |
subscc_after_last_gray.4 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| subscc_after_last_gray.4.1 | --- | --- | --- | --- | --- | 0.14 | --- | --- |
wf_color_postcond_split | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| wf_color_postcond_split.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| wf_color_postcond_split.1.1 | --- | --- | --- | --- | --- | 0.09 | --- | --- |
wf_color_postcond_split.1.2 | --- | --- | --- | --- | --- | 2.11 | --- | --- |
wf_color_sccs | --- | --- | --- | 0.76 | --- | --- | --- | --- |
wf_color_3_cases | --- | --- | --- | 0.17 | --- | --- | --- | --- |
39. VC for split | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
4. postcondition | --- | 0.34 | --- | --- | --- | --- | --- | --- |
5. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
6. postcondition | 0.07 | --- | --- | --- | --- | --- | --- | --- |
40. VC for add_stack_incr | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. index in array bounds | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. type invariant | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
41. VC for add_blacks | 0.01 | --- | --- | --- | --- | --- | --- | --- |
42. VC for set_max_int | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | --- | 0.50 | --- | --- | --- | --- | --- | --- |
3. index in array bounds | --- | 2.27 | --- | --- | --- | --- | --- | --- |
4. postcondition | 0.04 | --- | --- | --- | --- | --- | --- | --- |
5. postcondition | 0.04 | --- | --- | --- | --- | --- | --- | --- |
43. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. assertion | --- | --- | --- | 30.87 | --- | --- | --- | --- |
2. index in array bounds | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. type invariant | 0.01 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
5. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | 0.85 | --- | --- |
6. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | 0.26 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | 0.18 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | 0.08 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.09 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | 0.04 | --- | --- | --- | --- | --- | --- | --- |
5. precondition | 0.12 | --- | --- | --- | --- | --- | --- | --- |
6. precondition | 0.10 | --- | --- | --- | --- | --- | --- | --- |
7. precondition | 0.51 | --- | --- | --- | --- | --- | --- | --- |
8. precondition | 0.49 | --- | --- | --- | --- | --- | --- | --- |
9. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.03 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | 0.08 | --- | --- | --- | --- | --- | --- | --- |
5. precondition | 0.89 | --- | --- | --- | --- | --- | --- | --- |
6. precondition | --- | --- | --- | --- | 0.89 | --- | --- | --- |
7. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
8. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | 0.12 | --- | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.13 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | 1.80 | --- | --- | --- | --- | --- | --- | --- |
9. assertion | --- | --- | --- | --- | --- | 2.24 | --- | --- |
10. assertion | --- | --- | --- | --- | 1.03 | --- | --- | --- |
11. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.31 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 4.50 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | 0.80 | --- | --- | 0.46 | --- | --- | --- | --- |
4. postcondition | 0.68 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.04 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.27 | --- | --- | 1.59 | --- | --- | --- | --- |
3. postcondition | 0.06 | --- | --- | --- | --- | --- | --- | --- |
4. postcondition | 0.03 | --- | --- | 0.58 | --- | --- | --- | --- |
5. postcondition | 0.28 | --- | --- | 1.51 | --- | --- | --- | --- |
6. postcondition | 0.28 | --- | --- | 0.98 | --- | --- | --- | --- |
7. postcondition | 0.07 | --- | --- | --- | --- | --- | --- | --- |
8. postcondition | 0.04 | --- | --- | --- | --- | --- | --- | --- |
9. postcondition | 0.03 | --- | --- | 0.26 | --- | --- | --- | --- |
3. postcondition | --- | --- | --- | 2.30 | --- | --- | --- | --- |
4. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
5. postcondition | 0.55 | --- | --- | 0.24 | --- | --- | --- | --- |
6. postcondition | --- | --- | --- | 3.60 | --- | --- | --- | --- |
12. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.46 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | --- | --- | 11.70 | --- | --- | --- | --- |
13. postcondition | 0.58 | --- | --- | --- | --- | --- | --- | --- |
14. postcondition | --- | --- | 3.32 | --- | --- | --- | --- | --- |
15. postcondition | 24.15 | --- | --- | --- | --- | --- | --- | --- |
16. postcondition | 0.02 | --- | --- | 0.13 | --- | 0.06 | --- | --- |
17. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | 2.64 | --- | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.64 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | 0.02 | --- | --- | --- | --- | --- | --- | --- |
4. VC for dfs1 | 0.45 | --- | --- | --- | --- | --- | --- | --- |
18. assertion | --- | --- | --- | --- | 1.25 | --- | --- | --- |
19. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | --- | 0.35 | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.03 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | --- | --- | --- | --- | 4.00 | --- | --- |
20. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | 1.47 | --- | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.02 | --- | --- | --- | --- | --- | --- | --- |
21. assertion | 0.01 | --- | --- | --- | --- | --- | --- | --- |
22. assertion | --- | --- | --- | --- | --- | --- | --- | 1.40 |
23. precondition | 0.28 | --- | --- | --- | --- | --- | --- | --- |
24. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. assertion | 0.02 | --- | --- | --- | --- | --- | --- | --- |
2. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | 31.64 |
25. type invariant | 0.01 | --- | --- | --- | --- | --- | --- | --- |
26. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.28 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 1.19 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | --- | --- | 15.48 | --- | --- | --- | --- |
4. postcondition | 1.17 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | --- | --- | --- | 1.80 | --- | --- | --- | --- |
2. postcondition | 0.19 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | --- | --- | 2.11 | --- | --- | --- | --- |
4. postcondition | --- | --- | --- | 2.66 | --- | --- | --- | --- |
5. postcondition | --- | --- | --- | 2.31 | --- | --- | --- | --- |
6. postcondition | --- | --- | --- | 6.63 | --- | --- | --- | --- |
7. postcondition | 0.21 | --- | --- | --- | --- | --- | --- | --- |
8. postcondition | 0.20 | --- | --- | --- | --- | --- | --- | --- |
9. postcondition | 0.03 | --- | --- | 0.30 | --- | --- | --- | --- |
3. postcondition | 2.07 | --- | --- | 1.28 | --- | --- | --- | --- |
4. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
5. postcondition | 0.03 | --- | --- | 0.23 | --- | --- | --- | --- |
6. postcondition | 0.10 | --- | --- | 0.41 | --- | --- | --- | --- |
27. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.51 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.03 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | --- | --- | --- | --- | 12.35 | --- | --- |
28. postcondition | 0.28 | --- | --- | 0.29 | --- | 0.24 | --- | --- |
29. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | 0.08 | --- | --- | --- | --- |
30. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | 0.05 | --- | --- | 0.22 | --- | --- | --- | --- |
31. postcondition | 0.02 | --- | --- | 0.13 | --- | 0.16 | --- | --- |
32. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | 0.14 | --- | --- |
2. VC for dfs1 | 0.29 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | 0.02 | --- | --- | --- | --- | --- | --- | --- |
4. VC for dfs1 | --- | --- | --- | 0.24 | --- | --- | --- | --- |
44. VC for dfs' | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
4. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
5. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
6. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
7. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs' | --- | 0.23 | --- | --- | --- | --- | --- | --- |
2. VC for dfs' | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs' | 0.01 | --- | --- | --- | --- | --- | --- | --- |
4. VC for dfs' | 0.01 | --- | --- | --- | --- | --- | --- | --- |
8. assertion | 2.26 | --- | --- | --- | --- | --- | --- | --- |
9. index in array bounds | 0.02 | --- | --- | --- | --- | --- | --- | --- |
10. index in array bounds | 0.01 | --- | --- | --- | --- | --- | --- | --- |
11. assertion | 0.06 | --- | --- | --- | --- | --- | --- | --- |
12. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
13. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
14. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
15. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
16. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
17. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
18. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | 15.42 | --- | 0.69 | --- | --- | --- | --- |
19. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | 16.71 | --- | --- | --- | --- | --- | --- |
20. postcondition | --- | --- | --- | 0.18 | --- | --- | --- | --- |
21. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | 0.33 | --- | --- | --- | --- | --- | --- | --- |
22. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
23. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
24. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
25. precondition | 0.03 | --- | --- | --- | --- | --- | --- | --- |
26. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
27. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
28. assertion | --- | --- | --- | --- | --- | --- | --- | 0.37 |
29. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
30. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
31. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
32. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
33. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
34. postcondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
35. postcondition | 1.02 | --- | --- | --- | --- | --- | --- | --- |
36. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | 0.24 | --- | --- | --- | --- |
37. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | 0.51 | --- | --- | --- | --- | --- | --- | --- |
38. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
39. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs' | --- | --- | --- | --- | --- | --- | --- | 0.30 |
2. VC for dfs' | 0.02 | --- | --- | --- | --- | --- | --- | --- |
3. VC for dfs' | 0.02 | --- | --- | --- | --- | --- | --- | --- |
4. VC for dfs' | 0.04 | --- | --- | --- | --- | --- | --- | --- |
45. VC for tarjan | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. array creation size | 0.01 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | 0.05 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
2. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | 0.02 | --- | --- | 0.13 | --- | --- | --- | --- |
5. precondition | 0.02 | --- | --- | 0.14 | --- | --- | --- | --- |
6. precondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
7. precondition | 0.02 | --- | --- | 0.12 | --- | --- | --- | --- |
8. precondition | 0.02 | --- | --- | 0.13 | --- | --- | --- | --- |
9. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
3. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
4. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
5. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
6. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
5. precondition | 0.01 | --- | --- | --- | --- | --- | --- | --- |
6. assertion | 0.02 | --- | --- | --- | --- | --- | --- | --- |
7. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | 0.29 | --- | --- | --- | --- | --- | --- | --- |
2. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |
3. postcondition | 0.02 | --- | --- | --- | --- | --- | --- | --- |