Obligations | Alt-Ergo (2.2.0) | CVC4 (1.5) | 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.11 | --- | --- | --- | --- |
list_assoc_cons | --- | 0.08 | --- | --- | --- | --- |
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 | --- | 0.34 | --- | --- | --- | --- |
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.12 | --- | --- | --- | --- |
simplelist_split | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| simplelist_split.1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| simplelist_split.1.1 | --- | 0.09 | --- | --- | --- | --- |
simplelist_split.1.2 | --- | 0.10 | --- | --- | --- | --- |
simplelist_split.1.3 | --- | 0.79 | --- | --- | --- | --- |
simplelist_split.1.4 | --- | 0.57 | --- | --- | --- | --- |
simplelist_hd_max_rank | 0.02 | --- | --- | --- | --- | --- |
rank_before_suffix | 0.18 | --- | --- | --- | --- | --- |
inter_com | --- | 0.05 | --- | --- | --- | --- |
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 | --- | --- | --- | --- | --- |
union_sym | 0.01 | --- | --- | --- | --- | --- |
union_var1 | 0.01 | --- | --- | --- | --- | --- |
union_var2 | 0.01 | --- | --- | --- | --- | --- |
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.62 | --- | --- | --- | --- |
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 | --- | --- | --- | --- | 3.24 | --- |
elt_set_of | --- | --- | --- | 0.17 | --- | --- |
subset_set_of | 0.04 | --- | --- | --- | --- | --- |
reachable_refl | Timeout (45s) | Timeout (45s) | --- | 0.03 | --- | Timeout (45s) |
reachable_trans | --- | 0.07 | --- | --- | --- | --- |
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.27 | --- | --- | --- | --- |
subscc_after_last_gray | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| subscc_after_last_gray.1 | --- | 0.57 | --- | --- | --- | --- |
subscc_after_last_gray.2 | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| subscc_after_last_gray.2.1 | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| subscc_after_last_gray.2.1.1 | --- | 10.58 | --- | --- | --- | --- |
subscc_after_last_gray.3 | --- | 1.36 | --- | --- | --- | --- |
subscc_after_last_gray.4 | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| subscc_after_last_gray.4.1 | --- | --- | --- | 2.73 | --- | --- |
wf_color_postcond_split | --- | 0.30 | --- | --- | --- | --- |
wf_color_sccs | --- | 0.31 | --- | --- | --- | --- |
wf_color_3_cases | --- | 0.16 | --- | --- | --- | --- |
rank_lmem | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| rank_lmem.1 | --- | 0.62 | --- | --- | --- | --- |
rank_lmem.2 | 0.02 | --- | --- | --- | --- | --- |
rank_lmem.3 | 0.02 | --- | --- | --- | --- | --- |
rank_lmem.4 | --- | --- | --- | 0.20 | --- | --- |
rank_inj | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | |
| rank_inj.1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| rank_inj.1.1 | 0.04 | --- | --- | --- | --- | --- |
rank_inj.1.2 | 0.02 | --- | --- | --- | --- | --- |
num_lmem | --- | 4.29 | --- | --- | --- | --- |
num_inj | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| num_inj.1 | --- | 0.12 | --- | --- | --- | --- |
num_rank1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| num_rank1.1 | 0.02 | 0.09 | --- | --- | --- | --- |
num_rank | --- | 0.21 | --- | --- | --- | --- |
num_rank2 | 0.02 | --- | --- | --- | --- | --- |
50. VC for split | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. postcondition | 0.01 | --- | --- | --- | --- | --- |
2. postcondition | 0.01 | --- | --- | --- | --- | --- |
3. postcondition | 0.01 | --- | --- | --- | --- | --- |
4. postcondition | --- | 0.17 | --- | --- | --- | --- |
5. postcondition | 0.01 | --- | --- | --- | --- | --- |
6. postcondition | 0.05 | --- | --- | --- | --- | --- |
51. VC for add_stack_incr | 0.01 | --- | --- | --- | --- | --- |
52. VC for add_blacks | 0.01 | --- | --- | --- | --- | --- |
53. VC for set_infty | 0.03 | --- | --- | --- | --- | --- |
54. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. precondition | 0.03 | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. precondition | --- | --- | --- | 1.09 | --- | --- |
3. precondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. precondition | 0.42 | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. precondition | --- | 0.68 | --- | --- | --- | --- |
2. precondition | 0.10 | --- | --- | --- | --- | --- |
3. precondition | 0.66 | --- | --- | --- | --- | --- |
4. precondition | 0.13 | --- | --- | --- | --- | --- |
5. precondition | 0.22 | --- | --- | --- | --- | --- |
6. precondition | 0.22 | --- | --- | --- | --- | --- |
7. precondition | --- | 0.45 | --- | --- | --- | --- |
8. precondition | --- | 0.42 | --- | --- | --- | --- |
9. precondition | --- | 0.36 | --- | --- | --- | --- |
3. precondition | 0.05 | --- | --- | --- | --- | --- |
4. precondition | 0.14 | --- | --- | --- | --- | --- |
5. precondition | --- | 19.76 | --- | --- | --- | --- |
6. precondition | --- | 17.86 | 0.93 | --- | --- | --- |
7. precondition | 0.03 | --- | --- | --- | --- | --- |
8. precondition | 0.03 | --- | --- | --- | --- | --- |
9. precondition | 0.03 | --- | --- | --- | --- | --- |
4. assertion | --- | --- | 0.85 | --- | --- | --- |
5. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | --- | 4.40 | --- | --- | --- | --- |
2. VC for dfs1 | --- | 12.62 | --- | --- | --- | --- |
3. VC for dfs1 | 2.49 | --- | --- | --- | --- | --- |
4. VC for dfs1 | 0.07 | --- | --- | --- | --- | --- |
5. VC for dfs1 | 0.85 | --- | --- | --- | --- | --- |
6. VC for dfs1 | --- | 4.13 | --- | --- | --- | --- |
7. VC for dfs1 | --- | 0.84 | --- | --- | --- | --- |
8. VC for dfs1 | --- | 0.15 | --- | --- | --- | --- |
9. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. VC for dfs1 | --- | 12.95 | --- | --- | --- | --- |
10. VC for dfs1 | --- | --- | 0.74 | --- | --- | --- |
11. VC for dfs1 | 0.25 | --- | --- | --- | --- | --- |
12. VC for dfs1 | 0.05 | --- | --- | --- | --- | --- |
13. VC for dfs1 | 0.28 | --- | --- | --- | --- | --- |
14. VC for dfs1 | 1.28 | --- | --- | --- | --- | --- |
6. postcondition | 0.01 | --- | --- | --- | --- | --- |
7. postcondition | 0.14 | --- | --- | --- | --- | --- |
8. postcondition | --- | 0.97 | --- | --- | --- | --- |
9. postcondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. postcondition | 7.63 | --- | --- | --- | --- | --- |
10. assertion | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | 0.08 | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.24 | --- | --- | --- | --- | --- |
3. VC for dfs1 | 2.17 | --- | --- | --- | --- | --- |
11. assertion | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. assertion | --- | 0.23 | --- | --- | --- | --- |
12. assertion | --- | --- | 1.12 | --- | --- | --- |
13. assertion | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | --- | 1.18 | --- | --- | --- | --- |
2. VC for dfs1 | 0.17 | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | --- | --- | 6.72 | --- | --- |
14. assertion | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | 0.86 | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.04 | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.02 | --- | --- | --- | --- | --- |
15. postcondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | 0.84 | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | --- | --- | 15.14 | --- | --- |
3. VC for dfs1 | 26.79 | 2.03 | --- | --- | --- | --- |
4. VC for dfs1 | 2.30 | --- | --- | --- | --- | --- |
2. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs1 | 5.24 | --- | --- | --- | --- | --- |
2. VC for dfs1 | 0.84 | --- | --- | --- | --- | --- |
3. VC for dfs1 | 0.94 | --- | --- | --- | --- | --- |
4. VC for dfs1 | 0.99 | --- | --- | --- | --- | --- |
5. VC for dfs1 | --- | 6.70 | --- | --- | --- | --- |
6. VC for dfs1 | 1.10 | --- | --- | --- | --- | --- |
7. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. VC for dfs1 | 4.23 | --- | --- | --- | --- | --- |
8. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. VC for dfs1 | 4.29 | --- | --- | --- | --- | --- |
9. VC for dfs1 | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. VC for dfs1 | 4.33 | --- | --- | --- | --- | --- |
3. postcondition | 4.45 | --- | --- | --- | --- | --- |
4. postcondition | 0.03 | --- | --- | --- | --- | --- |
5. postcondition | --- | 13.86 | --- | --- | --- | --- |
6. postcondition | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- |
inline_all | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | 27.97 | --- | --- |
7. postcondition | 0.99 | 3.27 | --- | --- | --- | --- |
8. postcondition | 0.31 | --- | --- | --- | --- | --- |
9. postcondition | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | 15.95 | --- | --- |
10. postcondition | --- | --- | --- | 0.14 | --- | --- |
11. postcondition | 0.10 | 0.51 | --- | 29.81 | --- | --- |
12. postcondition | 0.10 | 0.51 | --- | 24.90 | --- | --- |
13. postcondition | --- | 15.14 | --- | --- | --- | --- |
14. postcondition | 0.04 | --- | --- | --- | --- | --- |
16. postcondition | 0.02 | --- | --- | --- | --- | --- |
17. postcondition | 0.18 | --- | --- | --- | --- | --- |
18. postcondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. postcondition | 0.01 | --- | --- | --- | --- | --- |
19. postcondition | 0.03 | --- | --- | --- | --- | --- |
55. VC for dfs | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
2. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
3. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
4. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
5. VC for dfs | 0.05 | --- | --- | --- | --- | --- |
6. VC for dfs | 0.25 | --- | --- | --- | --- | --- |
7. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
8. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
9. VC for dfs | 0.03 | --- | --- | --- | --- | --- |
10. VC for dfs | --- | 0.14 | --- | --- | --- | --- |
11. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
12. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
13. VC for dfs | 0.01 | --- | --- | --- | --- | --- |
14. VC for dfs | 0.02 | --- | --- | --- | --- | --- |
2. postcondition | 0.02 | --- | --- | --- | --- | --- |
3. postcondition | 0.02 | --- | --- | --- | --- | --- |
4. postcondition | 0.02 | --- | --- | --- | --- | --- |
5. postcondition | 0.02 | --- | --- | --- | --- | --- |
6. assertion | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
2. VC for dfs | --- | --- | --- | --- | --- | 0.06 |
7. precondition | 0.02 | --- | --- | --- | --- | --- |
8. precondition | 0.02 | --- | --- | --- | --- | --- |
9. precondition | 0.02 | --- | --- | --- | --- | --- |
10. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs | 0.03 | --- | --- | --- | --- | --- |
2. VC for dfs | 0.03 | --- | --- | --- | --- | --- |
3. VC for dfs | 0.03 | --- | --- | --- | --- | --- |
4. VC for dfs | 0.03 | --- | --- | --- | --- | --- |
5. VC for dfs | 0.14 | --- | --- | --- | --- | --- |
6. VC for dfs | 0.63 | --- | --- | --- | --- | --- |
7. VC for dfs | 0.06 | --- | --- | --- | --- | --- |
8. VC for dfs | 0.06 | --- | --- | --- | --- | --- |
9. VC for dfs | 0.06 | --- | --- | --- | --- | --- |
10. VC for dfs | --- | --- | --- | --- | --- | 0.05 |
11. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
12. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
13. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
14. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
11. postcondition | 0.45 | --- | --- | --- | --- | --- |
12. postcondition | --- | 1.50 | --- | --- | --- | --- |
13. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs | 1.00 | --- | --- | --- | --- | --- |
14. postcondition | 0.02 | --- | --- | --- | --- | --- |
15. precondition | 0.02 | --- | --- | --- | --- | --- |
16. precondition | 0.02 | --- | --- | --- | --- | --- |
17. precondition | 0.03 | --- | --- | --- | --- | --- |
18. precondition | 0.02 | --- | --- | --- | --- | --- |
19. precondition | 0.02 | --- | --- | --- | --- | --- |
20. precondition | 0.04 | --- | --- | --- | --- | --- |
21. precondition | 0.02 | --- | --- | --- | --- | --- |
22. postcondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. postcondition | 0.02 | --- | --- | --- | --- | --- |
2. postcondition | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- |
inline_all | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | 0.20 |
2. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
3. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
4. VC for dfs | 0.21 | --- | --- | --- | --- | --- |
5. VC for dfs | 0.04 | --- | --- | --- | --- | --- |
23. postcondition | 0.10 | --- | --- | --- | --- | --- |
24. postcondition | --- | 2.85 | --- | --- | --- | --- |
25. postcondition | 0.66 | --- | --- | --- | --- | --- |
26. postcondition | --- | 4.57 | --- | --- | --- | --- |
56. VC for tarjan | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. precondition | 0.01 | --- | --- | --- | --- | --- |
2. precondition | 0.01 | --- | --- | --- | --- | --- |
3. precondition | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. precondition | 0.05 | --- | --- | --- | --- | --- |
2. precondition | 0.04 | --- | --- | --- | --- | --- |
3. precondition | 0.01 | --- | --- | --- | --- | --- |
4. precondition | 0.01 | --- | --- | --- | --- | --- |
5. precondition | 0.01 | --- | --- | --- | --- | --- |
6. precondition | 0.01 | --- | --- | --- | --- | --- |
7. precondition | 0.02 | --- | --- | --- | --- | --- |
8. precondition | 0.02 | --- | --- | --- | --- | --- |
9. precondition | 0.02 | --- | --- | --- | --- | --- |
4. assertion | 0.15 | --- | --- | --- | --- | --- |
5. postcondition | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | |
| 1. postcondition | 0.36 | --- | --- | --- | --- | --- |
2. postcondition | 0.02 | --- | --- | --- | --- | --- |
3. postcondition | 0.15 | --- | --- | --- | --- | --- |