Why3 Proof Results for Project "dfs34"

Theory "dfs34.DfsWhitePathCompleteness": 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.01	---	---
	7. loop invariant init	0.02	---	---
	8. loop invariant init	0.01	---	---
	9. loop invariant init	0.01	14.97 (obsolete)	---
	10. loop invariant init	0.01	---	---
	11. loop invariant init	0.01	---	---
	12. type invariant	0.01	---	---
	13. index in array bounds	Timeout (15s) (obsolete)	14.90 (obsolete)	0.13
	14. precondition	0.01	---	---
	15. precondition	0.01	---	---
	16. precondition	0.01	---	---
	17. precondition	0.01	---	---
	18. loop invariant preservation	Timeout (15s) (obsolete)	0.53	---
	19. loop invariant preservation	0.03	---	---
	20. loop invariant preservation	0.02	---	---
	21. loop invariant preservation	0.02	---	---
	22. loop invariant preservation	0.05	---	---
	23. loop invariant preservation	0.01	---	---
	24. loop invariant preservation	0.09	---	---
	25. loop invariant preservation	Timeout (15s) (obsolete)	0.19	---
	26. loop invariant preservation	Timeout (15s) (obsolete)	0.33	---
	27. loop invariant preservation	0.01	---	---
	28. loop invariant preservation	0.01	---	---
	29. loop invariant preservation	0.01	---	---
	30. loop invariant preservation	0.02	---	---
	31. loop invariant preservation	0.01	---	---
	32. loop invariant preservation	0.01	---	---
	33. loop invariant preservation	Timeout (15s) (obsolete)	0.15	---
	34. assertion	0.11	---	---
	35. type invariant	0.01	---	---
	36. index in array bounds	0.01	---	---
	37. postcondition	0.02	---	---
	38. postcondition	0.01	---	---
	39. postcondition	0.02	---	---
	40. postcondition	0.47	---	---
	41. postcondition	0.03	---	---
5. VC for dfs_main		---	---	---
split_goal_wp
	1. array creation size	0.01	---	---
	2. postcondition	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.01	---	---
	10. precondition	0.01	---	---
	11. precondition	0.01	---	---
	12. precondition	0.01	---	---
	13. precondition	0.01	---	---
	14. loop invariant preservation	0.02	---	---
	15. loop invariant preservation	0.01	---	---
	16. loop invariant preservation	0.03	---	---
	17. loop invariant preservation	0.03	---	---
	18. loop invariant preservation	0.05	---	---
	19. loop invariant preservation	0.01	---	---
	20. loop invariant preservation	0.01	---	---
	21. loop invariant preservation	0.01	---	---
	22. loop invariant preservation	0.01	---	---
	23. loop invariant preservation	0.04	---	---
	24. type invariant	0.01	---	---
	25. postcondition	0.02	---	---