Why3 Proof Results for Project "dfs77"

Theory "dfs77.DFSWhitePathGrayCompteness": fully verified in 0.21 s

Obligations			Alt-Ergo (2.0.0)	CVC4 (1.5)	Coq (8.7.1)	Eprover (1.9)	Spass (3.5)	Z3 (4.4.0)
whiteaccess_var			0.01	---	---	---	---	---
whiteaccess_minus			0.01	---	---	---	---	---
nbtw_path			---	---	---	---	---	---
induction_pr
	nbtw_path.1		---	0.05	---	---	---	---
	nbtw_path.2		Timeout (5s)	0.05	---	---	---	---
nbtw_whiteaccess			0.01	---	---	---	---	---
diff_empty			Timeout (15s)	0.06	---	---	---	---
whiteaccess_roots_result			0.12	---	---	---	---	---
7. VC for dfs			---	---	---	---	---	---
split_goal_wp
	1. postcondition		0.01	---	---	---	---	---
	2. postcondition		0.01	---	---	---	---	---
	3. postcondition		0.00	---	---	---	---	---
	4. postcondition		0.10	---	---	---	---	---
	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		1.07	---	---	---	---	---
	14. variant decrease		0.01	---	---	---	---	---
	15. precondition		0.01	---	---	---	---	---
	16. precondition		0.01	---	---	---	---	---
	17. precondition		0.01	---	---	---	---	---
	18. precondition		0.03	---	---	---	---	---
	19. assertion		0.47	---	---	---	---	---
	20. variant decrease		0.02	---	---	---	---	---
	21. precondition		0.02	---	---	---	---	---
	22. precondition		0.02	---	---	---	---	---
	23. precondition		0.01	---	---	---	---	---
	24. precondition		0.17	---	---	---	---	---
	25. assertion		3.46	---	---	---	---	---
	26. postcondition		0.01	---	---	---	---	---
	27. postcondition		0.01	---	---	---	---	---
	28. postcondition		0.01	---	---	---	---	---
	29. postcondition		---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs	---	0.15	---	---	---	---
		2. VC for dfs	7.66	6.15	---	---	---	---
		3. VC for dfs	Timeout (5s) (obsolete)	0.09	Not yet run (obsolete)	Timeout (5s) (obsolete)	Timeout (15s) (obsolete)	Timeout (15s) (obsolete)