Why3 Proof Results for Project "dfs6"

Theory "dfs6.DfsWhitePathSoundness": fully verified in 4.09 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Coq (8.7.1)Eprover (1.9)Z3 (4.4.0)
whiteaccess_var0.01------------
whiteaccess_covar10.01------------
wpath_covar2---------------
induction_pr
  wpath_covar2.1---0.04---------
wpath_covar2.2---0.05---------
whiteaccess_covar2---0.05---------
wpath_trans---------------
induction_pr
  wpath_trans.10.01------------
wpath_trans.2---------0.03---
whiteaccess_trans---0.14---------
whiteaccess_cons---3.310.57------
8. VC for dfs---------------
split_goal_wp
  1. postcondition------------0.02
2. postcondition------------0.02
3. postcondition------------0.02
4. variant decrease------------0.02
5. precondition------------0.02
6. precondition------------0.02
7. postcondition------------0.02
8. postcondition------------0.02
9. postcondition------------0.02
10. variant decrease------------0.02
11. precondition------------0.02
12. precondition------------0.02
13. assertion------------0.05
14. assertion------------0.02
15. assertion---------------
split_goal_wp
  1. VC for dfs0.28------------
2. VC for dfs0.08------------
16. variant decrease------------0.02
17. precondition------------0.02
18. precondition------------0.02
19. assertion0.93------------
20. assertion------------0.03
21. postcondition------------0.03
22. postcondition------------0.02
23. postcondition---0.67---------
9. VC for dfs_main---------------
split_goal_wp
  1. precondition0.01------------
2. precondition0.01------------
3. postcondition0.02------------