Why3 Proof Results for Project "dfs4"

Theory "dfs4.DfsWhitePathThm": fully verified in 4.56 s

Obligations			Alt-Ergo (2.0.0)	Alt-Ergo (2.2.0)	CVC4 (1.5)	Coq (8.7.1)	Eprover (1.9)
whiteaccess_var			0.01	---	---	---	---
whiteaccess_covar1			0.01	---	---	---	---
wpath_covar2			---	---	---	---	---
induction_pr
	wpath_covar2.1		0.01	---	---	---	---
	wpath_covar2.2		---	---	0.06	---	---
whiteaccess_covar2			---	---	0.06	---	---
wpath_trans			---	---	---	---	---
induction_pr
	wpath_trans.1		0.01	---	---	---	---
	wpath_trans.2		---	---	0.05	---	---
whiteaccess_trans			---	---	0.14	---	---
whiteaccess_cons			---	---	3.79	0.55	---
nbtw_path			---	---	---	---	---
induction_pr
	nbtw_path.1		0.01	---	0.03	---	---
	nbtw_path.2		---	---	0.05	---	0.12
9. VC for dfs			---	---	---	---	---
split_goal_wp
	1. postcondition		0.01	---	---	---	---
	2. postcondition		0.01	---	---	---	---
	3. postcondition		0.01	---	---	---	---
	4. postcondition		---	0.02	---	---	---
	5. variant decrease		0.01	---	---	---	---
	6. precondition		0.01	---	---	---	---
	7. precondition		0.01	---	---	---	---
	8. postcondition		---	0.01	---	---	---
	9. postcondition		---	0.01	---	---	---
	10. postcondition		---	0.01	---	---	---
	11. postcondition		---	0.18	---	---	---
	12. variant decrease		0.01	---	---	---	---
	13. precondition		0.01	---	---	---	---
	14. precondition		0.01	---	---	---	---
	15. assertion		---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	0.01	---	---	---
		2. VC for dfs	0.02 (obsolete)	0.02	---	---	---
		3. VC for dfs	---	---	---	---	0.10
		4. VC for dfs	---	0.01	---	---	---
	16. assertion		---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	---	0.11	---	---
		2. VC for dfs	---	---	0.17	---	---
	17. variant decrease		---	0.03	---	---	---
	18. precondition		---	0.01	---	---	---
	19. precondition		---	0.01	---	---	---
	20. assertion		---	0.12	---	---	---
	21. assertion		---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	---	0.10	---	---
		2. VC for dfs	---	---	---	---	0.09
	22. postcondition		---	0.01	---	---	---
	23. postcondition		---	0.01	---	---	---
	24. postcondition		---	0.01	---	---	---
	25. postcondition		---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	0.11	---	---	---
		2. VC for dfs	---	---	0.64	---	---
		3. VC for dfs	---	0.27	---	---	---