Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (1.01)Alt-Ergo (1.30)CVC3 (2.4.1)CVC4 (1.4)CVC4 (1.5-prerelease)Coq (8.5pl2)Eprover (1.9)Spass (3.7)Yices (1.0.40)Z3 (4.5.0)
lmem_dec0.00---------------------------
list_simpl_r------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.---------0.08------------------
list_assoc_cons---------0.06------------------
rank_not_mem------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.0.01---------------------------
rank_range------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.0.01---------------------------
3.0.01---------------------------
4.0.01---------------------------
rank_min------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.---------0.72------------------
rank_app_l------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.0.10---------------------------
rank_app_r------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.0.04---------------------------
simplelist_tl---------0.10------------------
simplelist_split------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.------------------------0.10---
2.------------------------0.11---
3.---------2.60------------------
4.---------2.58------------------
simplelist_hd_max_rank0.02---------------------------
rank_before_suffix0.18---------------------------
inter_com------0.04---------------------
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
  1.------------------------------
split_goal_wp
  1.------------------0.06---------
2.0.04---------------------------
simplelist_length------------------------------
induction_ty_lex
  1.------------------------------
split_goal_wp
  1.0.01---------------------------
2.0.01---------------------------
set_of_elt------------------------------
split_goal_wp
  1.0.02---------------------------
2.---------------------1.14------
elt_set_of------------------0.34---------
subset_set_of0.04---------------------------
reachable_trans------0.19---------------------
xset_path_xedge------------------------------
induction_pr
  1.0.01---------------------------
2.------------------0.04---------
same_scc_refl------------------0.07---------
same_scc_sym0.01---------------------------
same_scc_trans0.02---------------------------
subscc_add0.04---------------------------
scc_max---------1.60------------------
subscc_after_last_gray------------------------------
split_goal_wp
  1.------------------------------
inline_goal
  1.------------------------------
split_goal_wp
  1.0.57---------------------------
2.0.29---------------------------
2.2.58---------------------------
3.---------8.69------------------
4.------------------------------
inline_goal
  1.------------------0.14---------
wf_color_postcond_split------------------------------
inline_goal
  1.------------------------------
split_goal_wp
  1.------------------0.25---------
2.------------------4.79---------
wf_color_sccs---------2.43------------------
wf_color_3_cases---------0.31------------------
VC for split------------------------------
split_goal_wp
  1. postcondition0.01---------------------------
2. postcondition0.01---------------------------
3. postcondition0.01---------------------------
4. postcondition------0.34---------------------
5. postcondition0.01---------------------------
6. postcondition1.26---------------------------
VC for add_stack_incr------------------------------
split_goal_wp
  1. index in array bounds0.01---------------------------
2. type invariant0.01---------------------------
3. postcondition0.01---------------------------
VC for add_blacks0.01---------------------------
VC for set_max_int------------------------------
split_goal_wp
  1. postcondition---0.02------------------------
2. precondition------0.73---------------------
3. index in array bounds------3.80---------------------
4. postcondition---0.04------------------------
5. postcondition---0.04------------------------
VC for dfs1------------------------------
split_goal_wp
  1. assertion------------------------------
inline_goal
  1. assertion------------------------------
inline_goal
  1. assertion---------25.81------------------
2. index in array bounds------------------------------
split_goal_wp
  1. VC for dfs1---0.01------------------------
2. VC for dfs1---0.01------------------------
3. type invariant---0.01------------------------
4. precondition---0.02------------------------
5. precondition------------------------------
inline_goal
  1. precondition------------------1.77---------
6. precondition------------------------------
inline_goal
  1. precondition------------------------------
split_goal_wp
  1. precondition---1.29------------------------
2. precondition------------------------------
inline_goal
  1. precondition------------------------------
split_goal_wp
  1. precondition---1.03------------------------
2. precondition---0.23------------------------
3. precondition---0.71------------------------
4. precondition---0.04------------------------
5. precondition---1.96------------------------
6. precondition---0.49------------------------
7. precondition---1.54------------------------
8. precondition---3.24------------------------
9. precondition---0.02------------------------
3. precondition---0.03------------------------
4. precondition---0.81------------------------
5. precondition---2.76------------------------
6. precondition---------------1.70------------
7. precondition------------------------------
split_goal_wp
  1. precondition---0.01------------------------
2. precondition---0.01------------------------
3. precondition---0.01------------------------
8. assertion------------------------------
split_goal_wp
  1. VC for dfs1---0.30------------------------
2. VC for dfs1---0.75------------------------
3. VC for dfs1---1.17------------------------
9. assertion------------------4.57---------
10. assertion---------------2.64------------
11. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition---0.31------------------------
2. postcondition---19.94------------------------
3. postcondition---10.44---3.28------------------
4. postcondition---0.03------------------------
2. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition---0.04------------------------
2. postcondition---5.28---3.70------------------
3. postcondition---0.58------------------------
4. postcondition---0.03---1.35------------------
5. postcondition---6.08---3.95------------------
6. postcondition---1.27---4.04------------------
7. postcondition---0.46------------------------
8. postcondition---0.04------------------------
9. postcondition---0.03---0.51------------------
3. postcondition---------6.57------------------
4. postcondition---0.02------------------------
5. postcondition---0.06---1.01------------------
6. postcondition---------48.70------------------
12. postcondition------------------------------
split_goal_wp
  1. postcondition---0.46------------------------
