Why3 Proof Results for Project "scc"

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

ObligationsAlt-Ergo (2.1.0)CVC3 (2.4.1)CVC4 (1.5)Eprover (1.9)Spass (3.5)Z3 (4.6.2)
reachable_transTimeout (15s)0.050.040.109.87Timeout (15s)
access_from_extensionTimeout (45s)---43.46Timeout (45s)------
introduce_premises
  access_from_extension.1------------------
inline_goal
  access_from_extension.1.1Timeout (15s)---13.380.020.03Timeout (15s)
access_var0.01---0.053.810.040.02
access_covar0.01---0.043.520.040.02
access_trans0.01---0.13Timeout (15s)Timeout (15s)0.02
access_from_successorsTimeout (15s)0.738.75Timeout (15s)Timeout (15s)Timeout (15s)

Theory "scc.SCCK": fully verified in 42.31 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Eprover (1.9)Spass (3.5)Z3 (4.6.2)
rank_range---------------
induction_ty_lex
  rank_range.10.030.070.09Timeout (15s)Timeout (15s)
simplelist_subTimeout (15s)0.122.74Timeout (15s)Timeout (15s)
inter_assoc0.020.06Timeout (15s)Timeout (15s)9.71
inter_add0.060.08Timeout (15s)Timeout (15s)Timeout (15s)
inter_elt0.0314.150.04Timeout (15s)Timeout (15s)
set_elt0.020.14Timeout (15s)Timeout (15s)Timeout (15s)
elements_add0.080.070.039.080.04
simplelist_inter---------------
induction_ty_lex
  simplelist_inter.1---------------
split_goal_wp
  simplelist_inter.1.1Timeout (15s)14.240.18Timeout (15s)Timeout (15s)
simplelist_inter.1.2Timeout (15s)0.50Timeout (15s)Timeout (15s)Timeout (15s)
length_eq_cardinal---------------
induction_ty_lex
  length_eq_cardinal.1---------------
split_goal_wp
  length_eq_cardinal.1.10.030.070.030.050.03
length_eq_cardinal.1.20.070.1012.44Timeout (15s)Timeout (15s)
elements_elt_exchange0.032.55Timeout (15s)Timeout (15s)Timeout (15s)
elements_append_comm0.060.11Timeout (15s)Timeout (15s)5.86
subset_inter_subsetTimeout (15s)0.090.87Timeout (15s)0.04
same_scc_reflTimeout (15s)14.200.080.12Timeout (15s)
same_scc_sym0.020.060.040.050.03
same_scc_trans0.030.060.040.090.03
cc_ext0.076.59Timeout (15s)Timeout (15s)Timeout (15s)
scc_maxTimeout (15s)0.14Timeout (15s)Timeout (15s)Timeout (15s)
disjoint_scc---------------
inline_goal
  disjoint_scc.1---------------
split_goal_wp
  disjoint_scc.1.1Timeout (15s)14.264.371.37Timeout (15s)
disjoint_scc.1.2Timeout (15s)14.374.371.38Timeout (15s)
wf_stack_white_extensionTimeout (15s)14.130.09Timeout (15s)Timeout (15s)
reverse_path---------------
induction_pr
  reverse_path.10.0214.410.050.09Timeout (15s)
reverse_path.20.081.27Timeout (15s)Timeout (15s)Timeout (15s)
reverse_pathG2---------------
induction_pr
  reverse_pathG2.10.0214.170.050.09Timeout (15s)
reverse_pathG2.20.070.875.09Timeout (15s)Timeout (15s)
reachable_before_pop0.310.83Timeout (15s)Timeout (15s)Timeout (15s)
reachable_before_push0.030.21Timeout (15s)Timeout (15s)Timeout (15s)
reachable_before_reverse---------------
split_goal_wp
  reachable_before_reverse.10.0215.32Timeout (15s)Timeout (15s)Timeout (15s)
reachable_before_reverse.2---------------
introduce_premises
  reachable_before_reverse.2.1---------------
inline_goal
  reachable_before_reverse.2.1.1---------------
inline_goal
  reachable_before_reverse.2.1.1.10.350.15Timeout (15s)Timeout (15s)Timeout (15s)
