Why3 Proof Results for Project "dfs6"

Theory "dfs6.DfsWhitePathSoundness": fully verified in 4.09 s

Obligations			Alt-Ergo (2.0.0)	Alt-Ergo (2.1.0)	CVC4 (1.5)	Coq (8.7.1)	Eprover (1.9)	Z3 (4.4.0)
whiteaccess_var			0.01	---	---	---	---	---
whiteaccess_covar1			0.01	---	---	---	---	---
wpath_covar2			---	---	---	---	---	---
induction_pr
	wpath_covar2.1		---	---	0.04	---	---	---
	wpath_covar2.2		---	---	0.05	---	---	---
whiteaccess_covar2			---	---	0.05	---	---	---
wpath_trans			---	---	---	---	---	---
induction_pr
	wpath_trans.1		0.01	---	---	---	---	---
	wpath_trans.2		---	---	---	---	0.03	---
whiteaccess_trans			---	---	0.14	---	---	---
whiteaccess_cons			---	---	3.31	0.57	---	---
8. VC for dfs			---	---	---	---	---	---
split_goal_wp
	1. postcondition		---	---	---	---	---	0.02
	2. postcondition		---	---	---	---	---	0.02
	3. postcondition		---	---	---	---	---	0.02
	4. variant decrease		---	---	---	---	---	0.02
	5. precondition		---	---	---	---	---	0.02
	6. precondition		---	---	---	---	---	0.02
	7. postcondition		---	---	---	---	---	0.02
	8. postcondition		---	---	---	---	---	0.02
	9. postcondition		---	---	---	---	---	0.02
	10. variant decrease		---	---	---	---	---	0.02
	11. precondition		---	---	---	---	---	0.02
	12. precondition		---	---	---	---	---	0.02
	13. assertion		---	---	---	---	---	0.05
	14. assertion		---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	0.06	---	---	---	---
		2. VC for dfs	---	0.08	---	---	---	---
	15. variant decrease		---	---	---	---	---	0.02
	16. precondition		---	---	---	---	---	0.02
	17. precondition		---	---	---	---	---	0.02
	18. assertion		---	0.11	---	---	---	---
	19. assertion		---	---	---	---	---	0.03
	20. postcondition		---	---	---	---	---	0.03
	21. postcondition		---	---	---	---	---	0.02
	22. postcondition		---	---	0.67	---	---	---
9. VC for dfs_main			---	---	---	---	---	---
split_goal_wp
	1. precondition		0.01	---	---	---	---	---
	2. precondition		0.01	---	---	---	---	---
	3. postcondition		0.02	---	---	---	---	---