Why3 Proof Results for Project "dfs16"

Theory "dfs16.DfsWhitePathSoundness": fully verified in 0.00 s

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
nbtw_path			---	---	---
induction_pr
	nbtw_path.1		0.01	---	---
	nbtw_path.2		0.01	---	---
2. VC for dfs			---	---	---
split_goal_wp
	1. postcondition		0.01	---	---
	2. postcondition		0.01	---	---
	3. postcondition		0.01	---	---
	4. postcondition		0.01	---	---
	5. postcondition		0.03	---	---
	6. index in array bounds		Timeout (15s)	---	---
	split_goal_wp
		1. VC for dfs	Timeout (15s)	9.42	0.04
		2. VC for dfs	Timeout (15s)	8.93	0.04
	7. precondition		0.02	---	---
	8. precondition		0.01	---	---
	9. precondition		0.01	---	---
	10. precondition		0.01	---	---
	11. postcondition		0.01	---	---
	12. postcondition		0.01	---	---
	13. postcondition		0.01	---	---
	14. postcondition		0.02	---	---
	15. postcondition		0.09	---	---
	16. index in array bounds		0.01	---	---
	17. precondition		0.01	---	---
	18. precondition		0.02	---	---
	19. precondition		0.01	---	---
	20. precondition		0.02	---	---
	21. assertion		0.10	---	---
	22. precondition		0.04	---	---
	23. precondition		0.01	---	---
	24. precondition		0.01	---	---
	25. precondition		0.01	---	---
	26. assertion		0.10	---	---
	27. postcondition		0.01	---	---
	28. postcondition		0.06	---	---
	29. postcondition		0.02	---	---
	30. postcondition		0.03	---	---
	31. postcondition		1.43	---	---