Why3 Proof Results for Project "dfs5"

Theory "dfs5.DfsWhitePathSoundness": fully verified in 4.45 s

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)
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.06
wpath_trans			---	---
induction_pr
	wpath_trans.1		0.01	---
	wpath_trans.2		0.01	---
whiteaccess_trans			---	0.14
whiteaccess_cons			---	4.23
8. VC for dfs			---	---
split_goal_wp
	1. postcondition		0.01	---
	2. postcondition		0.01	---
	3. postcondition		0.01	---
	4. precondition		0.01	---
	5. precondition		0.01	---
	6. postcondition		0.01	---
	7. postcondition		0.01	---
	8. postcondition		0.02	---
	9. precondition		0.02	---
	10. precondition		0.02	---
	11. assertion		0.06	---
	12. assertion		0.01	---
	13. assertion		---	---
	split_goal_wp
		1. VC for dfs	0.10	---
		2. VC for dfs	0.06	---
	14. precondition		0.03	---
	15. precondition		0.01	---
	16. assertion		0.13	---
	17. assertion		0.11	---
	18. postcondition		0.09	---
	19. postcondition		0.01	---
	20. postcondition		0.33	---
9. VC for dfs_main			---	---
split_goal_wp
	1. precondition		0.01	---
	2. precondition		0.01	---
	3. postcondition		0.02	---