Why3 Proof Results for Project "dfs44"

Theory "dfs44.DfsWhitePathSoundness": fully verified in 7.12 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.18	---	---
whiteaccess_cons				---	6.76	---	---
whiteaccess_union				0.02	0.07	---	---
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. 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. type invariant			0.01	---	---	---
	11. index in array bounds			Timeout (15s) (obsolete)	14.65 (obsolete)	---	0.11
	12. precondition			0.01	---	---	---
	13. precondition			0.01	---	---	---
	14. precondition			0.01	---	---	---
	15. precondition			0.01	---	---	---
	16. loop invariant preservation			Timeout (15s) (obsolete)	0.61	---	---
	17. loop invariant preservation			0.03	---	---	---
	18. loop invariant preservation			0.02	---	---	---
	19. loop invariant preservation			---	---	0.73	---
	20. loop invariant preservation			0.02	---	---	---
	21. loop invariant preservation			Timeout (15s) (obsolete)	0.19	---	---
	22. loop invariant preservation			Timeout (15s) (obsolete)	0.33	---	---
	23. loop invariant preservation			0.01	---	---	---
	24. loop invariant preservation			0.01	---	---	---
	25. loop invariant preservation			0.05	---	---	---
	26. loop invariant preservation			0.01	---	---	---
	27. loop invariant preservation			Timeout (15s) (obsolete)	0.15	---	---
	28. assertion			0.15	---	---	---
	29. assertion			0.01	---	---	---
	30. assertion			---	---	---	---
	split_goal_wp
		1. VC for dfs1		0.02	---	---	---
		2. VC for dfs1		0.13	---	---	---
		3. VC for dfs1		0.08	---	---	---
	31. type invariant			0.01	---	---	---
	32. index in array bounds			0.01	---	---	---
	33. postcondition			0.02	---	---	---
	34. postcondition			0.04	---	---	---
	35. 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			---	---	---	0.08
	9. precondition			0.01	---	---	---
	10. precondition			0.01	---	---	---
	11. precondition			0.01	---	---	---
	12. precondition			0.01	---	---	---
	13. loop invariant preservation			Timeout (15s) (obsolete)	---	---	0.50
	14. loop invariant preservation			0.02	---	---	---
	15. loop invariant preservation			0.01	---	---	---
	16. loop invariant preservation			---	---	---	---
	introduce_premises
		1. loop invariant preservation		---	---	---	---
		inline_goal
			1. loop invariant preservation	---	---	---	1.13
	17. loop invariant preservation			Timeout (15s) (obsolete)	---	---	0.09
	18. loop invariant preservation			Timeout (15s) (obsolete)	---	---	0.83
	19. loop invariant preservation			0.01	---	---	---
	20. loop invariant preservation			0.01	---	---	---
	21. loop invariant preservation			0.03	---	---	---
	22. loop invariant preservation			Timeout (15s) (obsolete)	---	---	0.08
	23. postcondition			0.02	---	---	---
	24. loop invariant init			0.01	---	---	---
	25. type invariant			0.01	---	---	---
	26. index in array bounds			Timeout (15s) (obsolete)	---	---	0.33
	27. loop invariant preservation			0.02	---	---	---
	28. loop invariant preservation			0.02	---	---	---
	29. postcondition			0.18	---	---	---