Why3 Proof Results for Project "scc"

Theory "scc.SCCTarjan72": fully verified in 2.32 s

ObligationsAlt-Ergo (2.2.0)CVC4 (1.5)Coq (8.7.2)Eprover (1.9)Spass (3.5)Z3 (4.4.0)
lmem_dec0.00---------------
list_simpl_r------------------
induction_ty_lex
  list_simpl_r.1------------------
split_goal_wp
  list_simpl_r.1.10.01---------------
list_simpl_r.1.2---0.11------------
list_assoc_cons---0.07------------
rank_not_mem------------------
induction_ty_lex
  rank_not_mem.1------------------
split_goal_wp
  rank_not_mem.1.10.01---------------
rank_not_mem.1.20.01---------------
rank_range------------------
induction_ty_lex
  rank_range.1------------------
split_goal_wp
  rank_range.1.10.01---------------
rank_range.1.20.01---------------
rank_range.1.30.01---------------
rank_range.1.40.01---------------
rank_min------------------
induction_ty_lex
  rank_min.1------------------
split_goal_wp
  rank_min.1.10.01---------------
rank_min.1.2---0.32------------
rank_app_l------------------
induction_ty_lex
  rank_app_l.1------------------
split_goal_wp
  rank_app_l.1.10.01---------------
rank_app_l.1.20.10---------------
rank_app_r------------------
induction_ty_lex
  rank_app_r.1------------------
split_goal_wp
  rank_app_r.1.10.01---------------
rank_app_r.1.20.04---------------
simplelist_tl---0.11------------
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.80------------
simplelist_split.1.4---0.57------------
simplelist_hd_max_rank0.02---------------
rank_before_suffix0.18---------------
inter_com---0.05------------
inter_add0.03---------------
set_elt0.04---------------
set_mem---------0.03------
inter_subset_inter---------0.15------
subset_add0.04---------------
union_add_l0.01---------------
union_add_r0.01---------------
elts_cons0.03---------------
elts_app0.02---------------
simplelist_app_inter------------------
induction_ty_lex
  simplelist_app_inter.1------------------
split_goal_wp
  simplelist_app_inter.1.1---------0.18------
simplelist_app_inter.1.2---1.38------------
simplelist_length------------------
induction_ty_lex
  simplelist_length.1------------------
split_goal_wp
  simplelist_length.1.10.01---------------
simplelist_length.1.20.01---------------
set_of_elt------------------
split_goal_wp
  set_of_elt.10.02---------------
set_of_elt.2------------3.21---
elt_set_of---------0.17------
subset_set_of0.04---------------
reachable_trans---0.07------------
xset_path_xedge------------------
induction_pr
  xset_path_xedge.10.01---------------
xset_path_xedge.2---------0.04------
same_scc_refl---------0.07------
same_scc_sym0.01---------------
same_scc_trans0.02---------------
subscc_add0.04---------------
scc_max---0.27------------
subscc_after_last_gray------------------
split_goal_wp
  subscc_after_last_gray.1---0.51------------
subscc_after_last_gray.22.28---------------
subscc_after_last_gray.3---1.03------------
subscc_after_last_gray.4------------------
inline_goal
  subscc_after_last_gray.4.1---------0.14------
wf_color_postcond_split---0.32------------
wf_color_sccs---0.33------------
wf_color_3_cases---0.15------------
39. VC for split------------------
split_goal_wp
  1. postcondition0.01---------------
2. postcondition0.01---------------
3. postcondition0.01---------------
4. postcondition---0.14------------
5. postcondition0.01---------------
6. postcondition0.05---------------
40. VC for add_stack_incr0.01---------------
41. VC for add_blacks0.01---------------
42. VC for set_max_int0.02---------------
43. VC for dfs1------------------
split_goal_wp
  1. precondition0.03---------------
2. precondition------------------
inline_goal
  1. precondition---------0.83------
3. precondition------------------
inline_goal
  1. precondition------------------
split_goal_wp
  1. precondition------------------
inline_goal
  1. precondition------------------
split_goal_wp
  1. precondition0.02---------------
2. precondition0.07---------------
3. precondition0.03---------------
4. precondition0.03---------------
2. precondition------------------
inline_goal
  1. precondition------------------
split_goal_wp
  1. precondition0.14---------------
2. precondition0.06---------------
3. precondition0.11---------------
4. precondition0.02---------------
5. precondition0.11---------------
6. precondition0.05---------------
7. precondition0.39---------------
8. precondition0.25---------------
3. precondition0.02---------------
4. precondition0.11---------------
5. precondition2.55---------------
6. precondition---2.25------------
4. precondition------------------
split_goal_wp
  1. precondition0.01---------------
