Why3 Proof Results for Project "dag1"

Theory "dag1.DfsWhitePathGraySoundness": fully verified in 0.01 s

Obligations						Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
paths_in						---	---	---
induction_pr
	paths_in.1					0.00	---	---
	paths_in.2					0.01	---	---
2. VC for add_grays						0.01	---	---
3. VC for add_blacks						0.00	---	---
4. VC for dfs						---	---	---
split_goal_wp
	1. postcondition					0.01	---	---
	2. postcondition					0.01	---	---
	3. postcondition					0.01	---	---
	4. exceptional postcondition					---	0.46	---
	5. assertion					0.11	---	---
	6. precondition					0.01	---	---
	7. precondition					0.05	---	---
	8. precondition					0.06	---	---
	9. precondition					---	0.14	---
	10. postcondition					0.19	---	---
	11. postcondition					0.03	---	---
	12. postcondition					0.02	---	---
	13. exceptional postcondition					0.01	---	---
	14. precondition					0.01	---	---
	15. precondition					---	---	---
	introduce_premises
		1. precondition				---	---	---
		inline_goal
			1. precondition			---	---	---
			introduce_premises
				1. precondition		---	---	---
				inline_goal
					1. precondition	---	---	0.15
	16. precondition					0.05	---	---
	17. precondition					0.01	---	---
	18. assertion					0.03	---	---
	19. precondition					0.01	---	---
	20. precondition					0.03	---	---
	21. precondition					---	---	---
	introduce_premises
		1. precondition				---	---	---
		inline_goal
			1. precondition			---	---	---
			split_goal_wp
				1. precondition		0.04	---	---
				2. precondition		0.08	---	---
				3. precondition		0.08	---	---
				4. precondition		---	0.08	---
	22. precondition					---	0.72	---
	23. postcondition					0.37	---	---
	24. postcondition					0.06	---	---
	25. postcondition					0.01	---	---
	26. exceptional postcondition					0.01	---	---
	27. exceptional postcondition					0.01	---	---
5. VC for is_acyclic						---	---	---
split_goal_wp
	1. precondition					0.01	---	---
	2. precondition					0.01	---	---
	3. precondition					0.01	---	---
	4. precondition					3.22	---	---
	5. assertion					0.26	---	---
	6. postcondition					0.01	---	---
	7. postcondition					0.01	---	---