Why3 Proof Results for Project "dfs22"

Theory "dfs22.DfsWhitePathSoundness": fully verified in 5.52 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Coq (8.7.2)Eprover (1.9)
whiteaccess_var0.01---------
whiteaccess_covar10.01---------
wpath_covar2------------
induction_pr
  wpath_covar2.10.01---------
wpath_covar2.20.01---------
whiteaccess_covar2---0.07------
wpath_trans------------
induction_pr
  wpath_trans.10.01---------
wpath_trans.20.01---------
whiteaccess_trans---0.16------
whiteaccess_cons---5.25------
whiteaccess_union0.02---------
path_wpathempty------------
induction_pr
  path_wpathempty.10.01---------
path_wpathempty.20.01---------
diff_inc------------
split_goal_wp
  diff_inc.10.02---------
diff_inc.20.01---------
11. VC for dfs1------------
split_goal_wp
  1. assertion0.01---------
2. index in array bounds0.01---------
3. loop invariant init0.01---------
4. loop invariant init0.01---------
5. loop invariant init0.02---------
6. loop invariant init0.01---------
7. loop invariant init0.01---------
8. loop invariant init0.01---------
9. type invariant0.01---------
10. index in array bounds------------
split_goal_wp
  1. VC for dfs1---------0.12
2. VC for dfs1---------0.12
11. precondition0.01---------
12. precondition0.01---------
13. precondition0.01---------
14. loop invariant preservation---0.48------
15. loop invariant preservation0.01---------
16. loop invariant preservation0.02---------
17. loop invariant preservation------0.69---
18. loop invariant preservation0.01---------
19. loop invariant preservation---0.17------
20. loop invariant preservation---0.27------
21. loop invariant preservation0.01---------
22. loop invariant preservation0.01---------
23. loop invariant preservation0.05---------
24. loop invariant preservation0.01---------
25. loop invariant preservation---0.14------
26. assertion------------
split_goal_wp
  1. VC for dfs10.03---------
2. VC for dfs10.09---------
27. assertion0.01---------
28. assertion------------
split_goal_wp
  1. VC for dfs10.03---------
2. VC for dfs10.11---------
3. VC for dfs10.08---------
29. type invariant0.01---------
30. index in array bounds0.01---------
31. postcondition0.05---------
32. postcondition0.04---------
33. postcondition0.01---------
12. VC for dfs_main------------
split_goal_wp
  1. array creation size0.01---------
2. loop invariant init0.01---------
3. loop invariant init0.01---------
4. loop invariant init0.01---------
5. loop invariant init0.01---------
6. loop invariant init0.01---------
7. type invariant0.01---------
8. index in array bounds---14.67---0.09
9. precondition0.01---------
10. precondition0.01---------
11. precondition0.01---------
12. loop invariant preservation---0.33------
13. loop invariant preservation0.02---------
14. loop invariant preservation0.01---------
15. loop invariant preservation------------
introduce_premises
  1. loop invariant preservation------------
inline_goal
  1. loop invariant preservation---------0.87
16. loop invariant preservation---0.14------
17. loop invariant preservation---0.17------
18. loop invariant preservation0.01---------
19. loop invariant preservation0.01---------
20. loop invariant preservation0.03---------
21. loop invariant preservation---0.11------
22. postcondition0.01---------
23. loop invariant init0.01---------
24. type invariant0.01---------
25. index in array bounds0.01---------
26. loop invariant preservation0.02---------
27. loop invariant preservation0.02---------
28. postcondition0.16---------