Obligations | Alt-Ergo (2.1.0) | CVC4 (1.4) | CVC4 (1.5) | Eprover (1.9) | Z3 (4.6.3) |
whiteaccess_var | 0.01 (obsolete) | --- | --- | --- | --- |
whiteaccess_covar1 | 0.01 (obsolete) | --- | --- | --- | --- |
wpath_covar2 | Timeout (15s) (obsolete) | --- | --- | --- | --- |
whiteaccess_covar2 | Timeout (15s) (obsolete) | --- | --- | --- | --- |
wpath_trans | Timeout (15s) (obsolete) | --- | --- | --- | --- |
whiteaccess_trans | Timeout (15s) (obsolete) | --- | --- | --- | --- |
whiteaccess_cons | Timeout (15s) (obsolete) | --- | --- | --- | --- |
whiteaccess_union | 0.02 (obsolete) | --- | --- | --- | --- |
path_wpathempty | Timeout (15s) (obsolete) | --- | --- | --- | --- |
diff_inc | --- | --- | --- | --- | --- |
split_goal_wp | | | | | |
| diff_inc.1 | 0.02 (obsolete) | --- | --- | --- | --- |
diff_inc.2 | 0.01 (obsolete) | --- | --- | --- | --- |
11. VC for dfs1 | --- | --- | --- | --- | --- |
split_goal_wp | | | | | |
| 1. assertion | 0.01 | --- | --- | --- | --- |
2. index in array bounds | 0.01 | --- | 0.07 | --- | --- |
3. index in array bounds | 0.01 | --- | --- | --- | --- |
4. loop invariant init | 0.01 | --- | --- | --- | --- |
5. loop invariant init | 0.01 | --- | --- | --- | --- |
6. loop invariant init | 0.02 | --- | --- | --- | --- |
7. loop invariant init | 0.02 | --- | --- | --- | --- |
8. loop invariant init | 0.01 | --- | --- | --- | --- |
9. loop invariant init | 0.01 | --- | --- | --- | --- |
10. type invariant | 0.01 | --- | 0.04 | --- | --- |
11. index in array bounds | Timeout (15s) (obsolete) | --- | 14.20 (obsolete) | 0.11 | --- |
12. precondition | 0.01 | --- | --- | --- | --- |
13. precondition | 0.01 | --- | --- | --- | --- |
14. precondition | 0.01 | --- | --- | --- | --- |
15. precondition | 0.02 | --- | --- | --- | --- |
16. loop invariant preservation | Timeout (15s) (obsolete) | --- | 0.55 | 0.40 | --- |
17. loop invariant preservation | 0.03 | --- | --- | --- | --- |
18. loop invariant preservation | 0.02 | --- | --- | --- | --- |
19. loop invariant preservation | Not yet run | --- | 29.89 (obsolete) | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) |
20. loop invariant preservation | 0.01 | --- | --- | --- | --- |
21. loop invariant preservation | Timeout (15s) (obsolete) | --- | 0.20 | 0.09 | --- |
22. loop invariant preservation | Timeout (15s) (obsolete) | --- | 0.33 | 0.39 | --- |
23. loop invariant preservation | 0.01 | --- | --- | --- | --- |
24. loop invariant preservation | 0.02 | --- | --- | --- | --- |
25. loop invariant preservation | 0.06 | --- | --- | --- | --- |
26. loop invariant preservation | 0.02 | --- | --- | --- | --- |
27. loop invariant preservation | Timeout (15s) (obsolete) | --- | 0.16 | 0.09 | --- |
28. assertion | Timeout (15s) (obsolete) | --- | 14.06 (obsolete) | Timeout (15s) (obsolete) | --- |
split_goal_wp | | | | | |
| 1. VC for dfs1 | 0.03 | --- | --- | --- | --- |
2. VC for dfs1 | 0.09 | --- | --- | --- | --- |
29. assertion | 0.01 | --- | 0.09 | --- | --- |
30. assertion | --- | --- | --- | --- | --- |
split_goal_wp | | | | | |
| 1. VC for dfs1 | 0.03 | --- | --- | --- | --- |
2. VC for dfs1 | 0.12 | --- | --- | --- | --- |
3. VC for dfs1 | 0.09 | --- | --- | --- | --- |
31. type invariant | 0.01 | --- | --- | --- | --- |
32. index in array bounds | 0.01 | --- | --- | --- | --- |
33. postcondition | 0.06 | --- | 0.13 | --- | --- |
34. postcondition | Not yet run | 14.86 | --- | Timeout (15s) | --- |
35. postcondition | 0.04 | --- | 0.13 | --- | --- |
36. postcondition | 0.01 | --- | 0.04 | 0.02 | --- |
12. VC for dfs_main | Timeout (15s) (obsolete) | --- | --- | --- | --- |
split_goal_wp | | | | | |
| 1. array creation size | 0.01 | --- | --- | --- | --- |
2. assertion | 0.01 | --- | --- | --- | --- |
3. assertion | Timeout (15s) | --- | 15.41 (obsolete) | --- | --- |
4. postcondition | Timeout (15s) (obsolete) | --- | 28.94 (obsolete) | Timeout (15s) (obsolete) | --- |
split_goal_wp | | | | | |
| 1. VC for dfs_main | 0.01 | --- | 15.46 (obsolete) | Timeout (15s) (obsolete) | --- |
2. VC for dfs_main | 0.01 | --- | 0.10 | --- | --- |
5. loop invariant init | 0.01 | --- | --- | --- | --- |
6. loop invariant init | 0.01 | --- | --- | --- | --- |
7. loop invariant init | 0.01 | --- | --- | --- | --- |
8. loop invariant init | 0.01 | --- | --- | --- | --- |
9. loop invariant init | 0.01 | --- | --- | --- | --- |
10. type invariant | 0.01 | --- | --- | --- | --- |
11. index in array bounds | 0.01 | --- | --- | --- | --- |
12. precondition | 0.01 | --- | --- | --- | --- |
13. precondition | 0.01 | --- | 13.82 (obsolete) | Timeout (15s) (obsolete) | --- |
14. precondition | 0.01 | --- | --- | --- | --- |
15. precondition | 0.01 | --- | --- | --- | --- |
16. loop invariant preservation | 0.02 | --- | --- | --- | --- |
17. loop invariant preservation | 0.02 | --- | --- | --- | --- |
18. loop invariant preservation | 0.01 | --- | --- | --- | --- |
19. loop invariant preservation | --- | --- | --- | --- | --- |
introduce_premises | | | | | |
| 1. loop invariant preservation | --- | --- | --- | --- | --- |
inline_goal | | | | | |
| 1. loop invariant preservation | --- | --- | --- | 0.90 | --- |
20. loop invariant preservation | 0.07 | --- | --- | --- | --- |
21. loop invariant preservation | 0.01 | --- | --- | --- | --- |
22. loop invariant preservation | 0.01 | --- | --- | --- | --- |
23. loop invariant preservation | 0.01 | --- | --- | --- | --- |
24. loop invariant preservation | 0.03 | --- | --- | --- | --- |
25. loop invariant preservation | 0.05 | --- | --- | --- | --- |
26. assertion | 0.01 | --- | --- | --- | --- |
27. assertion | Timeout (15s) | --- | 29.87 | Timeout (15s) | --- |
28. type invariant | 0.01 | --- | --- | --- | --- |
29. postcondition | Timeout (15s) (obsolete) | --- | 26.71 (obsolete) | Timeout (15s) (obsolete) | --- |
split_goal_wp | | | | | |
| 1. VC for dfs_main | 0.01 | 14.55 (obsolete) | 29.46 (obsolete) | Timeout (15s) (obsolete) | --- |
2. VC for dfs_main | 0.02 | --- | --- | --- | --- |
13. VC for test | --- | --- | --- | --- | --- |
split_goal_wp | | | | | |
| 1. array creation size | 0.01 | --- | --- | --- | --- |
2. assertion | 0.01 | --- | --- | --- | --- |
3. assertion | Timeout (15s) (obsolete) | --- | --- | --- | --- |
introduce_premises | | | | | |
| 1. assertion | --- | --- | --- | --- | --- |
inline_goal | | | | | |
| 1. assertion | --- | --- | --- | --- | --- |
split_goal_wp | | | | | |
| 1. assertion | Timeout (15s) | --- | Timeout (15s) | Timeout (15s) | Timeout (15s) (obsolete) |
2. assertion | 0.01 | --- | --- | --- | --- |