Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (2.2.0)Alt-Ergo (2.3.0)CVC4 (1.5)Coq (8.7.2)Eprover (1.9)Spass (3.5)Z3 (4.6.2)Z3 (4.6.3)
lmem_dec0.00---------------------
inter_com------0.05---------------
inter_add_l0.01---------------------
inter_not_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---------------------
set_of_elt------------------------
split_goal_wp
  set_of_elt.10.02---------------------
set_of_elt.2---------------2.50------
elt_set_of------------0.22---------
subset_set_of0.04---------------------
elts_cons0.03---------------------
elts_app0.02---------------------
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.22---------------
snoc_app0.02---------------------
precedes_mem0.05---------------------
head_precedes------0.10---------------
precedes_tail------1.50---------------
tail_not_precedes0.02---------------------
split_list_precedes------7.88---------------
precedes_refl0.02---------------------
precedes_append_left0.05---------------------
precedes_append_left_iff------------------------
induction_ty_lex
  precedes_append_left_iff.1------------------------
split_goal_wp
  precedes_append_left_iff.1.10.02---------------------
precedes_append_left_iff.1.20.02---------------------
precedes_append_left_iff.1.30.02---------------------
precedes_append_left_iff.1.40.01---------------------
precedes_append_right0.80---------------------
precedes_append_right_iff------------------------
induction_ty_lex
  precedes_append_right_iff.1------------------------
split_goal_wp
  precedes_append_right_iff.1.10.02---------------------
precedes_append_right_iff.1.20.02---------------------
precedes_append_right_iff.1.30.06---------------------
precedes_append_right_iff.1.40.01---------------------
simplelist_tl------0.12---------------
simplelist_split------------------------
induction_ty_lex
  simplelist_split.1------------------------
split_goal_wp
  simplelist_split.1.1------0.59---------------
simplelist_split.1.2------0.62---------------
simplelist_split.1.3------0.91---------------
simplelist_split.1.4------0.73---------------
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------0.69---------------
simplelist_length------------------------
induction_ty_lex
  simplelist_length.1------------------------
split_goal_wp
  simplelist_length.1.10.01---------------------
simplelist_length.1.20.01---------------------
precedes_antisym0.34---------------------
precedes_trans------------------------
induction_ty_lex
  precedes_trans.1------------------------
split_goal_wp
  precedes_trans.1.1------3.59---------------
reachable_refl------------0.03---------
reachable_trans------0.18---------------
xpath_xedge------------------------
induction_pr
  xpath_xedge.10.01---------------------
xpath_xedge.2------------0.06---------
same_scc_refl------------0.07---------
same_scc_sym0.01---------------------
same_scc_trans0.02---------------------
subscc_add0.04---------------------
scc_max------0.32---------------
subscc_after_last_gray------------------------
split_goal_wp
  subscc_after_last_gray.1------0.50---------------
subscc_after_last_gray.20.04---------------------
subscc_after_last_gray.3Timeout (45s) (obsolete)---19.29---------------
subscc_after_last_gray.4Timeout (45s) (obsolete)---0.42---Timeout (45s) (obsolete)---Timeout (45s) (obsolete)---
subscc_after_last_gray.5Timeout (45s) (obsolete)---2.42---Timeout (45s) (obsolete)---Timeout (45s) (obsolete)---
subscc_after_last_gray.6------------------------
inline_goal
  subscc_after_last_gray.6.1------------0.22---------
wf_color_postcond_split------0.36---------------
wf_color_sccs------0.32---------------
wf_color_3_cases------0.30---------------
num_lmemTimeout (45s) (obsolete)---2.88---------------
num_rank_strict------------------------
split_goal_wp
  num_rank_strict.1------0.32---------------
num_rank_strict.20.03---------------------
num_rank_strict.3------0.30---------------
simplelist_x_prec_strict_y'---0.54------------------
51. VC for split------------------------
split_goal_wp
  1. postcondition---0.01------------------
2. postcondition---0.01------------------
3. postcondition---0.01------------------
4. postcondition------0.29---------------
5. variant decrease---0.02------------------
6. postcondition---0.01------------------
7. postcondition---0.05------------------
52. VC for add_stack_incr---0.01------------------
53. VC for add_black---0.02------------------
54. VC for set_infty---0.03------------------
55. VC for dfs1------------------------
split_goal_wp
  1. variant decrease---0.07------------------
