Why3 Proof Results for Project "dfs1"

Theory "dfs1.DfsWhitePathSoundness": fully verified in 3.96 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)
whiteaccess_var0.01---
whiteaccess_covar10.01---
wpath_covar2Timeout (15s)---
induction_pr
  wpath_covar2.10.01---
wpath_covar2.20.01---
whiteaccess_covar2Timeout (15s)0.06
wpath_transTimeout (15s)14.94
induction_pr
  wpath_trans.10.01---
wpath_trans.20.01---
whiteaccess_transTimeout (15s)0.14
whiteaccess_consTimeout (15s)3.74
8. VC for dfs------
split_goal_wp
  1. precondition0.01---
2. precondition0.01---
3. postcondition0.01---
4. postcondition0.01---
5. postcondition0.01---
6. precondition0.01---
7. precondition0.01---
8. assertion0.04---
9. assertion0.01---
10. assertion------
split_goal_wp
  1. VC for dfs0.09---
2. VC for dfs0.05---
11. precondition0.01---
12. precondition0.01---
13. assertion0.16---
14. assertion0.04---
15. postcondition0.04---
16. postcondition0.01---
17. postcondition0.21---
18. postcondition0.01---
19. postcondition0.01---
20. postcondition0.01---
9. VC for dfs_main------
split_goal_wp
  1. precondition0.01---
2. precondition0.01---
3. postcondition0.02---