Why3 Proof Results for Project "dag3"

Theory "dag3.TestAcyclicGraph": fully verified in 0.00 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.04	0.03
	paths_in.2					0.01	0.05	0.03	0.06	Timeout (15s)
2. VC for dfs1						---	---	---	---	---
split_goal_wp
	1. index in array bounds					0.01	0.06	0.04	0.05	0.03
	2. loop invariant init					0.01	0.05	0.02	0.04	0.03
	3. loop invariant init					0.01	0.05	0.02	0.05	0.03
	4. loop invariant init					---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.09	0.27	Timeout (15s)	Timeout (15s)	Timeout (15s)
		2. VC for dfs1				0.01	6.03	Timeout (15s)	Timeout (15s)	Timeout (15s)
		3. VC for dfs1				0.01	0.05	0.02	0.04	0.03
		4. VC for dfs1				0.01	0.06	0.03	0.40	0.03
	5. loop invariant init					---	---	---	---	---
	introduce_premises
		1. loop invariant init				---	---	---	---	---
		inline_goal
			1. loop invariant init			---	---	---	---	---
			introduce_premises
				1. loop invariant init		---	---	---	---	---
				inline_goal
					1. loop invariant init	Timeout (15s)	15.04	0.42	9.49	Timeout (15s)
	6. loop invariant init					0.01	0.07	0.04	0.07	0.03
	7. loop invariant init					0.01	0.09	0.13	9.33	0.03
	8. type invariant					0.01	0.03	0.02	0.05	0.02
	9. index in array bounds					Timeout (15s)	14.41	0.25	5.01	Timeout (15s)
	10. assertion					0.03	0.26	Timeout (15s)	Timeout (15s)	0.05
	11. exceptional postcondition					---	---	---	---	---
	introduce_premises
		1. exceptional postcondition				---	---	---	---	---
		inline_goal
			1. exceptional postcondition			Timeout (15s)	28.83	8.45	2.01	Timeout (15s)
	12. index in array bounds					0.01	0.05	0.02	0.05	0.03
	13. precondition					0.01	0.07	0.03	0.07	0.03
	14. precondition					0.01	0.03	0.02	0.06	0.03
	15. precondition					0.01	0.05	0.02	0.06	0.03
	16. precondition					---	---	---	---	---
	introduce_premises
		1. precondition				---	---	---	---	---
		inline_goal
			1. precondition			---	---	---	---	---
			introduce_premises
				1. precondition		---	---	---	---	---
				inline_goal
					1. precondition	Timeout (15s)	13.95	0.05	2.01	Timeout (15s)
	17. precondition					0.01	0.06	0.02	0.05	0.03
	18. loop invariant preservation					Timeout (15s)	0.51	2.34	9.31	0.06
	19. loop invariant preservation					Timeout (15s)	0.19	0.14	0.15	0.04
	20. loop invariant preservation					0.01	0.06	0.05	0.09	0.03
	21. loop invariant preservation					Timeout (15s)	0.19	0.06	0.21	0.09
	22. loop invariant preservation					0.06	0.16	Timeout (15s)	Timeout (15s)	0.04
	23. loop invariant preservation					0.01	0.06	0.02	0.05	0.03
	24. exceptional postcondition					0.01	0.06	0.02	0.05	0.03
	25. loop invariant preservation					Timeout (15s)	0.30	1.85	5.91	0.05
	26. loop invariant preservation					Timeout (15s)	0.15	0.14	0.14	0.04
	27. loop invariant preservation					0.01	0.06	0.02	0.07	0.03
	28. loop invariant preservation					Timeout (15s)	0.14	0.06	0.18	0.05
	29. loop invariant preservation					0.05	0.29	Timeout (15s)	Timeout (15s)	Timeout (15s)
	30. loop invariant preservation					0.01	0.06	0.02	0.05	0.03
	31. type invariant					0.01	0.04	0.02	0.05	0.02
	32. index in array bounds					0.01	0.06	0.02	0.05	0.03
	33. assertion					0.14	0.31	Timeout (15s)	Timeout (15s)	0.07
	34. postcondition					0.01	0.06	0.03	0.07	0.03
	35. postcondition					---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.35	1.69	Timeout (15s)	Timeout (15s)	Timeout (15s)
		2. VC for dfs1				0.36	1.98	Timeout (15s)	Timeout (15s)	Timeout (15s)
		3. VC for dfs1				0.02	0.10	0.09	4.96	0.03
4. VC for dfs1				0.07	0.10	Timeout (15s)	Timeout (15s)	Timeout (15s)
36. postcondition					11.71	12.19	Timeout (15s)	Timeout (15s)	Timeout (15s)
3. VC for is_acyclic						---	---	---	---	---
split_goal_wp
		1. array creation size					0.01	0.05	0.01	0.03	0.03
	2. assertion					0.01	0.06	Timeout (15s)	Timeout (15s)	0.03
	3. assertion					0.02	0.06	0.17	0.05	0.11
	4. postcondition					0.02	0.07	0.17	0.05	0.03
	5. loop invariant init					0.01	0.03	Timeout (15s)	Timeout (15s)	0.02
	6. loop invariant init					0.02	0.29	Timeout (15s)	Timeout (15s)	Timeout (15s)
	7. loop invariant init					Timeout (15s)	0.14	0.07	Timeout (15s)	0.04
	8. type invariant					0.01	0.03	0.01	0.04	0.02
	9. index in array bounds					0.01	0.05	0.91	6.46	0.03
	10. precondition					0.01	0.06	0.03	0.06	0.03
	11. precondition					0.01	0.03	0.01	0.05	0.03
	12. precondition					0.01	0.05	0.02	0.05	0.03
	13. precondition					0.01	0.06	0.04	0.06	0.03
	14. precondition					0.01	0.05	0.02	0.04	0.03
	15. loop invariant preservation					0.01	0.99	Timeout (15s)	Timeout (15s)	Timeout (15s)
	16. loop invariant preservation					0.01	0.05	0.04	0.07	0.03
	17. loop invariant preservation					0.01	0.05	0.02	0.04	0.03
	18. postcondition					0.01	0.06	0.02	0.05	0.03
	19. loop invariant preservation					0.01	0.11	Timeout (15s)	Timeout (15s)	Timeout (15s)
	20. loop invariant preservation					0.01	0.05	0.02	0.05	0.03
	21. loop invariant preservation					0.01	0.05	0.02	0.04	0.03
	22. assertion					0.01	0.13	Timeout (15s)	Timeout (15s)	0.87
	23. assertion					0.38	29.35	Timeout (15s)	Timeout (15s)	Timeout (15s)
	24. postcondition					0.01	0.06	0.02	0.04	0.03