2. precondition---0.02------------------
3. precondition------------------------
inline_goal
  1. precondition------------1.69---------
4. precondition------------------------
introduce_premises
  1. precondition------------------------
inline_goal
  1. precondition------------------------
split_goal_wp
  1. precondition---1.08------------------
2. precondition------------------------
introduce_premises
  1. precondition------------------------
inline_goal
  1. precondition------------------------
split_goal_wp
  1. preconditionTimeout (45s) (obsolete)---1.17---------------
2. precondition---0.06------------------
3. precondition---0.81------------------
4. precondition---0.22------------------
5. precondition---0.46------------------
6. precondition---0.27------------------
7. preconditionTimeout (45s) (obsolete)---1.20---------------
8. precondition------1.40---------------
3. precondition---0.06------------------
4. precondition---0.34------------------
5. precondition------16.17---------------
6. precondition------12.02---------------
7. precondition---0.03------------------
8. precondition---0.03------------------
9. precondition---0.03------------------
5. assertion------0.41---------------
6. assertion------13.38---------------
7. postcondition------------------------
introduce_premises
  1. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs1------------------------
introduce_premises
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1---1.08------------------
2. VC for dfs1------1.13---------------
3. VC for dfs1---3.92------------------
4. VC for dfs1------1.74---------------
2. VC for dfs1------29.09---------------
3. VC for dfs1---1.41------------------
4. VC for dfs1---0.07------------------
5. VC for dfs1---0.50------------------
6. VC for dfs1------5.92---------------
7. VC for dfs1---2.881.85---------------
8. VC for dfs1---0.310.33---------------
9. VC for dfs1---------------------10.23
10. VC for dfs1---------1.19------------
11. VC for dfs1---0.310.59---------------
12. VC for dfs1---0.030.28---------------
13. VC for dfs1---0.190.67---------------
14. VC for dfs1---1.220.81---------------
8. postcondition------0.24---------------
9. postcondition------0.63---------------
10. postcondition------1.77---------------
11. postcondition------------------------
inline_goal
  1. postcondition---4.85------------------
12. assertion------------------------
split_goal_wp
  1. VC for dfs1---0.19------------------
2. VC for dfs1---0.23------------------
3. VC for dfs1---7.96------------------
13. assertion------------------------
introduce_premises
  1. assertion------------------------
inline_goal
  1. assertion------0.51---------------
14. assertion---------2.22------------
15. assertion------------------------
inline_goal
  1. assertion------------------------
split_goal_wp
  1. VC for dfs1------2.80---------------
2. VC for dfs1---0.17------------------
3. VC for dfs1------------7.88---------
16. assertion------------------------
split_goal_wp
  1. assertion---------------------0.49
17. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. postcondition------------------------
introduce_premises
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1---1.93------------------
2. VC for dfs1---------------------2.18
3. VC for dfs1------------------------
introduce_premises
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1---Timeout (45s)50.25------------Timeout (45s)
2. VC for dfs1---28.84------------------
4. VC for dfs1---8.28------------------
2. postcondition------------------------
introduce_premises
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------------------------
split_goal_wp
  1. VC for dfs1---13.09------------------
2. VC for dfs1---1.98------------------
3. VC for dfs1---3.49------------------
4. VC for dfs1---2.02------------------
5. VC for dfs1------17.01---------------
6. VC for dfs1---2.14------------------
7. VC for dfs1------------------------
split_all_full
  1. VC for dfs1---13.12------------------
8. VC for dfs1------------------------
split_all_full
  1. VC for dfs1---14.46------------------
3. postcondition---14.70------------------
4. postcondition---0.03------------------
5. postcondition---Timeout (45s)43.41------------Timeout (45s)
6. postcondition------------------------
split_all_full
  1. postcondition------------------------
introduce_premises
  1. VC for dfs1------------------------
inline_goal
  1. VC for dfs1------65.07---------------
7. postcondition---2.9410.06---------------
8. postcondition---0.75------------------
9. postcondition------------------------
split_all_full
  1. postcondition------------------------
introduce_premises
  1. VC for dfs1------------22.41---------
10. postcondition------------0.31---------
11. postcondition---0.101.11---------------
12. postcondition---0.101.13---------------
13. postcondition---------------------3.65
14. postcondition---0.04------------------
18. postcondition---0.02------------------
19. postcondition---0.48------------------
20. postcondition------------------------
inline_goal
  1. postcondition---0.01------------------
