Why3 Proof Results for Project "nbtw2"

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

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Eprover (1.9)
reachable_succ------0.02
reachable_trans------0.10
access_monotony_l0.01------
access_monotony_r0.01---5.81
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.2------0.07
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.150.14---
22. postcondition0.010.08---
23. postcondition0.010.02---
24. postcondition0.020.08---
25. postcondition---12.36---
8. VC for dfs_main0.07------