Why3 Proof Results for Project "dfs23"

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

Obligations			Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
nbtw_wpath			---	---	---
induction_pr
	nbtw_wpath.1		0.01	---	---
	nbtw_wpath.2		0.01	---	---
path_wpathempty			---	---	---
induction_pr
	path_wpathempty.1		0.01	---	---
	path_wpathempty.2		0.01	---	---
nbtw_path			---	---	---
induction_pr
	nbtw_path.1		0.01	---	---
	nbtw_path.2		0.01	---	---
4. VC for dfs1			---	---	---
split_goal_wp
	1. assertion		0.01	---	---
	2. index in array bounds		0.01	---	---
	3. loop invariant init		0.01	---	---
	4. loop invariant init		0.01	---	---
	5. loop invariant init		0.02	---	---
	6. loop invariant init		0.01	---	---
	7. loop invariant init		0.01	---	---
	8. loop invariant init		0.01	---	---
	9. loop invariant init		0.01	---	---
	10. type invariant		0.01	---	---
	11. index in array bounds		---	---	---
	split_goal_wp
		1. VC for dfs1	---	---	0.12
		2. VC for dfs1	---	---	0.11
	12. precondition		0.01	---	---
	13. precondition		0.01	---	---
	14. precondition		0.01	---	---
	15. loop invariant preservation		---	0.50	---
	16. loop invariant preservation		0.01	---	---
	17. loop invariant preservation		0.02	---	---
	18. loop invariant preservation		0.01	---	---
	19. loop invariant preservation		0.05	---	---
	20. loop invariant preservation		0.08	---	---
	21. loop invariant preservation		---	0.18	---
	22. loop invariant preservation		---	0.30	---
	23. loop invariant preservation		0.01	---	---
	24. loop invariant preservation		0.01	---	---
	25. loop invariant preservation		0.01	---	---
	26. loop invariant preservation		0.02	---	---
	27. loop invariant preservation		0.01	---	---
	28. loop invariant preservation		---	0.13	---
	29. assertion		0.10	---	---
	30. type invariant		0.01	---	---
	31. index in array bounds		0.01	---	---
	32. postcondition		0.04	---	---
	33. postcondition		0.03	---	---
	34. postcondition		0.02	---	---
	35. postcondition		---	---	---
	split_goal_wp
		1. VC for dfs1	0.06	---	---
		2. VC for dfs1	0.12	---	---
5. VC for dfs_main			---	---	---
split_goal_wp
	1. array creation size		0.01	---	---
	2. loop invariant init		0.01	---	---
	3. loop invariant init		0.01	---	---
	4. loop invariant init		0.01	---	---
	5. loop invariant init		0.01	---	---
	6. loop invariant init		0.01	---	---
	7. loop invariant init		0.01	---	---
	8. type invariant		0.01	---	---
	9. index in array bounds		---	15.77	0.09
	10. precondition		0.01	---	---
	11. precondition		0.01	---	---
	12. precondition		0.01	---	---
	13. loop invariant preservation		---	0.28	---
	14. loop invariant preservation		0.02	---	---
	15. loop invariant preservation		0.01	---	---
	16. loop invariant preservation		0.04	---	---
	17. loop invariant preservation		0.03	---	---
	18. loop invariant preservation		---	0.14	---
	19. loop invariant preservation		---	0.19	---
	20. loop invariant preservation		0.01	---	---
	21. loop invariant preservation		0.01	---	---
	22. loop invariant preservation		0.01	---	---
	23. loop invariant preservation		0.02	---	---
	24. loop invariant preservation		---	0.11	---
	25. assertion		0.02	---	---
	26. assertion		0.02	---	---
	27. postcondition		0.01	---	---
	28. postcondition		0.01	---	---
	29. loop invariant init		0.01	---	---
	30. type invariant		0.01	---	---
	31. index in array bounds		0.01	---	---
	32. loop invariant preservation		0.02	---	---
	33. loop invariant preservation		0.02	---	---
	34. assertion		0.04	---	---
	35. postcondition		0.01	---	---
	36. postcondition		0.01	---	---