Obligations | Alt-Ergo (2.1.0) | CVC4 (1.5) | Eprover (1.9) |
paths_in | --- | --- | --- |
induction_pr | | | |
| paths_in.1 | 0.00 | --- | --- |
paths_in.2 | 0.01 | --- | --- |
2. VC for add_grays | 0.01 | --- | --- |
3. VC for add_blacks | 0.00 | --- | --- |
4. VC for dfs | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.01 | --- | --- |
2. postcondition | 0.01 | --- | --- |
3. postcondition | 0.01 | --- | --- |
4. exceptional postcondition | --- | 0.46 | --- |
5. assertion | 0.11 | --- | --- |
6. precondition | 0.01 | --- | --- |
7. precondition | 0.05 | --- | --- |
8. precondition | 0.06 | --- | --- |
9. precondition | --- | 0.14 | --- |
10. postcondition | 0.19 | --- | --- |
11. postcondition | 0.03 | --- | --- |
12. postcondition | 0.02 | --- | --- |
13. exceptional postcondition | 0.01 | --- | --- |
14. precondition | 0.01 | --- | --- |
15. precondition | --- | --- | --- |
introduce_premises | | | |
| 1. precondition | --- | --- | --- |
inline_goal | | | |
| 1. precondition | --- | --- | --- |
introduce_premises | | | |
| 1. precondition | --- | --- | --- |
inline_goal | | | |
| 1. precondition | --- | --- | 0.15 |
16. precondition | 0.05 | --- | --- |
17. precondition | 0.01 | --- | --- |
18. assertion | 0.03 | --- | --- |
19. precondition | 0.01 | --- | --- |
20. precondition | 0.03 | --- | --- |
21. precondition | --- | --- | --- |
introduce_premises | | | |
| 1. precondition | --- | --- | --- |
inline_goal | | | |
| 1. precondition | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 0.04 | --- | --- |
2. precondition | 0.08 | --- | --- |
3. precondition | 0.08 | --- | --- |
4. precondition | --- | 0.08 | --- |
22. precondition | --- | 0.72 | --- |
23. postcondition | 0.37 | --- | --- |
24. postcondition | 0.06 | --- | --- |
25. postcondition | 0.01 | --- | --- |
26. exceptional postcondition | 0.01 | --- | --- |
27. exceptional postcondition | 0.01 | --- | --- |
5. VC for is_acyclic | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 0.01 | --- | --- |
2. precondition | 0.01 | --- | --- |
3. precondition | 0.01 | --- | --- |
4. precondition | 3.22 | --- | --- |
5. assertion | 0.26 | --- | --- |
6. postcondition | 0.01 | --- | --- |
7. postcondition | 0.01 | --- | --- |