Why3 Proof Results for Project "dfs22"

Theory "dfs22.DfsWhitePathSoundness": fully verified in 5.52 s

Obligations				Alt-Ergo (2.1.0)	CVC4 (1.5)	Coq (8.7.2)	Eprover (1.9)
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.07	---	---
wpath_trans				---	---	---	---
induction_pr
	wpath_trans.1			0.01	---	---	---
	wpath_trans.2			0.01	---	---	---
whiteaccess_trans				---	0.16	---	---
whiteaccess_cons				---	5.25	---	---
whiteaccess_union				0.02	---	---	---
path_wpathempty				---	---	---	---
induction_pr
	path_wpathempty.1			0.01	---	---	---
	path_wpathempty.2			0.01	---	---	---
diff_inc				---	---	---	---
split_goal_wp
	diff_inc.1			0.02	---	---	---
	diff_inc.2			0.01	---	---	---
11. VC for dfs1				---	---	---	---
split_goal_wp
	1. assertion			0.01	---	---	---
	2. index in array bounds			0.01	---	---	---
	3. loop invariant init			0.01	---	---	---
	4. loop invariant init			0.01	---	---	---
	5. loop invariant init			0.02	---	---	---
	6. loop invariant init			0.01	---	---	---
	7. loop invariant init			0.01	---	---	---
	8. loop invariant init			0.01	---	---	---
	9. type invariant			0.01	---	---	---
	10. index in array bounds			---	---	---	---
	split_goal_wp
		1. VC for dfs1		---	---	---	0.12
		2. VC for dfs1		---	---	---	0.12
	11. precondition			0.01	---	---	---
	12. precondition			0.01	---	---	---
	13. precondition			0.01	---	---	---
	14. loop invariant preservation			---	0.48	---	---
	15. loop invariant preservation			0.01	---	---	---
	16. loop invariant preservation			0.02	---	---	---
	17. loop invariant preservation			---	---	0.69	---
	18. loop invariant preservation			0.01	---	---	---
	19. loop invariant preservation			---	0.17	---	---
	20. loop invariant preservation			---	0.27	---	---
	21. loop invariant preservation			0.01	---	---	---
	22. loop invariant preservation			0.01	---	---	---
	23. loop invariant preservation			0.05	---	---	---
	24. loop invariant preservation			0.01	---	---	---
	25. loop invariant preservation			---	0.14	---	---
	26. assertion			---	---	---	---
	split_goal_wp
		1. VC for dfs1		0.03	---	---	---
		2. VC for dfs1		0.09	---	---	---
	27. assertion			0.01	---	---	---
	28. assertion			---	---	---	---
	split_goal_wp
		1. VC for dfs1		0.03	---	---	---
		2. VC for dfs1		0.11	---	---	---
		3. VC for dfs1		0.08	---	---	---
	29. type invariant			0.01	---	---	---
	30. index in array bounds			0.01	---	---	---
	31. postcondition			0.05	---	---	---
	32. postcondition			0.04	---	---	---
	33. postcondition			0.01	---	---	---
12. 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. type invariant			0.01	---	---	---
	8. index in array bounds			---	14.67	---	0.09
	9. precondition			0.01	---	---	---
	10. precondition			0.01	---	---	---
	11. precondition			0.01	---	---	---
	12. loop invariant preservation			---	0.33	---	---
	13. loop invariant preservation			0.02	---	---	---
	14. loop invariant preservation			0.01	---	---	---
	15. loop invariant preservation			---	---	---	---
	introduce_premises
		1. loop invariant preservation		---	---	---	---
		inline_goal
			1. loop invariant preservation	---	---	---	0.87
	16. loop invariant preservation			---	0.14	---	---
	17. loop invariant preservation			---	0.17	---	---
	18. loop invariant preservation			0.01	---	---	---
	19. loop invariant preservation			0.01	---	---	---
	20. loop invariant preservation			0.03	---	---	---
	21. loop invariant preservation			---	0.11	---	---
	22. postcondition			0.01	---	---	---
	23. loop invariant init			0.01	---	---	---
	24. type invariant			0.01	---	---	---
	25. index in array bounds			0.01	---	---	---
	26. loop invariant preservation			0.02	---	---	---
	27. loop invariant preservation			0.02	---	---	---
	28. postcondition			0.16	---	---	---