Why3 Proof Results for Project "dfs5"
Theory "dfs5.DfsWhitePathSoundness": fully verified in 4.45 s
Obligations | Alt-Ergo (2.1.0) | CVC4 (1.5) |
whiteaccess_var | 0.01 | --- |
whiteaccess_covar1 | 0.01 | --- |
wpath_covar2 | --- | --- |
induction_pr | | |
| wpath_covar2.1 | 0.01 | --- |
wpath_covar2.2 | 0.01 | --- |
whiteaccess_covar2 | --- | 0.06 |
wpath_trans | --- | --- |
induction_pr | | |
| wpath_trans.1 | 0.01 | --- |
wpath_trans.2 | 0.01 | --- |
whiteaccess_trans | --- | 0.14 |
whiteaccess_cons | --- | 4.23 |
8. VC for dfs | --- | --- |
split_goal_wp | | |
| 1. postcondition | 0.01 | --- |
2. postcondition | 0.01 | --- |
3. postcondition | 0.01 | --- |
4. precondition | 0.01 | --- |
5. precondition | 0.01 | --- |
6. postcondition | 0.01 | --- |
7. postcondition | 0.01 | --- |
8. postcondition | 0.02 | --- |
9. precondition | 0.02 | --- |
10. precondition | 0.02 | --- |
11. assertion | 0.06 | --- |
12. assertion | 0.01 | --- |
13. assertion | --- | --- |
split_goal_wp | | |
| 1. VC for dfs | 0.10 | --- |
2. VC for dfs | 0.06 | --- |
14. precondition | 0.03 | --- |
15. precondition | 0.01 | --- |
16. assertion | 0.13 | --- |
17. assertion | 0.11 | --- |
18. postcondition | 0.09 | --- |
19. postcondition | 0.01 | --- |
20. postcondition | 0.33 | --- |
9. VC for dfs_main | --- | --- |
split_goal_wp | | |
| 1. precondition | 0.01 | --- |
2. precondition | 0.01 | --- |
3. postcondition | 0.02 | --- |