2. precondition0.01---------------
3. precondition0.01---------------
5. assertion------------------
split_goal_wp
  1. VC for dfs10.68---------------
2. VC for dfs10.70---------------
3. VC for dfs12.06---------------
6. assertion---------1.61------
7. assertion------1.08---------
8. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition0.07---------------
2. postcondition6.05---------------
3. postcondition---0.26------------
4. postcondition0.16---------------
2. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition---0.27------------
2. postcondition0.16---------------
3. postcondition---0.23------------
4. postcondition---0.23------------
5. postcondition---0.72------------
6. postcondition---0.76------------
7. postcondition---------3.69------
8. postcondition---------3.64------
3. postcondition---1.21------------
4. postcondition0.02---------------
5. postcondition---0.23------------
6. postcondition---1.74------------
9. postcondition------------------
split_goal_wp
  1. postcondition0.30---------------
2. postcondition0.03---------------
3. postcondition---------------10.74
10. postcondition0.51---------------
11. postcondition---0.79------------
12. postcondition------------------
inline_goal
  1. postcondition0.80---------------
13. postcondition0.01---------------
14. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. VC for dfs1---------1.47------
2. VC for dfs10.15---------------
3. VC for dfs10.02---------------
4. VC for dfs1---------0.33------
15. assertion------1.31---------
16. assertion------------------
inline_goal
  1. assertion------------------
split_goal_wp
  1. VC for dfs1---0.35------------
2. VC for dfs10.03---------------
3. VC for dfs1---------7.19------
17. assertion------------------
split_goal_wp
  1. VC for dfs11.33---------------
2. VC for dfs10.02---------------
18. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition0.06---------------
2. postcondition0.93---------------
3. postcondition---2.02------------
4. postcondition0.78---------------
2. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. postcondition0.14---------------
2. postcondition0.11---------------
3. postcondition0.40---------------
4. postcondition---------2.19------
5. postcondition0.25---------------
6. postcondition0.23---------------
7. postcondition---------12.63------
8. postcondition---------12.43------
3. postcondition1.27---------------
4. postcondition0.01---------------
5. postcondition0.02---------------
6. postcondition0.09---------------
19. postcondition------------------
split_goal_wp
  1. postcondition0.52---------------
2. postcondition0.02---------------
3. postcondition---------5.19------
20. postcondition0.22---------------
21. postcondition------------------
inline_goal
  1. postcondition---0.06------------
22. postcondition0.03---------------
23. postcondition0.02---------------
24. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. VC for dfs1---------0.10------
2. VC for dfs10.02---------------
3. VC for dfs10.02---------------
4. VC for dfs1---------1.61------
44. VC for dfs------------------
split_goal_wp
  1. postcondition0.01---------------
2. postcondition0.02---------------
3. postcondition0.02---------------
4. postcondition0.01---------------
5. postcondition0.02---------------
6. postcondition0.02---------------
7. postcondition------------------
introduce_premises
  1. postcondition------------------
inline_goal
  1. postcondition------------------
split_goal_wp
  1. VC for dfs---0.12------------
2. VC for dfs0.02---------------
3. VC for dfs0.01---------------
4. VC for dfs0.01---------------
8. assertion2.21---------------
9. precondition0.02---------------
10. precondition0.02---------------
11. precondition0.01---------------
12. precondition0.02---------------
13. postcondition0.02---------------
14. postcondition0.02---------------
15. postcondition1.64---------------
16. postcondition------------------
introduce_premises
  1. VC for dfs------------------
inline_goal
  1. VC for dfs4.41---------------
17. postcondition0.02---------------
18. postcondition0.42---------------
19. postcondition0.02---------------
20. precondition0.02---------------
21. precondition0.02---------------
22. precondition0.04---------------
23. precondition0.01---------------
24. precondition0.02---------------
25. precondition0.02---------------
26. precondition0.02---------------
27. precondition0.02---------------
28. precondition0.02---------------
29. postcondition0.02---------------
30. postcondition0.02---------------
31. postcondition13.304.99------------
32. postcondition0.57---------------
33. postcondition3.24---------------
34. postcondition0.08---------------
35. postcondition12.68---------------
45. VC for tarjan------------------
split_goal_wp
  1. precondition0.01---------------
2. precondition0.01---------------
3. precondition------------------
inline_goal
  1. precondition------------------
split_goal_wp
  1. precondition0.05---------------
2. precondition0.04---------------
3. precondition0.01---------------
4. precondition0.01---------------
5. precondition0.01---------------
6. precondition0.01---------------
4. precondition0.01---------------
5. assertion0.02---------------
6. postcondition------------------
split_goal_wp
  1. postcondition0.22---------------
2. postcondition0.02---------------
3. postcondition0.02---------------