Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (1.30)CVC3 (2.4.1)CVC4 (1.4 noBV)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.------1.02------------------
2.22.12------------------------
3.------Timeout (55s)1.23---------------
4.---------------------------
inline_goal
  1.---------------1.20---------
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. VC for dfs1---------0.80---------------
2. VC for dfs18.01------------------------
3. VC for dfs1---------------------------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs10.11------------------------
4. VC for dfs10.31------------------------
5. VC for dfs11.15------------------------
6. VC for dfs12.94------------------------
4. precondition---------------------------
split_goal_wp
  1. precondition0.01------------------------
2. precondition0.01------------------------
3. precondition0.01------------------------
5. assertion---------------------------
split_goal_wp
  1. VC for dfs10.08------------------------
2. VC for dfs10.11------------------------
3. VC for dfs10.38------------------------
6. assertion---------11.69---Timeout (155s)---------
7. assertion------------1.13------------
8. postcondition---------------------------
inline_goal
  1. postcondition---------------------------
split_goal_wp
  1. VC for dfs1---------139.21 (obsolete)---------------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs10.12------------------------
2. VC for dfs10.11------------------------
3. VC for dfs1Timeout (35s)------0.53---------------
4. VC for dfs10.03------------------------
2. VC for dfs1---------2.21---------------
3. VC for dfs1---------------------------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs1---------1.84---------------
4. VC for dfs1---------0.21---------------
5. VC for dfs10.02------------------------
6. VC for dfs1Timeout (155s)Timeout (155s)---55.25---Timeout (155s)Timeout (155s)---Timeout (155s)
9. postcondition---------------------------
split_goal_wp
  1. postcondition0.15------------------------
2. postcondition0.03------------------------
3. postcondition---------7.13---Timeout (155s) (obsolete)------Timeout (155s) (obsolete)
10. postcondition---------------------------
inline_goal
  1. postcondition---------0.23---------------
11. postcondition0.65------------------------
12. postcondition24.49------------------------
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---------
5. VC for dfs12.23------------------------
15. assertion------------1.44------------
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 dfs1Timeout (155s) (obsolete)------Timeout (155s) (obsolete)---Timeout (155s) (obsolete)------Timeout (155s) (obsolete)
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs1---------2.44---------------
2. VC for dfs1---------0.13---------------
2. VC for dfs10.02------------------------
18. postcondition---------------------------
inline_goal
  1. postcondition---------------------------
split_goal_wp
  1. VC for dfs1Timeout (35s) (obsolete)------------Timeout (155s)---------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs10.07------------------------
2. VC for dfs16.85------------------------
3. VC for dfs1Timeout (255s)Timeout (155s)---179.45---Timeout (155s)Timeout (155s)---Timeout (155s)
4. VC for dfs10.63------------------------
2. VC for dfs1---------Timeout (35s)---------------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs10.13------0.42---5.26------0.12
2. VC for dfs1Timeout (155s)------Timeout (155s)---106.64------Timeout (155s)
3. VC for dfs19.56------1.05---Timeout (155s)------0.56
4. VC for dfs1------------------------0.13
5. VC for dfs1Timeout (155s)------1.81---Timeout (155s)------Timeout (155s)
6. VC for dfs1---------------Timeout (155s)------1.69
7. VC for dfs1Timeout (155s)------Timeout (155s)---17.50------Timeout (155s)
8. VC for dfs1Timeout (155s)------------17.69------Timeout (155s)
3. VC for dfs1---------------------------
inline_goal
  1. VC for dfs1---------------------------
split_goal_wp
  1. VC for dfs1Timeout (35s) (obsolete)------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 dfs1Timeout (35s) (obsolete)------2.07---------------
19. postcondition---------------------------
split_goal_wp
  1. postcondition0.95------------------------
2. postcondition0.02------------------------
3. postcondition---------------5.87---------
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---------------1.81---------
5. VC for dfs10.02------------------------
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------------------------
5. VC for dfs'0.01------------------------
8. assertionTimeout (35s)------13.46---Timeout (25s)---------
9. precondition0.01------------------------
10. precondition0.01------------------------
11. precondition0.01------------------------
12. precondition0.01------------------------
13. postcondition0.01------------------------
14. postcondition0.01------------------------
15. postconditionTimeout (35s)------0.33---------------
16. postcondition---------------------------
inline_goal
  1. postcondition---------5.28---------------
17. postcondition---------0.12---------------
18. postcondition---------------------------
inline_goal
  1. postcondition1.17------------------------
19. postcondition0.01------------------------
20. precondition0.01------------------------
21. precondition0.02------------------------
22. precondition0.03------------------------
23. precondition0.01------------------------
24. precondition0.01------------------------
25. precondition0.01------------------------
26. precondition0.02------------------------
27. precondition0.01------------------------
28. precondition0.01------------------------
29. postcondition0.01------------------------
30. postcondition0.01------------------------
31. postcondition---------------------------
inline_goal
  1. postcondition---------2.88---------------
32. postcondition---------------------------
inline_goal
  1. postcondition---------0.20---------------
33. postcondition---------------------------
inline_goal
  1. postconditionTimeout (55s)Timeout (25s)---96.08---Timeout (25s)Timeout (25s)---Timeout (25s)
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------------------------
5. VC for dfs'0.03------------------------
VC for tarjan---------------------------
split_goal_wp
  1. precondition0.01------------------------
2. precondition0.01------------------------
3. precondition---------------------------
inline_goal
  1. precondition---------------------------
split_goal_wp
  1. VC for tarjan0.01------------------------
2. VC for tarjan0.01------------------------
3. VC for tarjan0.04------------------------
4. VC for tarjan0.01------------------------
5. VC for tarjan0.01------------------------
6. VC for tarjan0.05------------------------
4. precondition0.01------------------------
5. assertion0.02------------------------
6. postcondition---------------------------
split_goal_wp
  1. postcondition3.18------------------------
2. postcondition0.02------------------------
3. postcondition0.02------------------------