Why3 Proof Results for Project "dfs8"

Theory "dfs8.DfsUndirNoWhiteToBlack": fully verified in 0.00 s

Obligations			Alt-Ergo (2.0.0)	CVC4 (1.5)
1. VC for dfs			---	---
split_goal_wp
	1. postcondition		0.01	---
	2. postcondition		0.01	---
	3. postcondition		0.01	---
	4. postcondition		0.01	---
	5. variant decrease		0.01	---
	6. precondition		0.01	---
	7. precondition		0.01	---
	8. precondition		0.01	---
	9. precondition		0.01	---
	10. postcondition		0.01	---
	11. postcondition		0.01	---
	12. postcondition		0.01	---
	13. postcondition		0.01	---
	14. variant decrease		0.01	---
	15. precondition		0.01	---
	16. precondition		0.01	---
	17. precondition		0.01	---
	18. precondition		0.03	---
	19. assertion		0.30	---
	20. variant decrease		0.02	---
	21. precondition		0.01	---
	22. precondition		0.01	---
	23. precondition		0.01	---
	24. precondition		0.18	---
	25. assertion		2.10	---
	26. postcondition		0.01	---
	27. postcondition		0.01	---
	28. postcondition		0.01	---
	29. postcondition		Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs	0.03	---
		2. VC for dfs	Timeout (15s) (obsolete)	1.70
		3. VC for dfs	0.04	---