Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (1.30)Alt-Ergo (2.2.0)CVC3 (2.4.1)CVC4 (1.4 noBV)CVC4 (1.5)CVC4 (1.5-prerelease)Coq (8.7.2)Eprover (1.9)Spass (3.5)Yices (Yices)Z3 (4.4.0)
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.02---------------
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.09------------High Failure---
simplelist_split.1.2------------0.10------------High Failure---
simplelist_split.1.3---------------0.53---------------
simplelist_split.1.4---------------0.46---------------
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---Timeout (55s)------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_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.23---------------
subscc_after_last_gray---------------------------------
split_goal_wp
  subscc_after_last_gray.1---------------0.48---------------
subscc_after_last_gray.2---2.02---------------------------
subscc_after_last_gray.3---------Timeout (55s) (obsolete)---1.23---------------
subscc_after_last_gray.4---------------------------------
inline_goal
  subscc_after_last_gray.4.1---------------------1.20---------
wf_color_postcond_split---------------0.19---------------
wf_color_sccs---------------0.58---------------
wf_color_3_cases---------------0.16---------------
39. VC for split---------------------------------
split_goal_wp
  1. postcondition---0.01---------------------------
2. postcondition---0.01---------------------------
3. postcondition---0.01---------------------------
4. postcondition------0.20------------------------
5. postcondition---0.01---------------------------
6. postcondition---0.05---------------------------
40. VC for add_stack_incr---0.01---------------------------
41. VC for add_blacks---0.01---------------------------
42. VC for set_max_int---0.02---------------------------
43. VC for dfs1---------------------------------
split_goal_wp
  1. precondition---0.03---------------------------
2. precondition---------------------------------
inline_goal
  1. precondition---------------------0.84---------
3. precondition---------------------------------
inline_goal
  1. precondition---------------------------------
split_goal_wp
  1. precondition---0.18---------------------------
2. precondition---------------------------------
inline_goal
  1. precondition---------------------------------
split_goal_wp
  1. precondition------------0.21------------------
2. precondition------------0.46------------------
3. precondition------------0.20------------------
4. precondition------------0.20------------------
5. precondition---0.11---------------------------
6. precondition------------0.26------------------
7. precondition---0.45---------------------------
8. precondition---0.41---------------------------
3. precondition---0.06---------------------------
4. precondition---0.19---------------------------
5. precondition---2.83---------------------------
6. precondition---1.46---------------------------
4. precondition---------------------------------
split_goal_wp
  1. precondition---0.01---------------------------
2. precondition---0.01---------------------------
3. precondition---0.01---------------------------
5. assertion---------------------------------
split_goal_wp
  1. VC for dfs1---0.60---------------------------
2. VC for dfs1---0.61---------------------------
3. VC for dfs1---1.57---------------------------
6. assertion---------------13.60---------------
7. assertion------------------1.13------------
8. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. postcondition---------------13.67---------------
2. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. postcondition------------0.31------------------
2. postcondition------------13.57------1.03---------
3. postcondition------------0.25------------------
4. postcondition------------0.25------------------
5. postcondition---------------1.84---------------
6. postcondition------------1.32------------------
7. postcondition---------------------3.86---------
8. postcondition---------------------3.71---------
3. postcondition---------------2.68---------------
4. postcondition---0.02---------------------------
5. postcondition---------------0.21---------------
6. postcondition------------21.15------------------
9. postcondition---------------------------------
split_goal_wp
  1. postcondition---0.28---------------------------
2. postcondition---0.03---------------------------
3. postcondition---------------8.00---------------
10. postcondition---------------------------------
inline_goal
  1. postcondition---------------0.23---------------
11. postcondition---10.44---------------------------
12. postcondition---48.22---------------------------
13. postcondition---0.01---------------------------
14. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. VC for dfs1---------------------1.13---------
2. VC for dfs1---0.13---------------------------
3. VC for dfs1---0.02---------------------------
4. VC for dfs1---------------------0.33---------
5. VC for dfs1---0.90---------------------------
15. assertion------------------1.44------------
16. assertion---------------------------------
inline_goal
  1. assertion---------------------------------