no_edge_out_pushTimeout (15s)0.30Timeout (15s)Timeout (15s)Timeout (15s)
path_cross_sets---------------
induction_pr
  path_cross_sets.1Timeout (15s)0.230.57Timeout (15s)0.07
path_cross_sets.2Timeout (15s)3.080.71Timeout (15s)Timeout (15s)
no_edge_out_no_path_out0.021.05Timeout (15s)Timeout (15s)0.05
no_black_to_white_no_path_out_of_blacksG2---------------
induction_pr
  no_black_to_white_no_path_out_of_blacksG2.10.010.040.020.090.03
no_black_to_white_no_path_out_of_blacksG2.20.040.140.070.20Timeout (15s)
no_black_to_white_convex_diffG20.04Timeout (15s)Timeout (15s)Timeout (15s)Timeout (15s)
convex_paths_closed_in_sccG2---------------
introduce_premises
  convex_paths_closed_in_sccG2.1---------------
split_goal_wp
  convex_paths_closed_in_sccG2.1.10.020.150.050.280.03
convex_paths_closed_in_sccG2.1.2Timeout (15s)0.22Timeout (15s)Timeout (15s)Timeout (15s)
31. VC for dfs1---------------
split_goal_wp
  1. postcondition0.020.040.020.080.03
2. postcondition0.020.080.050.110.03
3. postconditionTimeout (15s)0.110.070.12Timeout (15s)
4. postcondition0.030.060.020.080.03
5. precondition0.030.080.060.110.04
6. precondition0.030.040.020.080.03
7. postcondition0.030.040.020.090.02
8. postcondition0.040.13Timeout (15s)Timeout (15s)0.06
9. postcondition0.020.100.125.680.04
10. postcondition0.030.040.020.090.02
11. precondition0.040.080.060.110.03
12. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for dfs10.060.89Timeout (15s)Timeout (15s)Timeout (15s)
2. VC for dfs10.020.040.020.080.02
3. VC for dfs10.020.040.020.080.02
4. VC for dfs10.020.040.020.080.02
5. VC for dfs10.020.040.020.080.02
13. assertion0.160.211.69Timeout (15s)Timeout (15s)
14. assertion---------------
split_goal_wp
  1. VC for dfs10.030.190.040.444.71
2. VC for dfs10.060.160.20Timeout (15s)Timeout (15s)
15. assertion---------------
split_goal_wp
  1. VC for dfs1Timeout (15s)4.18Timeout (15s)Timeout (15s)Timeout (15s)
2. VC for dfs1Timeout (15s)4.18Timeout (15s)Timeout (15s)Timeout (15s)
16. precondition0.040.100.090.130.04
17. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for dfs1---------------
inline_goal
  1. VC for dfs1---------------
split_goal_wp
  1. VC for dfs10.070.30Timeout (15s)Timeout (15s)0.08
2. VC for dfs10.030.090.050.100.04
3. VC for dfs10.030.110.060.360.05
4. VC for dfs1Timeout (15s)5.34Timeout (15s)Timeout (15s)Timeout (15s)
2. VC for dfs10.091.07Timeout (15s)Timeout (15s)0.54
3. VC for dfs10.030.120.070.510.07
4. VC for dfs10.075.67Timeout (15s)Timeout (15s)0.57
5. VC for dfs1---------------
inline_goal
  1. VC for dfs1---------------
introduce_premises
  1. VC for dfs1---------------
inline_goal
  1. VC for dfs1---------------
split_goal_wp
  1. VC for dfs10.040.090.060.280.05
2. VC for dfs1High Failure50.06Timeout (55s)Timeout (55s)Timeout (55s)
18. postcondition0.030.050.020.090.02
19. postcondition0.290.29Timeout (15s)Timeout (15s)0.13
20. postconditionHigh Failure51.44Timeout (55s)Timeout (55s)29.80
21. postcondition0.060.288.910.280.06
32. VC for dfs2---------------
split_goal_wp
  1. postcondition0.030.040.020.080.03
