Why3 Proof Results for Project "dfs8"
Theory "dfs8.DfsUndirNoWhiteToBlack": fully verified in 0.00 s
Obligations | Alt-Ergo (2.0.0) | CVC4 (1.5) |
1. VC for dfs | --- | --- |
split_goal_wp | | |
| 1. postcondition | 0.01 | --- |
2. postcondition | 0.01 | --- |
3. postcondition | 0.01 | --- |
4. postcondition | 0.01 | --- |
5. variant decrease | 0.01 | --- |
6. precondition | 0.01 | --- |
7. precondition | 0.01 | --- |
8. precondition | 0.01 | --- |
9. precondition | 0.01 | --- |
10. postcondition | 0.01 | --- |
11. postcondition | 0.01 | --- |
12. postcondition | 0.01 | --- |
13. postcondition | 0.01 | --- |
14. variant decrease | 0.01 | --- |
15. precondition | 0.01 | --- |
16. precondition | 0.01 | --- |
17. precondition | 0.01 | --- |
18. precondition | 0.03 | --- |
19. assertion | 0.30 | --- |
20. variant decrease | 0.02 | --- |
21. precondition | 0.01 | --- |
22. precondition | 0.01 | --- |
23. precondition | 0.01 | --- |
24. precondition | 0.18 | --- |
25. assertion | 2.10 | --- |
26. postcondition | 0.01 | --- |
27. postcondition | 0.01 | --- |
28. postcondition | 0.01 | --- |
29. postcondition | Timeout (15s) (obsolete) | --- |
split_goal_wp | | |
| 1. VC for dfs | 0.03 | --- |
2. VC for dfs | Timeout (15s) (obsolete) | 1.70 |
3. VC for dfs | 0.04 | --- |