split_goal_wp
  1. VC for dfs1------------0.37------------------
2. VC for dfs1---0.03---------------------------
3. VC for dfs1---------------------6.67---------
17. assertion---------------------------------
split_goal_wp
  1. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---------------3.03---------------
2. VC for dfs1---------------0.13---------------
2. VC for dfs1---0.02---------------------------
18. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---1.03---------------------------
2. VC for dfs1---4.40---------------------------
3. VC for dfs1---------------------------------
introduce_premises
  1. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---------------------4.21---------
2. VC for dfs1---------------------2.81---------
4. VC for dfs1---0.96---------------------------
2. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---0.13---------0.42---7.06------0.12
2. VC for dfs1---------------------------------
introduce_premises
  1. VC for dfs1---------------------2.25---------
3. VC for dfs1---0.37---------1.05------------0.56
4. VC for dfs1------------------------------0.13
5. VC for dfs1---------------1.81---------------
6. VC for dfs1------------------------------1.69
7. VC for dfs1---------------------21.46---------
8. VC for dfs1---------------------21.78---------
3. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---------------1.49---------------
4. VC for dfs1---0.02---------------------------
5. VC for dfs1---0.02---------------------------
6. VC for dfs1---------------------------------
inline_goal
  1. VC for dfs1---------------------------------
split_goal_wp
  1. VC for dfs1---------------2.07---------------
19. postcondition---------------------------------
split_goal_wp
  1. postcondition---0.40---------------------------
2. postcondition---0.02---------------------------
3. postcondition---------------------6.68---------
20. postcondition---0.18---------------------------
21. postcondition---------------------------------
inline_goal
  1. postcondition---------------0.07---------------
22. postcondition---0.03---------------------------
23. postcondition---0.02---------------------------
24. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. VC for dfs1---------------------0.10---------
2. VC for dfs1---0.02---------------------------
3. VC for dfs1---0.02---------------------------
4. VC for dfs1---------------------2.40---------
5. VC for dfs1---0.02---------------------------
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---------------------------
5. VC for dfs'---0.01---------------------------
8. assertionTimeout (35s) (obsolete)------------13.46---Timeout (25s) (obsolete)---------
9. precondition---0.01---------------------------
10. precondition---0.01---------------------------
11. precondition---0.01---------------------------
12. precondition---0.01---------------------------
13. postcondition---0.01---------------------------
14. postcondition---0.01---------------------------
15. postconditionTimeout (35s) (obsolete)------------0.33---------------
16. postcondition---------------------------------
inline_goal
  1. postcondition---------------6.00---------------
17. postcondition---------------0.12---------------
18. postcondition---------------------------------
inline_goal
  1. postcondition---0.82---------------------------
19. postcondition---0.01---------------------------
20. precondition---0.01---------------------------
21. precondition---0.02---------------------------
22. precondition---0.03---------------------------
23. precondition---0.01---------------------------
24. precondition---0.01---------------------------
25. precondition---0.01---------------------------
26. precondition---0.02---------------------------
27. precondition---0.01---------------------------
28. precondition---0.01---------------------------
29. postcondition---0.01---------------------------
30. postcondition---0.01---------------------------
31. postcondition---------------------------------
inline_goal
  1. postcondition---------------2.88---------------
32. postcondition---------------------------------
inline_goal
  1. postcondition---------------0.20---------------
33. postcondition---------------------------------
inline_goal
  1. postcondition---0.46------30.08------------------
34. postcondition---0.02---------------------------
35. postcondition---------------------------------
inline_goal
  1. postcondition---------------------------------
split_goal_wp
  1. VC for dfs'------------------------------0.31
2. VC for dfs'---0.02---------------------------
3. VC for dfs'---0.02---------------------------
4. VC for dfs'---0.04---------------------------
5. VC for dfs'---0.03---------------------------
45. 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---------------------------
4. precondition---0.01---------------------------
5. assertion---0.02---------------------------
6. postcondition---------------------------------
split_goal_wp
  1. postcondition---0.63---------------------------
2. postcondition---0.02---------------------------
3. postcondition---0.02---------------------------