Why3 Proof Results for Project "dfs15"

Theory "dfs15.DfsWhitePathSoundness": fully verified in 5.41 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)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.15---
whiteaccess_cons---5.17---
path_wpathempty---------
induction_pr
  path_wpathempty.10.01------
path_wpathempty.20.01------
9. VC for dfs---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. postcondition0.01------
4. postcondition0.01------
5. index in array bounds---------
split_goal_wp
  1. VC for dfs------0.04
2. VC for dfs------0.04
6. precondition0.02------
7. precondition0.01------
8. precondition0.01------
9. precondition0.01------
10. postcondition0.01------
11. postcondition0.01------
12. postcondition0.01------
13. postcondition0.03------
14. index in array bounds0.01------
15. precondition0.01------
16. precondition0.02------
17. precondition0.01------
18. precondition0.02------
19. assertion0.08------
20. assertion0.02------
21. assertion---------
split_goal_wp
  1. VC for dfs0.10------
2. VC for dfs0.07------
22. precondition0.04------
23. precondition0.01------
24. precondition0.01------
25. precondition0.02------
26. assertion0.11------
27. assertion0.12------
28. postcondition0.07------
29. postcondition0.01------
30. postcondition0.02------
31. postcondition0.44------
10. VC for dfs_main---------
split_goal_wp
  1. array creation size0.01------
2. precondition0.01------
3. precondition0.01------
4. precondition0.01------
5. precondition0.01------
6. postcondition0.01------
7. loop invariant init0.01------
8. index in array bounds0.01------
9. loop invariant preservation0.02------
10. loop invariant preservation0.01------
11. postcondition0.04------