Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (1.30)CVC3 (2.4.1)CVC4 (1.4)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. variant decrease0.03---------------------------
6. postcondition0.01---------------------------
7. 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. variant decrease------------------------------
inline_goal
  1. variant decrease1.83---------------------------
2. precondition0.03---------------------------
3. precondition------------------------------
inline_goal
  1. precondition------------------0.58---------
4. 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---------------------------
5. precondition------------------------------
split_goal_wp
  1. precondition0.01---------------------------
2. precondition0.01---------------------------
3. precondition0.01---------------------------
6. assertion------------------------------
split_goal_wp
  1. VC for dfs10.08---------------------------
2. VC for dfs10.11---------------------------
3. VC for dfs10.38---------------------------
7. assertion------------11.69---Timeout (155s)---------
8. assertion---------------1.13------------
9. 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)
10. postcondition------------------------------
split_goal_wp
  1. postcondition0.15---------------------------
2. postcondition0.03---------------------------
3. postcondition------------7.13---Timeout (155s) (obsolete)------Timeout (155s) (obsolete)
11. postcondition------------------------------
inline_goal
  1. postcondition------------0.23---------------
12. postcondition0.65---------------------------
13. postcondition24.49---------------------------
14. postcondition0.01---------------------------
15. 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---------------------------
16. assertion---------------1.44------------
17. assertion------------------------------
inline_goal
  1. assertion------------------------------
split_goal_wp
  1. VC for dfs10.36---------------------------
2. VC for dfs10.03---------------------------
3. VC for dfs1------------------5.71---------
18. 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---------------------------
19. 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---------------
20. postcondition------------------------------
split_goal_wp
  1. postcondition0.95---------------------------
2. postcondition0.02---------------------------
3. postcondition------------------5.87---------
21. postcondition0.03---------------------------
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------------------1.81---------
5. VC for dfs10.02---------------------------
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. postconditionTimeout (35s)---------------------------
inline_goal
  1. postcondition------------------------------
split_goal_wp
  1. VC for dfsTimeout (35s)---0.81---------------------
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. postconditionTimeout (35s)---1.90---------------------
17. postconditionTimeout (85s)29.78Timeout (85s)------------------Timeout (85s)
18. postcondition0.01---------------------------
19. postcondition3.33---------------------------
20. postcondition0.01---------------------------
21. variant decrease0.01---------------------------
22. precondition0.01---------------------------
23. precondition0.01---------------------------
24. precondition0.03---------------------------
25. precondition0.01---------------------------
26. precondition0.01---------------------------
27. variant decrease1.30---------------------------
28. precondition0.02---------------------------
29. precondition0.04---------------------------
30. precondition0.01---------------------------
31. precondition0.02---------------------------
32. postcondition0.02---------------------------
33. postcondition0.02---------------------------
34. postconditionTimeout (35s)---------------------------
inline_goal
  1. postcondition---------18.15------------------
35. postcondition7.33---------------------------
36. postcondition34.20---------------------------
37. postcondition0.03---------------------------
38. postcondition8.72---------------------------
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---------------------------