Why3 Proof Results for Project "dfs1"

Theory "dfs1.DfsWhitePathSoundness": fully verified in 0.32 s

Obligations					Alt-Ergo (2.0.0)	CVC4 (1.5)	Eprover (1.9)
whitepath_id					0.01	---	---
whitepath_sub					0.01	---	---
whitepath_cons					0.01	---	---
4. VC for dfs					---	---	---
split_goal_wp
	1. postcondition				0.01	---	---
	2. postcondition				0.01	---	---
	3. postcondition				0.01	---	---
	4. variant decrease				0.01	---	---
	5. precondition				0.01	---	---
	6. precondition				0.00	---	---
	7. postcondition				0.00	---	---
	8. postcondition				0.01	---	---
	9. postcondition				0.02	---	---
	10. variant decrease				0.01	---	---
	11. precondition				0.01	---	---
	12. precondition				0.01	---	---
	13. variant decrease				0.02	---	---
	14. precondition				0.01	---	---
	15. precondition				0.01	---	---
	16. assertion				---	---	---
	split_goal_wp
		1. assertion			---	---	0.12
		2. VC for dfs			---	---	---
		introduce_premises
			1. VC for dfs		---	---	---
			inline_goal
				1. VC for dfs	---	0.72	---
	17. postcondition				0.01	---	---
	18. postcondition				0.01	---	---
	19. postcondition				---	2.46	---
5. VC for dfs_main					---	---	0.29