Why3 Proof Results for Project "bfs2"

Theory "bfs2.Dfs_stack2": fully verified in 6.39 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Eprover (1.9)
path_lst_occ---------
induction_pr
  path_lst_occ.10.01------
path_lst_occ.2------0.04
path_inv0.01------
whitepath_suffix0.02------
whitepath_invTimeout (15s) (obsolete)5.61---
whitepath_split_lst_occTimeout (15s) (obsolete)0.47---
6. VC for push_set0.28------
7. VC for bfs---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. postcondition0.01------
4. postcondition0.01------
5. variant decrease0.01------
6. precondition0.02------
7. precondition0.01------
8. postcondition0.01------
9. postcondition0.01------
10. postcondition0.01------
11. postcondition0.16------
12. assertion0.12------
13. variant decrease0.01------
14. preconditionTimeout (35s) (obsolete)0.09---
15. precondition0.02------
16. postcondition0.02------
17. postcondition0.01------
18. postcondition0.02------
19. postcondition1.78------
8. VC for bfs_main---------
split_goal_wp
  1. precondition0.01------
2. precondition0.01------
3. postcondition------0.17