Why3 Proof Results for Project "dfs_stack1"

Theory "dfs_stack1.Dfs_stack": fully verified in 0.25 s

Obligations			Alt-Ergo (2.0.0)	CVC4 (1.5)	Eprover (1.9)
whitepath_id			0.02	---	---
whitepath_covar			0.02	---	---
whitepath_cons			0.02	---	---
4. VC for push_set			0.19	---	---
5. VC for dfs			---	---	---
split_goal_wp
	1. postcondition		0.01	---	---
	2. postcondition		0.01	---	---
	3. postcondition		0.01	---	---
	4. postcondition		0.01	---	---
	5. variant decrease		0.01	---	---
	6. precondition		0.02	---	---
	7. precondition		0.01	---	---
	8. postcondition		0.01	---	---
	9. postcondition		0.01	---	---
	10. postcondition		0.01	---	---
	11. postcondition		0.12	---	---
	12. variant decrease		0.02	---	---
	13. precondition		Timeout (15s)	0.17	---
	14. precondition		0.02	---	---
	15. assertion		Timeout (15s)	---	---
	split_goal_wp
		1. assertion	Timeout (15s)	14.63	0.43
		2. VC for dfs	0.04	---	---
		3. VC for dfs	Timeout (15s)	0.14	---
	16. postcondition		0.02	---	---
	17. postcondition		0.01	---	---
	18. postcondition		0.02	---	---
	19. postcondition		0.48	---	---
6. VC for dfs_main			---	---	---
split_goal_wp
	1. precondition		0.01	---	---
	2. precondition		0.01	---	---
	3. postcondition		Timeout (15s)	---	0.05