Why3 Proof Results for Project "dfs66"
Theory "dfs66.DfsWhitePathGraySoundness": fully verified in 3.56 s
Obligations | Alt-Ergo (2.0.0) | CVC4 (1.5) | Eprover (1.9) | Z3 (4.4.0) |
whiteaccess_var | 0.01 | --- | --- | --- |
whiteaccess_covar1 | 0.01 | --- | --- | --- |
wpath_covar2 | Timeout (15s) | 14.80 | Timeout (15s) | --- |
induction_pr | | | | |
| wpath_covar2.1 | 0.01 | --- | --- | --- |
wpath_covar2.2 | Timeout (15s) | 0.06 | 0.03 | --- |
whiteaccess_covar2 | Timeout (15s) | 0.06 | --- | --- |
wpath_trans | Timeout (15s) | 14.83 | Timeout (15s) | --- |
induction_pr | | | | |
| wpath_trans.1 | 0.01 | --- | --- | --- |
wpath_trans.2 | Timeout (15s) | 0.04 | 0.03 | --- |
whiteaccess_trans | Timeout (15s) | 0.13 | --- | --- |
whiteaccess_cons | Timeout (15s) | 3.35 | Timeout (15s) | --- |
8. VC for dfs | --- | --- | --- | --- |
split_goal_wp | | | | |
| 1. postcondition | 0.01 | --- | --- | --- |
2. postcondition | 0.01 | --- | --- | --- |
3. postcondition | 0.00 | --- | --- | --- |
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 | --- | --- | --- | --- |
split_goal_wp | | | | |
| 1. VC for dfs | 0.01 | --- | --- | --- |
2. VC for dfs | 0.01 | --- | --- | --- |
3. VC for dfs | 0.01 | --- | --- | --- |
20. assertion | 0.01 | --- | --- | --- |
21. assertion | Timeout (15s) (obsolete) | 29.66 (obsolete) | Timeout (15s) (obsolete) | --- |
split_goal_wp | | | | |
| 1. VC for dfs | 0.33 | --- | --- | --- |
2. VC for dfs | 7.69 | 15.31 (obsolete) | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) |
22. variant decrease | 0.02 | --- | --- | --- |
23. precondition | 0.02 | --- | --- | --- |
24. precondition | 0.01 | --- | --- | --- |
25. precondition | 0.01 | --- | --- | --- |
26. precondition | 0.28 | --- | --- | --- |
27. assertion | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) | Timeout (15s) (obsolete) | --- |
split_goal_wp | | | | |
| 1. VC for dfs | 0.02 | --- | --- | --- |
2. VC for dfs | 0.01 | --- | --- | --- |
3. VC for dfs | 0.24 | 29.41 (obsolete) | Timeout (15s) (obsolete) | --- |
28. assertion | 1.76 | 29.73 (obsolete) | Timeout (15s) (obsolete) | --- |
29. postcondition | 0.01 | --- | --- | --- |
30. postcondition | 0.01 | --- | --- | --- |
31. postcondition | 0.01 | --- | --- | --- |
32. postcondition | 0.84 | 29.44 (obsolete) | Timeout (15s) (obsolete) | --- |