Why3 Proof Results for Project "bfs1"

Theory "bfs1.Dfs_stack": fully verified in 0.03 s

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
whitepath_id			0.01	---	---
whitepath_covar			0.01	---	---
whitepath_cons			0.01	---	---
4. VC for push_set			---	---	---
split_goal_wp
	1. variant decrease		0.01	---	---
	2. postcondition		0.10	---	---
	3. postcondition		0.01	---	---
5. VC for bfs			---	---	---
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.02	---	---
	12. variant decrease		0.01	---	---
	13. precondition		---	0.08	---
	14. precondition		0.02	---	---
	15. assertion		---	---	---
	split_goal_wp
		1. assertion	---	---	0.19
		2. VC for bfs	0.03	0.27	0.04
		3. VC for bfs	---	0.06	0.51
	16. postcondition		0.02	---	---
	17. postcondition		0.01	---	---
	18. postcondition		0.02	---	---
	19. postcondition		0.04	---	---
6. VC for bfs_main			---	---	---
split_goal_wp
	1. precondition		0.01	---	---
	2. precondition		0.01	---	---
	3. postcondition		---	---	0.04