Why3 Proof Results for Project "scc"

Theory "scc.Kosaraju": fully verified in 2.10 s

ObligationsCVC3 (2.4.1)Z3 (4.4.1)
reachable_trans0.05---
access_from_successors1.19---
access_from_extension---0.86

Theory "scc.SCCK": not fully verified

ObligationsAlt-Ergo (1.01)CVC3 (2.4.1)CVC4 (1.4)Coq (8.5pl1)Eprover (1.9)Spass (3.7)
rank_range------------------
induction_ty_lex
  1. 1.0.03---------------
simplelist_sub---0.74------------
inter_assoc0.02---------------
inter_add0.06---------------
inter_elt0.21---------------
set_elt0.25---------------
elements_add0.08---------------
simplelist_inter------------------
induction_ty_lex
  1. 1.------------------
split_goal_wp
  1. 1.------------0.18---
2. 2.0.21---------------
length_eq_cardinal------------------
induction_ty_lex
  1. 1.------------------
split_goal_wp
  1. 1.0.03---------------
2. 2.0.07---------------
elements_elt_exchange---0.24------------
elements_append_comm0.06---------------
subset_inter_subset------0.26---------
same_scc_refl------------0.080.12
same_scc_sym0.02---------------
same_scc_trans0.03---------------
cc_ext0.07---------------
scc_max------0.53---------
disjoint_scc------------------
inline_goal
  1. 1.------------------
split_goal_wp
  1. 1.------------3.94---
2. 2.------------3.92---
reverse_graph_reverse_path------------------
induction_pr
  1. 1.0.20---------------
2. 2.---------1.62------
reverse_graph_reverse_path_rev------------------
induction_pr
  1. 1.0.22---------------
2. 2.---------1.67------
reachable_before_shrink------1.15---------
reachable_before_extension------------------
inline_goal
  1. 1.0.19---------------
no_edge_out_of_cons------------------
inline_goal
  1. 1.------------------
inline_goal
  1. 1.------31.05---------
path_cross_sets------------------
induction_pr
  1. 1.---14.47------------
2. 2.------------2.08---
no_edge_out_of_no_path_out_of_in0.06---------------
no_black_to_white_no_path------------------
induction_pr
  1. 1.0.03---------------
2. 2.------------0.190.30
no_black_to_white_in_the_middle------------------
inline_goal
  1. 1.------------------
induction_pr
  1. 1.0.02---------------
2. 2.------------------
simplify_trivial_quantification_in_goal
  1. 1.---7.09------------
reachable_before_reverse---------2.53------
paths_in_set_reachable_before0.46---------------
paths_in_set_same_scc_in_set---------1.89------
wff_stack_white_extension------------0.22---
32. VC for dfs1------------------
split_goal_wp
  1. 1. postcondition0.02---------------
2. 2. postcondition0.02---------------
3. 3. postcondition---0.37------------
4. 4. postcondition0.03---------------
5. 5. precondition0.03---------------
6. 6. precondition0.03---------------
7. 7. postcondition0.03---------------
8. 8. postcondition0.04---------------
9. 9. postcondition0.35---------------
10. 10. postcondition0.03---------------
11. 11. precondition0.04---------------
12. 12. precondition------------------
inline_goal
  1. 1. precondition------------------
split_goal_wp
  1. 1. VC for dfs10.40---------------
2. 2. VC for dfs10.02---------------
3. 3. VC for dfs10.02---------------
4. 4. VC for dfs10.02---------------
5. 5. VC for dfs10.02---------------
13. 13. assertion------0.87---------
14. 14. assertion---------1.59------
15. 15. assertion3.56---------------
16. 16. assertion0.58---------------
17. 17. precondition0.04---------------
18. 18. precondition------------------
inline_goal
  1. 1. precondition------------------
split_goal_wp
  1. 1. VC for dfs1------------------
inline_goal
  1. 1. VC for dfs1------------------
split_goal_wp
  1. 1. VC for dfs10.03---------------
2. 2. VC for dfs10.96---------------
2. 2. VC for dfs10.05---------------
3. 3. VC for dfs10.05---------------
4. 4. VC for dfs10.09---------------
5. 5. VC for dfs110.55---------------
19. 19. postcondition0.03---------------
20. 20. postcondition0.80---------------
21. 21. postcondition---------1.66------
22. 22. postcondition0.06---------------
33. VC for dfs2------------------
split_goal_wp
  1. 1. postcondition0.03---------------
2. 2. postcondition0.03---------------
3. 3. postcondition0.03---------------
4. 4. postcondition0.03---------------
5. 5. precondition0.03---------------
6. 6. precondition0.03---------------
7. 7. postcondition0.03---------------
8. 8. postcondition0.05---------------
9. 9. postcondition0.04---------------
10. 10. postcondition0.03---------------
11. 11. precondition0.03---------------
12. 12. precondition0.19---------------
13. 13. precondition0.04---------------
14. 14. precondition------------------
inline_goal
  1. 1. precondition------------------
split_goal_wp
  1. 1. VC for dfs20.02---------------
2. 2. VC for dfs20.21---------------
15. 15. postcondition0.03---------------
16. 16. postcondition0.10---------------
17. 17. postcondition------------------
inline_goal
  1. 1. postcondition------------------
inline_goal
  1. 1. postcondition------------0.35---
18. 18. postcondition0.04---------------
34. VC for iter2------------------
split_goal_wp
  1. 1. postcondition0.03---------------
2. 2. postcondition0.03---------------
3. 3. precondition0.07---------------
4. 4. precondition0.42---------------
5. 5. precondition0.03---------------
6. 6. postcondition0.02---------------
7. 7. postcondition0.03---------------
8. 8. precondition------------------
split_goal_wp
  1. 1. precondition0.06---------------
9. 9. precondition0.02---------------
10. 10. assertion0.82---------------
11. 11. assertion20.81---------------
12. 12. assertion------------------
split_goal_wp
  1. 1. VC for iter21.22---------------
2. 2. VC for iter2------------0.17---
13. 13. assertion0.03---------------
14. 14. assertion------------------
inline_goal
  1. 1. assertion------------------
split_goal_wp
  1. 1. VC for iter2---0.26------------
2. 2. VC for iter2------2.91---------
15. 15. precondition------------------
inline_goal
  1. 1. precondition------3.88---------
16. 16. precondition5.04---------------
17. 17. precondition------------------
split_goal_wp
  1. 1. precondition------------------
inline_goal
  1. 1. precondition------------------
split_goal_wp
  1. 1. precondition0.08---------------
2. 2. precondition---------------0.35
2. 2. precondition0.06---------------
3. 3. precondition---------------4.89
18. 18. postcondition0.03---------------
19. 19. postcondition0.04---------------
35. VC for scc_main------------------