Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (1.30)CVC3 (2.4.1)CVC4 (1.5-prerelease)Coq (8.6)Eprover (1.9)Spass (3.5)Yices (1.0.40)Z3 (4.4.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.------2.02---------------
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.------0.53---------------
4.------0.46---------------
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.---------------0.75------
elt_set_of------------0.17---------
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------0.23---------------
subscc_after_last_gray------------------------
split_goal_wp
  1.------0.41---------------
2.1.53---------------------
3.------0.97---------------
4.------------------------
inline_goal
  1.------------0.14---------
wf_color_postcond_split------0.19---------------
wf_color_sccs------0.58---------------
wf_color_3_cases------0.16---------------
VC for split------------------------
split_goal_wp
  1. postcondition0.01---------------------
2. postcondition0.01---------------------
3. postcondition0.01---------------------
4. postcondition---0.20------------------
5. postcondition0.01---------------------
6. postcondition0.05---------------------
VC for add_stack_incr0.01---------------------
VC for add_blacks0.01---------------------
VC for set_max_int0.02---------------------
VC for dfs1------------------------
split_goal_wp
  1. precondition0.03---------------------
2. precondition------------------------
inline_goal
  1. precondition------------0.58---------
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. precondition2.55---------------------
8. precondition6.21---------------------
3. precondition0.02---------------------
4. precondition0.27---------------------
5. precondition0.97---------------------
6. precondition------9.30---------------
4. precondition------------------------
split_goal_wp
  1. precondition0.01---------------------
2. precondition0.01---------------------
3. precondition0.01---------------------
5. assertion------------------------
split_goal_wp
  1. VC for dfs10.11---------------------
2. VC for dfs10.25---------------------
3. VC for dfs10.38---------------------
6. assertion------------1.14---------
7. assertion---------1.37------------
8. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition0.07---------------------
2. postcondition9.95---------------------
3. postcondition------0.24---------------
4. postcondition0.03---------------------
2. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition------0.17---------------
2. postcondition2.83---------------------
3. postcondition------0.16---------------
4. postcondition------0.29---------------
5. postcondition------0.69---------------
6. postcondition------0.73---------------
7. postcondition------------7.41---------
8. postcondition------------7.36---------
3. postcondition------1.93---------------
4. postcondition0.02---------------------
5. postcondition------0.21---------------
6. postcondition------2.21---------------
9. postcondition------------------------
split_goal_wp
  1. postcondition0.15---------------------
2. postcondition0.03---------------------
3. postcondition---------------------9.01
10. postcondition1.25---------------------
11. postcondition0.90---------------------
12. postcondition------------------------
inline_goal
  1. postcondition------0.37---------------
13. postcondition0.01---------------------
14. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs1------------0.42---------
2. VC for dfs10.02---------------------
3. VC for dfs10.02---------------------
4. VC for dfs1------------0.33---------
15. assertion---------1.69------------
16. assertion------------------------
inline_goal
  1. assertion------------------------
split_goal_wp
  1. VC for dfs10.36---------------------
2. VC for dfs10.03---------------------
3. VC for dfs1------------5.71---------
17. assertionTimeout (35s) (obsolete)---------------------
split_goal_wp
  1. VC for dfs17.95---------------------
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.07---------------------
2. postcondition0.92---------------------
3. postconditionTimeout (35s) (obsolete)---12.42---------------
4. postcondition0.69---------------------
2. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition0.09---------------------
2. postcondition0.65---------------------
3. postcondition9.80---------------------
4. postconditionTimeout (35s) (obsolete)---0.46---------------
5. postcondition1.55---------------------
6. postcondition1.51---------------------
7. postconditionTimeout (35s) (obsolete)---Timeout (35s) (obsolete)---9.38---------
8. postconditionTimeout (35s) (obsolete)---Timeout (35s) (obsolete)---9.49---------
3. postcondition------1.15---------------
4. postcondition0.02---------------------
5. postcondition0.02---------------------
6. postcondition0.35---------------------
19. postcondition------------------------
split_goal_wp
  1. postcondition2.61---------------------
2. postcondition0.02---------------------
3. postcondition------------4.77---------
20. postcondition0.03---------------------
21. postcondition------------------------
inline_goal
  1. postcondition------0.07---------------
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------------0.24---------
VC for dfs'------------------------
split_goal_wp
  1. postcondition0.01---------------------
2. postcondition0.01---------------------
3. postcondition0.02---------------------
4. postcondition0.01---------------------
5. postcondition0.02---------------------
6. postcondition0.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. assertion3.48---------------------
9. precondition0.01---------------------
10. precondition0.02---------------------
11. precondition0.01---------------------
12. precondition0.01---------------------
13. postcondition0.01---------------------
14. postcondition0.01---------------------
15. postcondition------1.62---------------
16. postcondition------------------------
inline_goal
  1. postcondition------5.28---------------
17. postcondition0.01---------------------
18. postcondition------------------------
inline_goal
  1. postcondition0.68---------------------
19. postcondition0.01---------------------
20. precondition0.01---------------------
21. precondition0.02---------------------
22. precondition0.03---------------------
23. precondition0.01---------------------
24. precondition0.01---------------------
25. precondition0.01---------------------
26. precondition0.01---------------------
27. precondition0.01---------------------
28. precondition0.01---------------------
29. postcondition0.01---------------------
30. postcondition0.01---------------------
31. postcondition------------------------
inline_goal
  1. postcondition------2.13---------------
32. postcondition------------------------
inline_goal
  1. postcondition------0.20---------------
33. postcondition------------------------
inline_goal
  1. postcondition------------------------
inline_goal
  1. postcondition------2.40---------------
34. postcondition0.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---------------------
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---------------------