Why3 Proof Results for Project "nbtw4"

Theory "nbtw4.Dfs_nbtw": fully verified in 0.07 s

Obligations		Alt-Ergo (2.0.0)	CVC4 (1.5)	Eprover (1.9)
reachable_succ		---	---	0.02
reachable_trans		---	---	---
induction_pr
	reachable_trans.1	0.01	---	---
	reachable_trans.2	0.01	---	---
black_to_white_path_goes_thru_gray		---	---	---
induction_pr
	black_to_white_path_goes_thru_gray.1	0.00	---	---
	black_to_white_path_goes_thru_gray.2	0.01	---	---
4. VC for dfs		---	---	---
split_goal_wp
	1. postcondition	0.01	---	---
	2. postcondition	0.01	---	---
	3. postcondition	0.01	---	---
	4. postcondition	---	---	0.03
	5. variant decrease	0.01	---	---
	6. precondition	0.01	---	---
	7. precondition	0.01	---	---
	8. precondition	0.00	---	---
	9. postcondition	0.01	---	---
	10. postcondition	0.00	---	---
	11. postcondition	0.01	---	---
	12. postcondition	0.07	---	---
	13. variant decrease	0.01	---	---
	14. precondition	0.01	---	---
	15. precondition	0.01	---	---
	16. precondition	0.01	---	---
	17. assertion	---	0.93	---
	18. variant decrease	0.01	---	---
	19. precondition	0.01	---	---
	20. precondition	0.00	---	---
	21. precondition	0.13	---	---
	22. postcondition	0.01	---	---
	23. postcondition	0.01	---	---
	24. postcondition	0.01	---	---
	25. postcondition	---	5.09	---
5. VC for dfs_main		0.05	---	---