Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (2.2.0)CVC3 (2.4.1)CVC4 (1.5)Coq (8.7.2)Eprover (1.9)Spass (3.5)Z3 (4.4.0)Z3 (4.6.3)
lmem_dec0.00---------------------
inter_com---0.04------------------
inter_not_add_l0.01---------------------
inter_add_l0.01---------------------
diff_add_l0.01---------------------
diff_add_r0.02---------------------
subset_add_r0.01---------------------
union_add_l0.01---------------------
union_add_r0.01---------------------
union_com0.01---------------------
union_var_l0.01---------------------
union_var_r0.01---------------------
elts_cons0.03---------------------
elts_app0.02---------------------
set_of_elt------------------------
split_goal_wp
  set_of_elt.10.02---------------------
set_of_elt.2---------------2.44------
elt_set_of------------0.17---------
subset_set_of0.04---------------------
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.24---------------
list_assoc_cons------0.06---------------
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.60---------------
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.10---------------
simplelist_split------------------------
induction_ty_lex
  simplelist_split.1------------------------
split_goal_wp
  simplelist_split.1.1------0.09---------------
simplelist_split.1.2------0.11---------------
simplelist_split.1.3------1.46---------------
simplelist_split.1.4------1.13---------------
simplelist_app_disjoint------------------------
induction_ty_lex
  simplelist_app_disjoint.1------------------------
split_goal_wp
  simplelist_app_disjoint.1.1------------0.09---------
simplelist_app_disjoint.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---------------------
simplelist_hd_max_rank0.02---------------------
rank_before_suffix0.18---------------------
reachable_trans---0.19------------------
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.23---------------
subscc_after_last_gray------------------------
split_goal_wp
  subscc_after_last_gray.1------0.48---------------
subscc_after_last_gray.22.01---------------------
subscc_after_last_gray.3------1.63---------------
subscc_after_last_gray.4------------------------
inline_goal
  subscc_after_last_gray.4.1------------1.20---------
wf_color_postcond_split------0.31---------------
wf_color_sccs------0.39---------------
wf_color_3_cases------0.16---------------
42. VC for split------------------------
split_goal_wp
  1. postcondition0.01---------------------
2. postcondition0.01---------------------
3. postcondition0.01---------------------
4. postcondition---0.20------------------
5. variant decrease0.03---------------------
6. postcondition0.01---------------------
7. postcondition0.05---------------------
43. VC for add_stack_incr0.01---------------------
44. VC for add_blacks0.01---------------------
45. VC for set_infty0.02---------------------
46. VC for dfs1------------------------
split_goal_wp
  1. variant decrease------------------------
introduce_premises
  1. variant decrease------------------------
inline_goal
  1. variant decrease0.08---------------------
2. precondition0.03---------------------
3. precondition------------------------
inline_goal
  1. precondition------------0.90---------
4. precondition------------------------
inline_goal
  1. precondition------------------------
split_goal_wp
  1. precondition0.18---------------------
2. precondition------------------------
inline_goal
  1. precondition------------------------
split_goal_wp
  1. precondition0.11---------------------
2. precondition0.05---------------------
3. precondition0.07---------------------
4. precondition0.06---------------------
5. precondition0.11---------------------
6. precondition0.06---------------------
7. precondition------21.89---------------
8. precondition------20.68---------------
3. precondition0.06---------------------
4. precondition0.19---------------------
5. precondition3.27---------------------
6. precondition1.43---------------------
5. precondition------------------------
split_goal_wp
  1. precondition0.01---------------------
2. precondition0.01---------------------
3. precondition0.01---------------------
6. assertion------------------------
split_goal_wp
  1. VC for dfs10.66---------------------
2. VC for dfs10.66---------------------
3. VC for dfs11.59---------------------
7. assertion------9.98---------------
8. assertion---------1.13------------
9. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition------18.57---------------
2. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition------0.31---------------
2. postcondition------19.12---------------
3. postcondition------0.25---------------
4. postcondition------0.25---------------
5. postcondition------1.33---------------
6. postcondition------1.09---------------
7. postcondition0.08---------4.73---------
8. postcondition0.08---------4.62---------
3. postcondition------1.67---------------
4. postcondition0.02---------------------
5. postcondition------0.21---------------
6. postcondition------22.75---------------
10. postcondition------------------------
split_goal_wp
  1. postcondition0.28---------------------
