Obligations | Alt-Ergo (2.2.0) | Alt-Ergo (2.3.0) | CVC4 (1.5) | Coq (8.7.2) | Eprover (1.9) | Spass (3.5) | Z3 (4.4.0) | Z3 (4.6.3) |
lmem_dec | --- | 0.00 | --- | --- | --- | --- | --- | --- |
inter_com | --- | --- | 0.05 | --- | --- | --- | --- | --- |
inter_add_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
inter_not_add_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
diff_add_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
diff_not_add_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
subset_add_r | --- | 0.01 | --- | --- | --- | --- | --- | --- |
union_add_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
union_add_r | --- | 0.01 | --- | --- | --- | --- | --- | --- |
union_com | --- | 0.01 | --- | --- | --- | --- | --- | --- |
union_var_l | --- | 0.01 | --- | --- | --- | --- | --- | --- |
union_var_r | --- | 0.01 | --- | --- | --- | --- | --- | --- |
set_of_elt | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| set_of_elt.1 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
set_of_elt.2 | --- | --- | --- | --- | --- | 4.58 | --- | --- |
elt_set_of | --- | --- | --- | --- | 0.36 | --- | --- | --- |
subset_set_of | --- | 1.35 | --- | --- | --- | --- | --- | --- |
elts_cons | --- | 0.03 | --- | --- | --- | --- | --- | --- |
elts_app | --- | 0.02 | --- | --- | --- | --- | --- | --- |
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.40 | --- | --- | --- | --- | --- |
snoc_app | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_mem | --- | 0.05 | --- | --- | --- | --- | --- | --- |
head_precedes | --- | --- | 0.10 | --- | --- | --- | --- | --- |
precedes_tail | --- | --- | 2.77 | --- | --- | --- | --- | --- |
tail_not_precedes | --- | 0.02 | --- | --- | --- | --- | --- | --- |
split_list_precedes | --- | --- | 13.31 | --- | --- | --- | --- | --- |
precedes_refl | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_left | --- | 0.05 | --- | --- | --- | --- | --- | --- |
precedes_append_left_iff | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| precedes_append_left_iff.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| precedes_append_left_iff.1.1 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_left_iff.1.2 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_left_iff.1.3 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_left_iff.1.4 | --- | 0.01 | --- | --- | --- | --- | --- | --- |
precedes_append_right | --- | 0.80 | --- | --- | --- | --- | --- | --- |
precedes_append_right_iff | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| precedes_append_right_iff.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| precedes_append_right_iff.1.1 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_right_iff.1.2 | --- | 0.02 | --- | --- | --- | --- | --- | --- |
precedes_append_right_iff.1.3 | --- | 0.06 | --- | --- | --- | --- | --- | --- |
precedes_append_right_iff.1.4 | --- | 0.01 | --- | --- | --- | --- | --- | --- |
simplelist_tl | --- | --- | 0.31 | --- | --- | --- | --- | --- |
simplelist_split | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_split.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_split.1.1 | --- | --- | 1.27 | --- | --- | --- | --- | --- |
simplelist_split.1.2 | --- | --- | 1.34 | --- | --- | --- | --- | --- |
simplelist_split.1.3 | --- | --- | 2.09 | --- | --- | --- | --- | --- |
simplelist_split.1.4 | --- | --- | 1.67 | --- | --- | --- | --- | --- |
simplelist_app_disjoint | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_app_disjoint.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_app_disjoint.1.1 | --- | --- | --- | --- | 0.09 | --- | --- | --- |
simplelist_app_disjoint.1.2 | --- | --- | 1.57 | --- | --- | --- | --- | --- |
simplelist_length | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| simplelist_length.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| simplelist_length.1.1 | --- | 0.01 | --- | --- | --- | --- | --- | --- |
simplelist_length.1.2 | --- | 0.01 | --- | --- | --- | --- | --- | --- |
precedes_antisym | --- | 0.76 | --- | --- | --- | --- | --- | --- |
precedes_trans | --- | --- | --- | --- | --- | --- | --- | --- |
induction_ty_lex | | | | | | | | |
| precedes_trans.1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| precedes_trans.1.1 | --- | --- | 6.14 | --- | --- | --- | --- | --- |
reachable_refl | --- | --- | --- | --- | 0.03 | --- | --- | --- |
reachable_trans | --- | --- | 0.18 | --- | --- | --- | --- | --- |
xpath_xedge | --- | --- | --- | --- | --- | --- | --- | --- |
induction_pr | | | | | | | | |
| xpath_xedge.1 | --- | 0.01 | --- | --- | --- | --- | --- | --- |
xpath_xedge.2 | --- | --- | --- | --- | 0.06 | --- | --- | --- |
same_scc_refl | --- | --- | --- | --- | 0.07 | --- | --- | --- |
same_scc_sym | --- | 0.01 | --- | --- | --- | --- | --- | --- |
same_scc_trans | --- | 0.02 | --- | --- | --- | --- | --- | --- |
subscc_add | --- | 0.04 | --- | --- | --- | --- | --- | --- |
scc_max | --- | --- | 0.54 | --- | --- | --- | --- | --- |
subscc_after_last_gray | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| subscc_after_last_gray.1 | --- | 1.29 | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.2 | --- | 0.04 | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.3 | --- | Timeout (45s) | 40.01 | --- | Timeout (45s) | --- | --- | Timeout (45s) |
subscc_after_last_gray.4 | --- | 0.19 | 0.69 | --- | --- | --- | --- | --- |
subscc_after_last_gray.5 | --- | 0.30 | --- | --- | --- | --- | --- | --- |
subscc_after_last_gray.6 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| subscc_after_last_gray.6.1 | --- | 7.89 | --- | --- | --- | --- | --- | --- |
wf_color_postcond_split | --- | --- | 0.59 | --- | --- | --- | --- | --- |
wf_color_sccs | --- | --- | 0.73 | --- | --- | --- | --- | --- |
wf_color_3_cases | --- | --- | 0.30 | --- | --- | --- | --- | --- |
num_lmem | Timeout (45s) (obsolete) | --- | 3.17 | --- | --- | --- | --- | --- |
num_rank_strict | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| num_rank_strict.1 | --- | --- | 0.58 | --- | --- | --- | --- | --- |
num_rank_strict.2 | --- | 0.03 | --- | --- | --- | --- | --- | --- |
num_rank_strict.3 | --- | --- | 0.60 | --- | --- | --- | --- | --- |
simplelist_x_prec_strict_y' | --- | 0.83 | --- | --- | --- | --- | --- | --- |
51. VC for split | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. postcondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
2. postcondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | 0.01 | --- | --- | --- | --- | --- | --- |
4. postcondition | --- | 1.01 | --- | --- | --- | --- | --- | --- |
5. postcondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
6. postcondition | --- | 0.10 | --- | --- | --- | --- | --- | --- |
52. VC for add_stack_incr | --- | 0.01 | --- | --- | --- | --- | --- | --- |
53. VC for add_black | --- | 0.02 | --- | --- | --- | --- | --- | --- |
54. VC for set_infty | --- | 0.03 | --- | --- | --- | --- | --- | --- |
55. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | 1.65 | --- | --- | --- |
3. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | --- | 1.15 | --- | --- | --- | --- | --- | --- |
2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. precondition | --- | 1.00 | 1.24 | --- | --- | --- | --- | --- |
2. precondition | --- | 0.06 | --- | --- | --- | --- | --- | --- |
3. precondition | --- | 0.86 | --- | --- | --- | --- | --- | --- |
4. precondition | --- | 0.23 | --- | --- | --- | --- | --- | --- |
5. precondition | --- | 0.46 | --- | --- | --- | --- | --- | --- |
6. precondition | --- | 0.28 | --- | --- | --- | --- | --- | --- |
7. precondition | --- | 26.14 | 1.15 | --- | --- | --- | --- | --- |
8. precondition | --- | --- | 1.33 | --- | --- | --- | --- | --- |
3. precondition | --- | 0.06 | --- | --- | --- | --- | --- | --- |
4. precondition | --- | 0.34 | --- | --- | --- | --- | --- | --- |
5. precondition | --- | --- | 17.94 | --- | --- | --- | --- | --- |
6. precondition | --- | --- | 12.19 | --- | --- | --- | --- | --- |
7. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
8. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
9. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
4. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | 0.18 | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | 0.19 | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | 3.79 | --- | --- | --- | --- | --- | --- |
5. assertion | --- | Timeout (45s) (obsolete) | 0.90 | --- | --- | --- | --- | Timeout (45s) (obsolete) |
6. assertion | --- | 0.06 | --- | --- | --- | --- | --- | --- |
7. assertion | --- | --- | 11.59 | --- | --- | --- | --- | --- |
8. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | 2.73 | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | --- | 1.54 | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | 2.56 |
4. VC for dfs1 | --- | --- | 2.38 | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | --- | 21.93 | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | 5.22 | --- | --- | --- | --- | --- | --- |
4. VC for dfs1 | --- | 0.07 | --- | --- | --- | --- | --- | --- |
5. VC for dfs1 | --- | 1.00 | --- | --- | --- | --- | --- | --- |
6. VC for dfs1 | --- | Timeout (45s) (obsolete) | 3.88 | --- | --- | Timeout (45s) (obsolete) | --- | Timeout (45s) (obsolete) |
7. VC for dfs1 | --- | 10.30 | 2.25 | --- | --- | --- | --- | --- |
8. VC for dfs1 | --- | 0.60 | 0.34 | --- | --- | --- | --- | --- |
9. VC for dfs1 | --- | Timeout (45s) (obsolete) | 88.84 (obsolete) | --- | Timeout (45s) (obsolete) | Timeout (45s) (obsolete) | Timeout (45s) (obsolete) | 11.74 |
10. VC for dfs1 | --- | --- | --- | 1.49 | --- | --- | --- | --- |
11. VC for dfs1 | --- | 0.66 | 0.79 | --- | --- | --- | --- | --- |
12. VC for dfs1 | --- | 0.03 | 0.30 | --- | --- | --- | --- | --- |
13. VC for dfs1 | --- | 0.31 | 0.94 | --- | --- | --- | --- | --- |
14. VC for dfs1 | --- | 2.79 | 0.94 | --- | --- | --- | --- | --- |
9. postcondition | --- | --- | 0.24 | --- | --- | --- | --- | --- |
10. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | 0.34 | --- | --- | --- | --- | --- | --- |
11. postcondition | --- | --- | 1.35 | --- | --- | --- | --- | --- |
12. postcondition | --- | --- | 2.19 | --- | --- | --- | --- | --- |
13. assertion | --- | --- | --- | 1.30 | --- | --- | --- | --- |
14. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | --- | 2.78 | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | 0.17 | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | --- | --- | --- | 14.60 | --- | --- | --- |
15. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. assertion | --- | --- | --- | --- | --- | --- | --- | 0.48 |
16. 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 | --- | 1.91 | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | 2.18 |
3. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | Timeout (45s) (obsolete) | 59.87 | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | 38.67 | --- | --- | --- | --- | --- | --- |
4. VC for dfs1 | --- | 8.33 | --- | --- | --- | --- | --- | --- |
2. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_goal_wp | | | | | | | | |
| 1. VC for dfs1 | --- | 13.08 | --- | --- | --- | --- | --- | --- |
2. VC for dfs1 | --- | 1.92 | --- | --- | --- | --- | --- | --- |
3. VC for dfs1 | --- | 3.42 | --- | --- | --- | --- | --- | --- |
4. VC for dfs1 | --- | 2.03 | --- | --- | --- | --- | --- | --- |
5. VC for dfs1 | --- | 2.38 | --- | --- | --- | --- | --- | --- |
6. VC for dfs1 | --- | 2.22 | --- | --- | --- | --- | --- | --- |
7. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | | | |
| 1. VC for dfs1 | --- | 11.62 | --- | --- | --- | --- | --- | --- |
8. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | | | |
| 1. VC for dfs1 | --- | 14.21 | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | 14.64 | --- | --- | --- | --- | --- | --- |
4. postcondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
5. postcondition | --- | Timeout (45s) (obsolete) | 48.26 | --- | --- | --- | --- | Timeout (45s) (obsolete) |
6. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. VC for dfs1 | --- | --- | 65.85 | --- | --- | --- | --- | --- |
7. postcondition | --- | 3.09 | 10.14 | --- | --- | --- | --- | --- |
8. postcondition | --- | 0.73 | --- | --- | --- | --- | --- | --- |
9. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
split_all_full | | | | | | | | |
| 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs1 | --- | --- | --- | --- | 22.07 | --- | --- | --- |
10. postcondition | --- | --- | --- | --- | 0.31 | --- | --- | --- |
11. postcondition | --- | 0.10 | 1.11 | --- | --- | --- | --- | --- |
12. postcondition | --- | 0.10 | 1.13 | --- | --- | --- | --- | --- |
13. postcondition | --- | --- | --- | --- | --- | --- | --- | 3.64 |
14. postcondition | --- | 0.04 | --- | --- | --- | --- | --- | --- |
17. postcondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
18. postcondition | --- | 0.47 | --- | --- | --- | --- | --- | --- |
19. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. postcondition | --- | 0.01 | --- | --- | --- | --- | --- | --- |
20. postcondition | --- | 1.89 | --- | --- | --- | --- | --- | --- |
56. 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.31 | --- | --- | --- | --- | --- | --- |
7. VC for dfs | --- | 0.02 | --- | --- | --- | --- | --- | --- |
8. VC for dfs | --- | 0.02 | --- | --- | --- | --- | --- | --- |
9. VC for dfs | --- | 0.03 | --- | --- | --- | --- | --- | --- |
10. VC for dfs | --- | --- | 0.24 | --- | --- | --- | --- | --- |
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.58 | --- | --- | --- | --- | --- | --- |
6. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
7. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
8. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
9. 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.17 | --- | --- | --- | --- | --- | --- |
6. VC for dfs | --- | 1.01 | --- | --- | --- | --- | --- | --- |
7. VC for dfs | --- | 0.05 | --- | --- | --- | --- | --- | --- |
8. VC for dfs | --- | 0.06 | --- | --- | --- | --- | --- | --- |
9. VC for dfs | --- | 0.06 | --- | --- | --- | --- | --- | --- |
10. VC for dfs | --- | --- | --- | --- | --- | --- | --- | 0.04 |
11. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
12. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
13. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
14. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
10. postcondition | --- | 2.21 | --- | --- | --- | --- | --- | --- |
11. postcondition | --- | --- | 1.86 | --- | --- | --- | --- | --- |
12. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
introduce_premises | | | | | | | | |
| 1. VC for dfs | --- | --- | --- | --- | --- | --- | --- | --- |
inline_goal | | | | | | | | |
| 1. VC for dfs | --- | 2.87 | --- | --- | --- | --- | --- | --- |
13. postcondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
14. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
15. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
16. precondition | --- | 0.15 | --- | --- | --- | --- | --- | --- |
17. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
18. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
19. precondition | --- | 0.04 | --- | --- | --- | --- | --- | --- |
20. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
21. 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.36 |
2. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
3. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
4. VC for dfs | --- | 0.21 | --- | --- | --- | --- | --- | --- |
5. VC for dfs | --- | 0.04 | --- | --- | --- | --- | --- | --- |
22. postcondition | --- | 0.10 | --- | --- | --- | --- | --- | --- |
23. postcondition | --- | --- | 3.41 | --- | --- | --- | --- | --- |
24. postcondition | --- | 1.11 | --- | --- | --- | --- | --- | --- |
25. postcondition | --- | --- | 7.63 | --- | --- | --- | --- | --- |
57. 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 | --- | 1.78 | --- | --- | --- | --- | --- | --- |
2. postcondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
3. postcondition | --- | 0.15 | --- | --- | --- | --- | --- | --- |