21. postcondition---1.65------------------
56. VC for dfs------------------------
split_goal_wp
  1. postcondition------------------------
introduce_premises
  1. postcondition------------------------
inline_goal
  1. postcondition------------------------
split_goal_wp
  1. VC for dfs---0.02------------------
2. VC for dfs---0.02------------------
3. VC for dfs---0.02------------------
4. VC for dfs---0.02------------------
5. VC for dfs---0.05------------------
6. VC for dfs---0.35------------------
7. VC for dfs---0.02------------------
8. VC for dfs---0.02------------------
9. VC for dfs---0.03------------------
10. VC for dfs------0.24---------------
11. VC for dfs---0.02------------------
12. VC for dfs---0.02------------------
13. VC for dfs---0.01------------------
14. VC for dfs---0.02------------------
2. postcondition---0.02------------------
3. postcondition---0.02------------------
4. postcondition---0.02------------------
5. postcondition---0.64------------------
6. variant decrease------0.27---------------
7. precondition---0.02------------------
8. precondition---0.02------------------
9. precondition---0.02------------------
10. postcondition------------------------
introduce_premises
  1. VC for dfs------------------------
inline_goal
  1. VC for dfs------------------------
split_goal_wp
  1. VC for dfs---0.03------------------
2. VC for dfs---0.03------------------
3. VC for dfs---0.03------------------
4. VC for dfs---0.03------------------
5. VC for dfs---0.17------------------
6. VC for dfs---0.96------------------
7. VC for dfs---0.05------------------
8. VC for dfs---0.06------------------
9. VC for dfs---0.06------------------
10. VC for dfs---------------------0.04
11. VC for dfs---0.04------------------
12. VC for dfs---0.04------------------
13. VC for dfs---0.04------------------
14. VC for dfs---0.04------------------
11. postcondition---2.31------------------
12. postcondition------1.74---------------
13. postcondition------------------------
introduce_premises
  1. VC for dfs------------------------
inline_goal
  1. VC for dfs---2.75------------------
14. postcondition---0.02------------------
15. variant decrease------0.06---------------
16. precondition---0.02------------------
17. precondition---0.02------------------
18. precondition---0.15------------------
19. precondition---0.02------------------
20. variant decrease------24.74 (obsolete)---------------
inline_all
  1. variant decrease------------------------
split_all_full
  1. variant decrease---0.24------------------
2. variant decrease---0.09------------------
3. variant decrease---0.09------------------
4. variant decrease---0.23------------------
5. variant decrease---0.24------------------
6. variant decreaseTimeout (25s) (obsolete)------------------0.56
7. variant decrease---0.08------------------
8. variant decrease---0.08------------------
9. variant decrease---0.26------------------
10. variant decrease---0.76------------------
21. precondition---0.02------------------
22. precondition---0.04------------------
23. precondition---0.02------------------
24. postcondition------------------------
split_goal_wp
  1. postcondition---0.02------------------
2. postcondition------------------------
introduce_premises
  1. VC for dfs------------------------
inline_goal
  1. VC for dfs------------------------
split_goal_wp
  1. VC for dfs------------------------
inline_goal
  1. VC for dfs------------------------
inline_all
  1. VC for dfs---------------------0.43
2. VC for dfs---0.04------------------
3. VC for dfs---0.04------------------
4. VC for dfs---0.21------------------
5. VC for dfs---0.04------------------
25. postcondition---0.10------------------
26. postcondition------3.72---------------
27. postcondition---1.13------------------
28. postcondition------6.49---------------
57. VC for tarjan------------------------
split_goal_wp
  1. precondition---0.01------------------
2. precondition---0.01------------------
3. precondition------------------------
inline_goal
  1. precondition------------------------
split_goal_wp
  1. precondition---0.05------------------
2. precondition---0.04------------------
3. precondition---0.01------------------
4. precondition---0.01------------------
5. precondition---0.01------------------
6. precondition---0.01------------------
7. precondition---0.02------------------
8. precondition---0.02------------------
9. precondition---0.02------------------
4. assertion---0.15------------------
5. postcondition------------------------
split_goal_wp
  1. postcondition---1.66------------------
2. postcondition---0.02------------------
3. postcondition---0.15------------------