Why3 Proof Results for Project "nbtw1"

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

ObligationsAlt-Ergo (2.0.0)Alt-Ergo (2.1.0)CVC4 (1.5)
reachable_succ------0.07
reachable_trans---------
induction_pr
  reachable_trans.10.00------
reachable_trans.20.01------
access_var---0.01---
access_covar---0.01---
access_trans---0.02---
black_to_white_path_goes_thru_gray---------
induction_pr
  black_to_white_path_goes_thru_gray.1---0.01---
black_to_white_path_goes_thru_gray.2---0.01---
7. VC for dfs---------
split_goal_wp
  1. postcondition---0.01---
2. postcondition---0.01---
3. postcondition---0.01---
4. postcondition------0.05
5. variant decrease---0.01---
6. precondition---0.01---
7. precondition---0.00---
8. precondition---0.00---
9. postcondition---0.01---
10. postcondition---0.00---
11. postcondition---0.01---
12. postcondition---0.03---
13. variant decrease---0.01---
14. precondition---0.01---
15. precondition---0.01---
16. precondition---0.01---
17. assertion------3.93
18. variant decrease---0.01---
19. precondition---0.01---
20. precondition---0.01---
21. precondition---0.13---
22. postcondition---0.01---
23. postcondition---0.01---
24. postcondition---0.02---
25. postcondition------8.35
8. VC for dfs_main---0.06---