Why3 Proof Results for Project "nbtw2"

Theory "nbtw2.Dfs_nbtw": fully verified in 0.24 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Eprover (1.9)
reachable_succ------0.02
reachable_trans------0.10
access_var0.01------
access_covar0.01------
access_trans0.03------
black_to_white_path_goes_thru_gray---------
induction_pr
  black_to_white_path_goes_thru_gray.10.01------
black_to_white_path_goes_thru_gray.20.10------
7. VC for dfs---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. postcondition0.01------
4. postcondition------0.36
5. variant decrease0.01------
6. precondition0.01------
7. precondition0.00------
8. precondition0.00------
9. postcondition0.00------
10. postcondition0.00------
11. postcondition0.01------
12. postcondition0.03------
13. variant decrease0.01------
14. precondition0.01------
15. precondition0.01------
16. precondition0.01------
17. assertion---2.03---
18. variant decrease0.010.05---
19. precondition0.01------
20. precondition0.010.02---
21. precondition0.030.14---
22. postcondition0.010.08---
23. postcondition0.010.02---
24. postcondition0.020.08---
25. postcondition---14.01---
8. VC for dfs_main0.07------