Why3 Proof Results for Project "dfs45"

Theory "dfs45.DfsWhitePathSoundness": fully verified in 0.00 s

Obligations		Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
nbtw_wpath		---	---	---
induction_pr
	nbtw_wpath.1	0.01	---	---
	nbtw_wpath.2	0.02	---	---
path_wpathempty		---	---	---
induction_pr
	path_wpathempty.1	0.01	---	---
	path_wpathempty.2	0.01	---	---
nbtw_path		---	---	---
induction_pr
	nbtw_path.1	0.01	---	---
	nbtw_path.2	0.01	---	---
4. VC for dfs1		---	---	---
split_goal_wp
	1. assertion	0.01	---	---
	2. index in array bounds	0.01	---	---
	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.01	---	---
	8. loop invariant init	0.01	---	---
	9. loop invariant init	0.01	---	---
	10. loop invariant init	0.01	---	---
	11. type invariant	0.01	---	---
	12. index in array bounds	---	---	0.13
	13. precondition	0.01	---	---
	14. precondition	0.01	---	---
	15. precondition	0.01	---	---
	16. precondition	0.01	---	---
	17. loop invariant preservation	---	0.56	0.38
	18. loop invariant preservation	0.03	---	---
	19. loop invariant preservation	0.02	---	---
	20. loop invariant preservation	0.02	---	---
	21. loop invariant preservation	0.05	---	---
	22. loop invariant preservation	0.10	---	---
	23. loop invariant preservation	---	0.21	---
	24. loop invariant preservation	---	0.34	0.45
	25. loop invariant preservation	0.01	---	---
	26. loop invariant preservation	0.01	---	---
	27. loop invariant preservation	0.01	---	---
	28. loop invariant preservation	0.02	---	---
	29. loop invariant preservation	0.01	---	---
	30. loop invariant preservation	---	0.14	---
	31. assertion	0.12	---	---
	32. type invariant	0.01	---	---
	33. index in array bounds	0.01	---	---
	34. postcondition	0.05	---	---
	35. postcondition	0.04	---	---
	36. postcondition	0.03	---	---
	37. postcondition	0.36	---	---
5. VC for dfs_main		---	---	---
split_goal_wp
	1. array creation size	0.01	---	---
	2. loop invariant init	0.01	---	---
	3. loop invariant init	0.01	---	---
	4. loop invariant init	0.01	---	---
	5. loop invariant init	0.01	---	---
	6. loop invariant init	0.01	---	---
	7. loop invariant init	0.01	---	---
	8. type invariant	0.01	---	---
	9. index in array bounds	---	---	0.10
	10. precondition	0.01	---	---
	11. precondition	0.01	---	---
	12. precondition	0.01	---	---
	13. precondition	0.01	---	---
	14. loop invariant preservation	---	0.28	---
	15. loop invariant preservation	0.02	---	---
	16. loop invariant preservation	0.01	---	---
	17. loop invariant preservation	0.04	---	---
	18. loop invariant preservation	---	0.14	---
	19. loop invariant preservation	---	0.15	0.09
	20. loop invariant preservation	---	0.19	---
	21. loop invariant preservation	0.01	---	---
	22. loop invariant preservation	0.01	---	---
	23. loop invariant preservation	0.01	---	---
	24. loop invariant preservation	---	0.19	---
	25. loop invariant preservation	---	0.12	0.07
	26. assertion	0.02	---	---
	27. assertion	0.02	---	---
	28. postcondition	0.01	---	---
	29. postcondition	0.01	---	---
	30. loop invariant init	0.01	---	---
	31. type invariant	0.01	---	---
	32. index in array bounds	0.01	---	---
	33. loop invariant preservation	0.02	---	---
	34. loop invariant preservation	0.03	---	---
	35. assertion	0.04	---	---
	36. postcondition	0.01	---	---
	37. postcondition	0.01	---	---