Why3 Proof Results for Project "dag2"

Theory "dag2.TestAcyclicGraph": fully verified in 0.14 s

Obligations						Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)	Spass (3.5)	Z3 (4.6.2)
paths_in						---	---	---	---	---
induction_pr
	paths_in.1					0.01	0.03	0.01	0.03	0.03
	paths_in.2					0.01	0.04	0.03	0.04	Timeout (15s)
2. VC for add_grays						0.00	0.02	0.01	0.03	0.01
3. VC for add_blacks						0.00	0.02	0.01	0.03	0.01
4. VC for dfs						---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	0.05	0.02	0.04	0.12
	2. postcondition					0.01	0.05	0.03	0.04	0.02
	3. postcondition					0.01	0.04	0.01	0.03	0.02
	4. exceptional postcondition					0.09	1.42	Timeout (15s)	Timeout (15s)	0.20
	5. assertion					0.04	0.07	0.06	Timeout (15s)	0.04
	6. precondition					0.01	0.05	0.03	0.04	0.03
	7. precondition					0.03	0.09	1.37	Timeout (15s)	0.03
	8. precondition					0.11	0.08	0.66	Timeout (15s)	Timeout (15s)
	9. precondition					Timeout (15s)	0.08	0.06	Timeout (15s)	Timeout (15s)
	10. postcondition					0.11	0.08	0.74	Timeout (15s)	Timeout (15s)
	11. postcondition					0.04	0.08	Timeout (15s)	Timeout (15s)	0.04
	12. postcondition					0.01	0.04	0.01	0.03	0.03
	13. exceptional postcondition					0.01	0.04	0.01	0.03	0.01
	14. precondition					0.01	0.05	0.03	0.04	0.03
	15. precondition					Timeout (15s)	14.90	---	---	---
	introduce_premises
		1. precondition				---	---	---	---	---
		inline_goal
			1. precondition			---	---	---	---	---
			introduce_premises
				1. precondition		---	---	---	---	---
				inline_goal
					1. precondition	Timeout (15s)	14.68	0.15	Timeout (15s)	Timeout (15s)
	16. precondition					0.06	0.50	1.66	Timeout (15s)	Timeout (15s)
	17. precondition					0.02	0.07	0.05	Timeout (15s)	0.03
	18. assertion					0.13	0.20	Timeout (15s)	Timeout (15s)	0.06
	19. precondition					0.01	0.05	0.04	0.05	0.03
	20. precondition					0.10	0.15	2.12	Timeout (15s)	0.04
	21. precondition					0.79	0.22	Timeout (15s)	Timeout (15s)	Timeout (15s)
	22. precondition					Timeout (15s)	1.28	Timeout (15s)	Timeout (15s)	Timeout (15s)
	23. postcondition					0.33	0.10	8.17	Timeout (15s)	Timeout (15s)
	24. postcondition					0.08	0.09	Timeout (15s)	Timeout (15s)	0.04
	25. postcondition					0.01	0.04	0.01	0.03	0.03
	26. exceptional postcondition					0.01	0.04	0.01	0.03	0.02
	27. exceptional postcondition					0.01	0.04	0.01	0.03	0.02
5. VC for is_acyclic						---	---	---	---	---
split_goal_wp
	1. precondition					0.01	0.03	0.01	0.03	0.02
	2. precondition					0.01	0.04	0.03	0.04	0.03
	3. precondition					0.02	0.04	0.05	10.33	0.17
	4. precondition					Timeout (15s)	0.08	0.03	7.21	0.03
	5. assertion					0.01	0.05	0.33	0.07	0.03
	6. assertion					0.32	14.72	Timeout (15s)	Timeout (15s)	Timeout (15s)
	7. postcondition					0.01	0.05	0.01	0.03	0.03
	8. postcondition					0.01	0.04	0.01	0.03	0.02