Why3 Proof Results for Project "dfs1"
Theory "dfs1.DfsWhitePathSoundness": fully verified in 0.32 s
Obligations | Alt-Ergo (2.0.0) | CVC4 (1.5) | Eprover (1.9) |
whitepath_id | 0.01 | --- | --- |
whitepath_sub | 0.01 | --- | --- |
whitepath_cons | 0.01 | --- | --- |
4. VC for dfs | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.01 | --- | --- |
2. postcondition | 0.01 | --- | --- |
3. postcondition | 0.01 | --- | --- |
4. variant decrease | 0.01 | --- | --- |
5. precondition | 0.01 | --- | --- |
6. precondition | 0.00 | --- | --- |
7. postcondition | 0.00 | --- | --- |
8. postcondition | 0.01 | --- | --- |
9. postcondition | 0.02 | --- | --- |
10. variant decrease | 0.01 | --- | --- |
11. precondition | 0.01 | --- | --- |
12. precondition | 0.01 | --- | --- |
13. variant decrease | 0.02 | --- | --- |
14. precondition | 0.01 | --- | --- |
15. precondition | 0.01 | --- | --- |
16. assertion | --- | --- | --- |
split_goal_wp | | | |
| 1. assertion | --- | --- | 0.12 |
2. VC for dfs | --- | --- | --- |
introduce_premises | | | |
| 1. VC for dfs | --- | --- | --- |
inline_goal | | | |
| 1. VC for dfs | --- | 0.72 | --- |
17. postcondition | 0.01 | --- | --- |
18. postcondition | 0.01 | --- | --- |
19. postcondition | --- | 2.46 | --- |
5. VC for dfs_main | --- | --- | 0.29 |