Why3 Proof Results for Project "dfs44"

Theory "dfs44.DfsWhitePathThm": fully verified in 3.77 s

Obligations			Alt-Ergo (2.0.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		Timeout (15s)	0.06	---
whiteaccess_covar2			Timeout (15s)	0.06	---
wpath_trans			Timeout (15s)	---	---
induction_pr
	wpath_trans.1		0.01	---	---
	wpath_trans.2		Timeout (15s)	0.04	---
whiteaccess_trans			Timeout (15s)	0.13	---
whiteaccess_cons			Timeout (15s)	3.26	---
whiteaccess_minus			0.01	---	---
nbtw_path			Timeout (15s)	---	---
induction_pr
	nbtw_path.1		0.01	---	---
	nbtw_path.2		Timeout (15s)	0.05	---
nbtw_whiteaccess			0.02	---	---
diff_empty			Timeout (15s)	0.06	---
whiteaccess_roots_result			0.21	---	---
13. VC for dfs			---	---	---
split_goal_wp
	1. postcondition		0.01	---	---
	2. postcondition		0.01	---	---
	3. postcondition		0.01	---	---
	4. postcondition		0.08	---	---
	5. variant decrease		0.01	---	---
	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		1.10	---	---
	14. variant decrease		0.01	---	---
	15. precondition		0.01	---	---
	16. precondition		0.01	---	---
	17. precondition		0.01	---	---
	18. precondition		0.03	---	---
	19. assertion		Timeout (15s)	---	---
	split_goal_wp
		1. VC for dfs	0.01	---	---
		2. VC for dfs	0.02	---	---
		3. VC for dfs	0.15	---	---
	20. assertion		0.01	---	---
	21. assertion		---	---	---
	split_goal_wp
		1. VC for dfs	0.71	---	---
		2. VC for dfs	0.17	---	---
	22. variant decrease		0.02	---	---
	23. precondition		0.02	---	---
	24. precondition		0.02	---	---
	25. precondition		0.01	---	---
	26. precondition		0.43	---	---
	27. assertion		Timeout (15s)	---	---
	split_goal_wp
		1. VC for dfs	0.02	---	---
		2. VC for dfs	0.01	---	---
		3. VC for dfs	0.31	---	---
	28. assertion		3.12	---	---
	29. postcondition		0.01	---	---
	30. postcondition		0.02	---	---
	31. postcondition		0.01	---	---
	32. postcondition		Timeout (15s)	---	---
	split_goal_wp
		1. VC for dfs	0.04	---	---
		2. VC for dfs	Timeout (15s)	15.61	Timeout (15s)
		3. VC for dfs	Timeout (15s)	0.14	Timeout (15s)
		4. VC for dfs	Timeout (15s)	2.91	Timeout (15s)