| 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.6.2) | 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 (obsolete) | 0.03 | --- | --- | --- | --- | --- | --- |
| set_of_elt.2 | --- | Timeout (45s) | --- | --- | --- | 3.82 | --- | --- |
| elt_set_of | --- | --- | --- | --- | 0.22 | --- | --- | --- |
| subset_set_of | 0.04 | --- | --- | --- | --- | --- | --- | --- |
| 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 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| list_simpl_r.1.2 | --- | --- | 0.22 (obsolete) | --- | --- | --- | --- | --- |
| snoc_app | 0.02 | --- | --- | --- | --- | --- | --- | --- |
| precedes_mem | 0.05 | --- | --- | --- | --- | --- | --- | --- |
| head_precedes | --- | --- | 0.10 | --- | --- | --- | --- | --- |
| precedes_tail | --- | --- | 1.50 | --- | --- | --- | --- | --- |
| tail_not_precedes | 0.02 | --- | --- | --- | --- | --- | --- | --- |
| split_list_precedes | --- | --- | 7.88 | --- | --- | --- | --- | --- |
| 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 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_left_iff.1.2 | 0.02 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_left_iff.1.3 | 0.02 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_left_iff.1.4 | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 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 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_right_iff.1.2 | 0.02 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_right_iff.1.3 | 0.06 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_append_right_iff.1.4 | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| simplelist_tl | --- | --- | 0.12 | --- | --- | --- | --- | --- |
| simplelist_split | --- | --- | --- | --- | --- | --- | --- | --- |
| induction_ty_lex | | | | | | | | |
| | simplelist_split.1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | simplelist_split.1.1 | --- | --- | 0.59 (obsolete) | --- | --- | --- | --- | --- |
| simplelist_split.1.2 | --- | --- | 0.62 (obsolete) | --- | --- | --- | --- | --- |
| simplelist_split.1.3 | --- | --- | 0.91 (obsolete) | --- | --- | --- | --- | --- |
| simplelist_split.1.4 | --- | --- | 0.73 (obsolete) | --- | --- | --- | --- | --- |
| simplelist_app_disjoint | --- | --- | --- | --- | --- | --- | --- | --- |
| induction_ty_lex | | | | | | | | |
| | simplelist_app_disjoint.1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | simplelist_app_disjoint.1.1 | --- | --- | --- | --- | 0.09 (obsolete) | --- | --- | --- |
| simplelist_app_disjoint.1.2 | --- | --- | 0.69 (obsolete) | --- | --- | --- | --- | --- |
| simplelist_length | --- | --- | --- | --- | --- | --- | --- | --- |
| induction_ty_lex | | | | | | | | |
| | simplelist_length.1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | simplelist_length.1.1 | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| simplelist_length.1.2 | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| precedes_antisym | 0.34 | --- | --- | --- | --- | --- | --- | --- |
| precedes_trans | --- | --- | --- | --- | --- | --- | --- | --- |
| induction_ty_lex | | | | | | | | |
| | precedes_trans.1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | precedes_trans.1.1 | --- | --- | 4.14 (obsolete) | --- | --- | --- | --- | --- |
| reachable_refl | --- | --- | --- | --- | 0.03 | --- | --- | --- |
| reachable_trans | --- | --- | 0.18 | --- | --- | --- | --- | --- |
| xpath_xedge | --- | --- | --- | --- | --- | --- | --- | --- |
| induction_pr | | | | | | | | |
| | xpath_xedge.1 | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| xpath_xedge.2 | --- | --- | --- | --- | 0.06 (obsolete) | --- | --- | --- |
| same_scc_refl | --- | --- | --- | --- | 0.07 | --- | --- | --- |
| same_scc_sym | 0.01 | --- | --- | --- | --- | --- | --- | --- |
| same_scc_trans | 0.02 | --- | --- | --- | --- | --- | --- | --- |
| subscc_add | 0.04 | --- | --- | --- | --- | --- | --- | --- |
| scc_max | --- | --- | 0.32 | --- | --- | --- | --- | --- |
| subscc_after_last_gray | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | subscc_after_last_gray.1 | --- | --- | 0.94 (obsolete) | --- | --- | --- | --- | --- |
| subscc_after_last_gray.2 | 0.04 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| subscc_after_last_gray.3 | Timeout (45s) (obsolete) | --- | 26.89 (obsolete) | --- | --- | --- | --- | --- |
| subscc_after_last_gray.4 | Timeout (45s) (obsolete) | --- | 0.75 (obsolete) | --- | Timeout (45s) (obsolete) | --- | Timeout (45s) (obsolete) | --- |
| subscc_after_last_gray.5 | Timeout (45s) (obsolete) | --- | 4.60 (obsolete) | --- | Timeout (45s) (obsolete) | --- | Timeout (45s) (obsolete) | --- |
| subscc_after_last_gray.6 | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | subscc_after_last_gray.6.1 | --- | --- | --- | --- | 0.40 (obsolete) | --- | --- | --- |
| wf_color_postcond_split | --- | --- | 0.51 | --- | --- | --- | --- | --- |
| wf_color_sccs | --- | --- | 0.66 | --- | --- | --- | --- | --- |
| wf_color_3_cases | --- | --- | 0.30 | --- | --- | --- | --- | --- |
| num_lmem | Timeout (45s) (obsolete) | --- | 3.90 | --- | --- | --- | --- | --- |
| num_rank_strict | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | num_rank_strict.1 | --- | --- | 0.53 (obsolete) | --- | --- | --- | --- | --- |
| num_rank_strict.2 | 0.03 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| num_rank_strict.3 | --- | --- | 0.61 (obsolete) | --- | --- | --- | --- | --- |
| 50. VC for split | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. postcondition | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. postcondition | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 3. postcondition | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 4. postcondition | --- | --- | 0.33 (obsolete) | --- | --- | --- | --- | --- |
| 5. postcondition | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 6. postcondition | 0.05 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 51. VC for add_stack_incr | 0.01 | --- | --- | --- | --- | --- | --- | --- |
| 52. VC for add_black | 0.02 | --- | --- | --- | --- | --- | --- | --- |
| 53. VC for set_infty | 0.03 | --- | --- | --- | --- | --- | --- | --- |
| 54. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | 0.02 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | 0.29 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 3. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | 0.08 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 4. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. assertion | Timeout (15s) (obsolete) | --- | 0.23 (obsolete) | --- | --- | --- | --- | --- |
| 5. assertion | Timeout (15s) (obsolete) | --- | 2.53 (obsolete) | --- | --- | --- | --- | --- |
| 6. assertion | Timeout (15s) (obsolete) | --- | 14.09 (obsolete) | --- | --- | --- | --- | --- |
| 7. assertion | Timeout (25s) (obsolete) | --- | 49.48 (obsolete) | --- | Timeout (25s) (obsolete) | --- | --- | --- |
| inline_all | | | | | | | | |
| | 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| split_all_full | | | | | | | | |
| | 1. assertion | Timeout (45s) (obsolete) | --- | 14.70 (obsolete) | --- | --- | --- | --- | --- |
| 8. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. assertion | Timeout (15s) (obsolete) | --- | 24.04 (obsolete) | --- | Timeout (25s) (obsolete) | --- | --- | --- |
| 9. 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.26 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | --- | --- | 0.98 (obsolete) | --- | --- | --- | --- | --- |
| 3. VC for dfs1 | Timeout (15s) (obsolete) | --- | 14.32 (obsolete) | --- | --- | --- | --- | --- |
| 4. VC for dfs1 | --- | --- | 1.33 (obsolete) | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | --- | --- | 19.31 (obsolete) | --- | --- | --- | --- | --- |
| 3. VC for dfs1 | 4.61 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 4. VC for dfs1 | 0.07 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 5. VC for dfs1 | 0.74 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 6. VC for dfs1 | --- | --- | 18.61 (obsolete) | --- | --- | --- | --- | --- |
| 7. VC for dfs1 | 22.04 (obsolete) | --- | 0.99 (obsolete) | --- | --- | --- | --- | --- |
| 8. VC for dfs1 | 0.35 (obsolete) | --- | 0.15 (obsolete) | --- | --- | --- | --- | --- |
| 9. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | 19.92 (obsolete) |
| 10. VC for dfs1 | 0.03 (obsolete) | --- | 0.21 (obsolete) | High Failure (obsolete) | Timeout (55s) (obsolete) | Timeout (55s) (obsolete) | --- | Timeout (55s) (obsolete) |
| 11. VC for dfs1 | 0.41 (obsolete) | --- | 0.42 (obsolete) | --- | --- | --- | --- | --- |
| 12. VC for dfs1 | 0.03 (obsolete) | --- | 0.12 (obsolete) | --- | --- | --- | --- | --- |
| 13. VC for dfs1 | 0.19 (obsolete) | --- | 0.47 (obsolete) | --- | --- | --- | --- | --- |
| 14. VC for dfs1 | 2.43 (obsolete) | --- | 0.62 (obsolete) | --- | --- | --- | --- | --- |
| 10. postcondition | --- | --- | 0.11 (obsolete) | --- | --- | --- | --- | --- |
| 11. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. postcondition | 0.29 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 12. postcondition | --- | --- | 9.37 (obsolete) | --- | --- | --- | --- | --- |
| 13. postcondition | --- | --- | 2.09 (obsolete) | --- | --- | --- | --- | --- |
| 14. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. assertion | Timeout (55s) (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 15. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | 1.44 (obsolete) | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | 0.17 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 3. VC for dfs1 | --- | --- | --- | --- | 4.23 (obsolete) | --- | --- | --- |
| 16. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. assertion | --- | --- | --- | --- | --- | --- | --- | 0.21 (obsolete) |
| 17. 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.76 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | 1.00 (obsolete) |
| 3. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. VC for dfs1 | Timeout (15s) (obsolete) | --- | 14.89 (obsolete) | --- | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) | --- | Timeout (15s) (obsolete) |
| simplify_formula | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | 14.96 (obsolete) | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | Timeout (15s) (obsolete) | --- | 14.82 (obsolete) | --- | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) | --- | Timeout (15s) (obsolete) |
| inline_trivial | | | | | | | | |
| | 1. VC for dfs1 | Timeout (15s) (obsolete) | --- | 14.97 (obsolete) | --- | Timeout (15s) (obsolete) | --- | --- | Timeout (15s) (obsolete) |
| 4. VC for dfs1 | 3.85 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. VC for dfs1 | 6.50 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 2. VC for dfs1 | 0.75 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 3. VC for dfs1 | 0.87 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 4. VC for dfs1 | 1.04 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 5. VC for dfs1 | --- | --- | 9.79 (obsolete) | --- | --- | --- | --- | --- |
| 6. VC for dfs1 | 1.06 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 7. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_all_full | | | | | | | | |
| | 1. VC for dfs1 | 2.53 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 8. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| split_all_full | | | | | | | | |
| | 1. VC for dfs1 | 3.03 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 3. postcondition | 2.32 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 4. postcondition | 0.03 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 5. postcondition | Timeout (25s) (obsolete) | --- | 24.50 (obsolete) | --- | Timeout (25s) (obsolete) | --- | --- | --- |
| 6. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_all_full | | | | | | | | |
| | 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | 37.44 (obsolete) | --- | --- | --- | --- | --- |
| 7. postcondition | 0.98 (obsolete) | --- | 4.95 (obsolete) | --- | --- | --- | --- | --- |
| 8. postcondition | 0.28 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 9. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_all_full | | | | | | | | |
| | 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. VC for dfs1 | --- | --- | --- | --- | 11.07 (obsolete) | --- | --- | --- |
| 10. postcondition | --- | --- | 1.63 (obsolete) | --- | 0.25 (obsolete) | --- | --- | --- |
| 11. postcondition | 0.10 (obsolete) | --- | 1.10 (obsolete) | --- | --- | --- | --- | --- |
| 12. postcondition | 0.10 (obsolete) | --- | 1.15 (obsolete) | --- | --- | --- | --- | --- |
| 13. postcondition | --- | --- | --- | --- | --- | --- | --- | 1.46 (obsolete) |
| 14. postcondition | 0.04 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 18. postcondition | 0.02 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 19. postcondition | 0.19 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 20. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. postcondition | 0.01 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 21. postcondition | 0.78 (obsolete) | --- | --- | --- | --- | --- | --- | --- |
| 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.30 | --- | --- | --- | --- | --- | --- |
| 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.59 | --- | --- | --- | --- | --- | --- |
| 6. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 7. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 8. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 2. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 3. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 4. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 5. precondition | --- | 0.17 | --- | --- | --- | --- | --- | --- |
| 6. precondition | --- | 0.54 | --- | --- | --- | --- | --- | --- |
| 7. precondition | --- | 0.05 | --- | --- | --- | --- | --- | --- |
| 8. precondition | --- | 0.06 | --- | --- | --- | --- | --- | --- |
| 9. precondition | --- | 0.06 | --- | --- | --- | --- | --- | --- |
| 9. postcondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 10. postcondition | --- | --- | 0.84 | --- | --- | --- | --- | --- |
| 11. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| introduce_premises | | | | | | | | |
| | 1. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. postcondition | --- | 16.34 | --- | --- | --- | --- | --- | --- |
| 12. postcondition | --- | 1.21 | --- | --- | --- | --- | --- | --- |
| 13. postcondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 14. precondition | --- | 0.03 | --- | --- | --- | --- | --- | --- |
| 15. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 16. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 17. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 18. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | --- | 0.02 | --- | --- | --- | --- | --- | --- |
| 19. precondition | --- | Timeout (15s) | --- | --- | --- | --- | --- | --- |
| 20. precondition | --- | --- | 0.11 | --- | --- | --- | --- | --- |
| 21. postcondition | --- | 12.90 | --- | --- | --- | --- | --- | --- |
| 22. postcondition | --- | --- | 0.65 | --- | --- | --- | --- | --- |
| 23. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| 24. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| 25. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |
| 56. VC for tarjan | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | --- | 0.01 | --- | --- | --- | --- | --- | --- |
| 2. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| inline_goal | | | | | | | | |
| | 1. precondition | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. precondition | --- | 0.05 | --- | --- | --- | --- | --- | --- |
| 3. precondition | --- | 0.43 | --- | --- | --- | --- | --- | --- |
| 4. assertion | --- | --- | --- | --- | --- | --- | --- | --- |
| split_goal_wp | | | | | | | | |
| | 1. assertion | --- | 0.16 | --- | --- | --- | --- | --- | --- |
| 5. postcondition | --- | --- | --- | --- | --- | --- | --- | --- |