Why3 Proof Results for Project "dag1"

Theory "dag1.DfsWhitePathGraySoundness": fully verified in 0.01 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Eprover (1.9)
paths_in---------
induction_pr
  paths_in.10.00------
paths_in.20.01------
2. VC for add_grays0.01------
3. VC for add_blacks0.00------
4. VC for dfs---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. postcondition0.01------
4. exceptional postcondition---0.46---
5. assertion0.11------
6. precondition0.01------
7. precondition0.05------
8. precondition0.06------
9. precondition---0.14---
10. postcondition0.19------
11. postcondition0.03------
12. postcondition0.02------
13. exceptional postcondition0.01------
14. precondition0.01------
15. precondition---------
introduce_premises
  1. precondition---------
inline_goal
  1. precondition---------
introduce_premises
  1. precondition---------
inline_goal
  1. precondition------0.15
16. precondition0.05------
17. precondition0.01------
18. assertion0.03------
19. precondition0.01------
20. precondition0.03------
21. precondition---------
introduce_premises
  1. precondition---------
inline_goal
  1. precondition---------
split_goal_wp
  1. precondition0.04------
2. precondition0.08------
3. precondition0.08------
4. precondition---0.08---
22. precondition---0.72---
23. postcondition0.37------
24. postcondition0.06------
25. postcondition0.01------
26. exceptional postcondition0.01------
27. exceptional postcondition0.01------
5. VC for is_acyclic---------
split_goal_wp
  1. precondition0.01------
2. precondition0.01------
3. precondition0.01------
4. precondition3.22------
5. assertion0.26------
6. postcondition0.01------
7. postcondition0.01------