2. postcondition---0.02------------------------
3. postcondition------------11.70---------------
13. postcondition---34.69------------------------
14. postcondition---2.04------------------------
15. postcondition---107.64------------------------
16. postcondition---0.02---0.36------0.06---------
17. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. VC for dfs1---6.82------------------------
2. VC for dfs1---0.02------------------------
3. VC for dfs1---0.02------------------------
4. VC for dfs1---0.29------------------------
18. assertion---------------2.36------------
19. assertion------------------------------
inline_goal
  1. assertion------------------------------
split_goal_wp
  1. VC for dfs1---0.86------------------------
2. VC for dfs1---0.03------------------------
3. VC for dfs1------------------9.03---------
20. assertion------------------------------
split_goal_wp
  1. VC for dfs1---19.80------------------------
2. VC for dfs1---0.02------------------------
21. assertion---0.01------------------------
22. assertion---------------------------0.78
23. precondition---1.51------------------------
24. assertion------------------------------
split_goal_wp
  1. assertion---0.02------------------------
2. assertion------------------------------
inline_goal
  1. assertion---------------------------16.72
25. type invariant---0.01------------------------
26. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition---0.28------------------------
2. postcondition---3.89------------------------
3. postcondition---------3.45------------------
4. postcondition---2.38------------------------
2. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. postcondition---------64.59------------------
2. postcondition---2.39------------------------
3. postcondition---------56.43------------------
4. postcondition---------56.31------------------
5. postcondition---------60.41------------------
6. postcondition---------61.75------------------
7. postcondition---0.09------------------------
8. postcondition---1.08------------------------
9. postcondition---0.03---0.51------------------
3. postcondition---8.33---5.82------------------
4. postcondition---0.02------------------------
5. postcondition---0.03---0.46------------------
6. postcondition---1.48---6.89------------------
27. postcondition------------------------------
split_goal_wp
  1. postcondition---5.27------------------------
2. postcondition---0.03------------------------
3. postcondition------------------18.70---------
28. postcondition---0.28---1.80------0.24---------
29. postcondition------------------------------
inline_goal
  1. postcondition---------0.08------------------
30. postcondition------------------------------
inline_goal
  1. postcondition---0.05---0.40------------------
31. postcondition---0.02---0.34------0.16---------
32. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. VC for dfs1------------------0.30---------
2. VC for dfs1---0.02------------------------
3. VC for dfs1---0.02------------------------
4. VC for dfs1---------0.52------------------
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------------------------
8. assertion---13.18------------------------
9. index in array bounds---0.02------------------------
10. index in array bounds---0.01------------------------
11. assertion---0.37------------------------
12. precondition---0.01------------------------
13. precondition---0.02------------------------
14. precondition---0.01------------------------
15. precondition---0.01------------------------
16. postcondition---0.01------------------------
17. postcondition---0.01------------------------
18. postcondition------------------------------
inline_goal
  1. postcondition------17.942.31------------------
19. postcondition------------------------------
inline_goal
  1. postcondition------25.50---------------------
20. postcondition---------0.18------------------
21. postcondition------------------------------
inline_goal
  1. postcondition---1.39------------------------
22. postcondition---0.01------------------------
23. precondition---0.01------------------------
24. precondition---0.02------------------------
25. precondition---0.03------------------------
26. precondition---0.01------------------------
27. precondition---0.01------------------------
28. assertion---------------------------0.37
29. precondition---0.01------------------------
30. precondition---0.01------------------------
31. precondition---0.01------------------------
32. precondition---0.01------------------------
33. postcondition---0.01------------------------
34. postcondition---0.01------------------------
35. postcondition---------6.51------------------
36. postcondition------------------------------
inline_goal
  1. postcondition---------26.43------------------
37. postcondition------------------------------
inline_goal
  1. postcondition---------171.77------------------
38. postcondition---0.02------------------------
39. postcondition------------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. VC for dfs'---------------------------0.66
2. VC for dfs'---0.02------------------------
3. VC for dfs'---0.02------------------------
4. VC for dfs'---0.04------------------------
VC for tarjan------------------------------
split_goal_wp
  1. array creation size---0.01------------------------
2. precondition---0.01------------------------
3. precondition---0.01------------------------
4. precondition------------------------------
inline_goal
  1. precondition------------------------------
split_goal_wp
  1. precondition---0.05------------------------
2. precondition------------------------------
inline_goal
  1. precondition------------------------------
split_goal_wp
  1. precondition---0.02------------------------
2. precondition---0.02------------------------
3. precondition---0.02------------------------
4. precondition---0.02------0.13---------------
5. precondition---0.02------0.14---------------
6. precondition---0.02------------------------
7. precondition---0.02------0.12---------------
8. precondition---0.02------0.13---------------
9. precondition---0.01------------------------
3. precondition---0.01------------------------
4. precondition---0.01------------------------
5. precondition---0.01------------------------
6. precondition---0.01------------------------
5. precondition---0.01------------------------
6. assertion---0.02------------------------
7. postcondition------------------------------
split_goal_wp
  1. postcondition---0.29------------------------
2. postcondition---0.02------------------------
3. postcondition---0.02------------------------