Why3 Proof Results for Project "nbtw1"

Theory "nbtw1.Dfs_nbtw": fully verified in 0.17 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)
reachable_succ---0.07
reachable_trans------
induction_pr
  reachable_trans.10.00---
reachable_trans.20.01---
access_monotony_l0.01---
access_monotony_r0.01---
access_trans0.02---
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.01---
7. VC for dfs------
split_goal_wp
  1. postcondition0.01---
2. postcondition0.01---
3. postcondition0.01---
4. postcondition---0.05
5. variant decrease0.01---
6. precondition0.01---
7. precondition0.00---
8. precondition0.00---
9. postcondition0.01---
10. postcondition0.00---
11. postcondition0.01---
12. postcondition0.03---
13. variant decrease0.01---
14. precondition0.01---
15. precondition0.01---
16. precondition0.01---
17. assertion---5.34
18. variant decrease0.01---
19. precondition0.01---
20. precondition0.01---
21. precondition0.13---
22. postcondition0.01---
23. postcondition0.01---
24. postcondition0.02---
25. postcondition---10.53
8. VC for dfs_main0.06---