Why3 Proof Results for Project "dfs8"

Theory "dfs8.DfsWhitePathSoundness": fully verified in 4.67 s

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
whiteaccess_var			0.01	---	---
whiteaccess_covar1			0.01	---	---
wpath_covar2			Timeout (15s)	---	---
induction_pr
	wpath_covar2.1		0.01	---	---
	wpath_covar2.2		0.01	---	---
whiteaccess_covar2			---	0.07	---
wpath_trans			Timeout (15s)	---	---
induction_pr
	wpath_trans.1		0.01	---	---
	wpath_trans.2		0.01	---	---
whiteaccess_trans			---	0.15	---
whiteaccess_cons			---	4.43	---
path_wpathempty			---	---	---
split_goal_wp
	path_wpathempty.1		Timeout (15s)	---	---
	induction_pr
		path_wpathempty.1.1	0.01	---	---
		path_wpathempty.1.2	0.01	---	---
9. VC for dfs			---	---	---
split_goal_wp
	1. postcondition		0.01	---	---
	2. postcondition		0.01	---	---
	3. postcondition		---	---	---
	split_goal_wp
		1. postcondition	0.01	---	---
		2. postcondition	0.01	---	---
		3. postcondition	0.01	---	---
	4. postcondition		0.01	---	---
	5. index in array bounds		---	---	---
	split_goal_wp
		1. VC for dfs	---	---	0.03
		2. VC for dfs	Timeout (35s) (obsolete)	---	0.04
	6. precondition		0.01	---	---
	7. precondition		0.01	---	---
	8. precondition		0.01	---	---
	9. precondition		0.01	---	---
	10. postcondition		0.01	---	---
	11. postcondition		0.01	---	---
	12. postcondition		0.01	---	---
	13. postcondition		0.02	---	---
	14. index in array bounds		0.01	---	---
	15. precondition		0.02	---	---
	16. precondition		0.02	---	---
	17. precondition		0.01	---	---
	18. precondition		0.01	---	---
	19. assertion		0.06	---	---
	20. assertion		0.02	---	---
	21. assertion		Timeout (35s) (obsolete)	---	---
	split_goal_wp
		1. VC for dfs	0.09	---	---
		2. VC for dfs	0.06	---	---
	22. precondition		0.03	---	---
	23. precondition		0.01	---	---
	24. precondition		0.01	---	---
	25. precondition		0.01	---	---
	26. assertion		0.10	---	---
	27. assertion		0.10	---	---
	28. postcondition		0.07	---	---
	29. postcondition		0.01	---	---
	30. postcondition		0.01	---	---
	31. postcondition		0.33	---	---
10. VC for dfs_main			---	---	---
split_goal_wp
	1. array creation size		0.01	---	---
	2. precondition		0.01	---	---
	3. precondition		0.01	---	---
	4. precondition		0.01	---	---
	5. precondition		---	---	---
	split_goal_wp
		1. precondition	0.01	---	---
		2. precondition	0.01	---	---
		3. precondition	0.01	---	---
	6. postcondition		---	---	---
	split_goal_wp
		1. VC for dfs_main	0.02	0.47	1.24
		2. VC for dfs_main	0.03	---	---