Why3 Proof Results for Project "dfs6"

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

ObligationsAlt-Ergo (2.0.0)Alt-Ergo (2.1.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------------------
split_goal_wp
  1. VC for dfs---0.06------------
2. VC for dfs---0.08------------
15. variant decrease---------------0.02
16. precondition---------------0.02
17. precondition---------------0.02
18. assertion---0.11------------
19. assertion---------------0.03
20. postcondition---------------0.03
21. postcondition---------------0.02
22. postcondition------0.67---------
9. VC for dfs_main------------------
split_goal_wp
  1. precondition0.01---------------
2. precondition0.01---------------
3. postcondition0.02---------------