2. postcondition0.03---------------------
3. postcondition---------------------4.56
11. postcondition------------------------
inline_goal
  1. postcondition------0.23---------------
12. postcondition10.04---------------------
13. postcondition------1.69---------------
14. postcondition0.01---------------------
15. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs1------------1.11---------
2. VC for dfs10.13---------------------
3. VC for dfs10.02---------------------
4. VC for dfs1------------0.33---------
5. VC for dfs10.86---------------------
16. assertion---------1.12------------
17. assertion------------------------
inline_goal
  1. assertion------------------------
split_goal_wp
  1. VC for dfs1------0.35---------------
2. VC for dfs10.03---------------------
3. VC for dfs1------------5.38---------
18. assertion------------------------
split_goal_wp
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1------0.73---------------
2. VC for dfs1------0.13---------------
2. VC for dfs10.02---------------------
19. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs10.84---------------------
2. VC for dfs16.54---------------------
3. VC for dfs1------151.47---------------
4. VC for dfs10.93---------------------
2. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs10.13---0.42---7.21---0.12---
2. VC for dfs1------------52.39---------
3. VC for dfs10.38---0.41---------0.56---
4. VC for dfs1------------------0.13---
5. VC for dfs1------2.57---------------
6. VC for dfs1------------------8.39---
7. VC for dfs1------------14.59---------
8. VC for dfs1------------16.99---------
3. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1------1.49---------------
4. VC for dfs10.02---------------------
5. VC for dfs10.02---------------------
6. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1------2.65---------------
20. postcondition------------------------
split_goal_wp
  1. postcondition0.41---------------------
2. postcondition0.02---------------------
3. postcondition------------8.28---------
21. postcondition0.18---------------------
22. postcondition------------------------
inline_goal
  1. postcondition------0.07---------------
23. postcondition0.03---------------------
24. postcondition0.02---------------------
25. 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.33---------
5. VC for dfs10.02---------------------
47. VC for dfs------------------------
split_goal_wp
  1. postcondition0.01---------------------
2. postcondition0.01---------------------
3. postcondition0.01---------------------
4. postcondition0.01---------------------
5. postcondition0.01---------------------
6. postcondition0.01---------------------
7. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs------0.18---------------
2. VC for dfs0.01---------------------
3. VC for dfs0.01---------------------
4. VC for dfs0.01---------------------
5. VC for dfs0.01---------------------
8. assertion------------------------
split_goal_wp
  1. VC for dfs0.06---------------------
2. VC for dfs------------------0.19---
9. variant decrease0.02---------------------
10. precondition0.01---------------------
11. precondition0.01---------------------
12. precondition0.01---------------------
13. precondition0.01---------------------
14. postcondition0.01---------------------
15. postcondition0.01---------------------
16. postcondition------1.08---------------
17. postcondition---19.67------------------
18. postcondition0.01---------------------
19. postcondition0.31---------------------
20. postcondition0.01---------------------
21. variant decrease0.01---------------------
22. precondition0.01---------------------
23. precondition0.01---------------------
24. precondition0.03---------------------
25. precondition0.01---------------------
26. precondition0.01---------------------
27. variant decrease------------------------
split_all_full
  1. variant decrease0.02---------------------
2. variant decrease0.02---------------------
3. variant decrease0.02---------------------
4. variant decrease0.02---------------------
5. variant decrease0.02---------------------
6. variant decrease------------------------
inline_all
  1. variant decrease---------------------0.36
7. variant decrease0.02---------------------
8. variant decrease0.02---------------------
9. variant decrease0.02---------------------
10. variant decrease0.02---------------------
28. precondition0.02---------------------
29. precondition0.04---------------------
30. precondition0.01---------------------
31. precondition0.02---------------------
32. postcondition0.02---------------------
33. postcondition0.02---------------------
34. postcondition------------------------
inline_goal
  1. postcondition------2.46---------------
35. postcondition0.39---------------------
36. postcondition2.40---------------------
37. postcondition0.03---------------------
38. postcondition------------------------
introduce_premises
  1. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs11.80---------------------
2. VC for dfs0.03---------------------
3. VC for dfs0.03---------------------
4. VC for dfs0.10---------------------
5. VC for dfs0.03---------------------
48. 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.23---------------------
2. postcondition0.02---------------------
3. postcondition0.02---------------------