2. postcondition0.100.080.060.100.03
3. postcondition0.020.090.07Timeout (15s)0.03
4. postcondition0.030.060.020.080.03
5. precondition0.030.080.060.100.03
6. precondition0.030.040.020.080.03
7. assertion0.120.16Timeout (15s)Timeout (15s)Timeout (15s)
8. postcondition0.030.040.020.080.03
9. postcondition0.050.11Timeout (15s)Timeout (15s)0.04
10. postcondition0.040.090.100.110.04
11. postcondition0.030.040.020.080.03
12. precondition0.040.080.060.100.03
13. precondition0.030.040.020.080.03
14. precondition0.030.090.060.110.04
15. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for dfs20.010.11Timeout (15s)Timeout (15s)0.05
2. VC for dfs20.040.040.020.090.02
3. VC for dfs20.020.120.070.75Timeout (15s)
4. VC for dfs20.060.25Timeout (15s)Timeout (15s)Timeout (15s)
16. assertion0.040.25Timeout (15s)Timeout (15s)Timeout (15s)
17. postcondition0.030.040.020.090.03
18. postcondition0.030.15Timeout (15s)Timeout (15s)0.05
19. postcondition0.2414.61Timeout (15s)Timeout (15s)Timeout (15s)
20. postcondition0.040.150.120.180.05
33. VC for iter2---------------
split_goal_wp
  1. postcondition0.030.050.020.090.04
2. postcondition0.030.080.070.120.04
3. postcondition0.020.100.070.120.04
4. postcondition0.010.080.020.090.04
5. precondition0.070.19Timeout (15s)Timeout (15s)0.06
6. precondition0.080.574.48Timeout (15s)Timeout (15s)
7. precondition0.030.080.070.140.04
8. postcondition0.020.050.020.100.02
9. postcondition0.030.080.070.140.04
10. postcondition0.030.150.11Timeout (15s)0.05
11. postcondition0.010.050.020.100.02
12. precondition---------------
split_goal_wp
  1. precondition0.060.413.88Timeout (15s)0.14
13. precondition0.020.080.040.130.04
14. assertion---------------
split_goal_wp
  1. assertion0.130.49Timeout (15s)Timeout (15s)0.41
2. assertion0.050.25Timeout (15s)Timeout (15s)0.09
3. assertion0.020.110.070.150.04
4. VC for iter20.4114.49Timeout (15s)Timeout (15s)Timeout (15s)
5. VC for iter20.020.090.040.140.04
15. assertion---------------
split_goal_wp
  1. VC for iter20.1214.704.251.990.51
2. VC for iter20.040.190.170.170.06
16. assertion0.030.12Timeout (15s)0.150.05
17. assertion---------------
inline_goal
  1. assertion---------------
split_goal_wp
  1. VC for iter20.020.090.040.160.04
2. VC for iter20.030.120.08Timeout (15s)0.04
3. VC for iter2Timeout (15s)1.302.53Timeout (15s)Timeout (15s)
18. precondition---------------
inline_goal
  1. preconditionTimeout (15s)14.35Timeout (15s)Timeout (15s)1.16
19. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for iter20.010.040.020.080.02
2. VC for iter20.020.080.050.100.04
3. VC for iter20.080.280.27Timeout (15s)0.11
4. VC for iter20.080.170.060.350.09
20. precondition---------------
split_goal_wp
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. precondition0.010.120.080.180.04
2. precondition0.080.120.080.180.04
3. precondition0.070.280.750.17Timeout (15s)
2. precondition0.060.220.080.16Timeout (15s)
3. preconditionTimeout (15s)2.052.762.72Timeout (15s)
21. postcondition0.030.050.020.100.02
22. postcondition0.040.090.070.150.04
23. postcondition0.030.191.30Timeout (15s)0.06
24. postcondition0.020.090.090.160.04
34. VC for scc_main---------------
split_goal_wp
  1. precondition0.010.060.020.070.03
2. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for scc_main0.020.090.14Timeout (15s)Timeout (15s)
2. VC for scc_main0.010.080.030.090.04
3. VC for scc_main0.010.090.060.090.04
4. VC for scc_main0.010.090.050.100.04
5. VC for scc_mainTimeout (15s)0.170.44Timeout (15s)0.05
3. precondition0.060.13Timeout (15s)6.290.06
4. precondition0.070.120.064.390.05
5. precondition---------------
split_goal_wp
  1. precondition0.010.080.020.100.04
2. precondition0.010.080.020.090.04
3. precondition0.020.140.070.130.05
6. postcondition---------------
split_goal_wp
  1. postcondition0.020.080.040.120.04
2. postcondition0.020.120.080.480.06
3. postcondition0.490.740.141.750.06