Why3 Proof Results for Project "bfs2"

Theory "bfs2.Dfs_stack2": fully verified in 6.39 s

Obligations		Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
path_lst_occ		---	---	---
induction_pr
	path_lst_occ.1	0.01	---	---
	path_lst_occ.2	---	---	0.04
path_inv		0.01	---	---
whitepath_suffix		0.02	---	---
whitepath_inv		Timeout (15s) (obsolete)	5.61	---
whitepath_split_lst_occ		Timeout (15s) (obsolete)	0.47	---
6. VC for push_set		0.28	---	---
7. VC for bfs		---	---	---
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.02	---	---
	7. precondition	0.01	---	---
	8. postcondition	0.01	---	---
	9. postcondition	0.01	---	---
	10. postcondition	0.01	---	---
	11. postcondition	0.16	---	---
	12. assertion	0.12	---	---
	13. variant decrease	0.01	---	---
	14. precondition	Timeout (35s) (obsolete)	0.09	---
	15. precondition	0.02	---	---
	16. postcondition	0.02	---	---
	17. postcondition	0.01	---	---
	18. postcondition	0.02	---	---
	19. postcondition	1.78	---	---
8. VC for bfs_main		---	---	---
split_goal_wp
	1. precondition	0.01	---	---
	2. precondition	0.01	---	---
	3. postcondition	---	---	0.17