Why3 Proof Results for Project "dfs1"

Theory "dfs1.DfsWhitePathSoundness": fully verified in 3.96 s

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)
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			Timeout (15s)	0.06
wpath_trans			Timeout (15s)	14.94
induction_pr
	wpath_trans.1		0.01	---
	wpath_trans.2		0.01	---
whiteaccess_trans			Timeout (15s)	0.14
whiteaccess_cons			Timeout (15s)	3.74
8. VC for dfs			---	---
split_goal_wp
	1. precondition		0.01	---
	2. precondition		0.01	---
	3. postcondition		0.01	---
	4. postcondition		0.01	---
	5. postcondition		0.01	---
	6. precondition		0.01	---
	7. precondition		0.01	---
	8. assertion		0.04	---
	9. assertion		0.01	---
	10. assertion		---	---
	split_goal_wp
		1. VC for dfs	0.09	---
		2. VC for dfs	0.05	---
	11. precondition		0.01	---
	12. precondition		0.01	---
	13. assertion		0.16	---
	14. assertion		0.04	---
	15. postcondition		0.04	---
	16. postcondition		0.01	---
	17. postcondition		0.21	---
	18. postcondition		0.01	---
	19. postcondition		0.01	---
	20. postcondition		0.01	---
9. VC for dfs_main			---	---
split_goal_wp
	1. precondition		0.01	---
	2. precondition		0.01	---
	3. postcondition		0.02	---