Why3 Proof Results for Project "dfs66"

Theory "dfs66.DfsWhitePathGraySoundness": fully verified in 3.56 s

Obligations			Alt-Ergo (2.0.0)	CVC4 (1.5)	Eprover (1.9)	Z3 (4.4.0)
whiteaccess_var			0.01	---	---	---
whiteaccess_covar1			0.01	---	---	---
wpath_covar2			Timeout (15s)	14.80	Timeout (15s)	---
induction_pr
	wpath_covar2.1		0.01	---	---	---
	wpath_covar2.2		Timeout (15s)	0.06	0.03	---
whiteaccess_covar2			Timeout (15s)	0.06	---	---
wpath_trans			Timeout (15s)	14.83	Timeout (15s)	---
induction_pr
	wpath_trans.1		0.01	---	---	---
	wpath_trans.2		Timeout (15s)	0.04	0.03	---
whiteaccess_trans			Timeout (15s)	0.13	---	---
whiteaccess_cons			Timeout (15s)	3.35	Timeout (15s)	---
8. VC for dfs			---	---	---	---
split_goal_wp
	1. postcondition		0.01	---	---	---
	2. postcondition		0.01	---	---	---
	3. postcondition		0.00	---	---	---
	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		---	---	---	---
	split_goal_wp
		1. VC for dfs	0.01	---	---	---
		2. VC for dfs	0.01	---	---	---
		3. VC for dfs	0.01	---	---	---
	20. assertion		0.01	---	---	---
	21. assertion		Timeout (15s) (obsolete)	29.66 (obsolete)	Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs	0.33	---	---	---
		2. VC for dfs	7.69	15.31 (obsolete)	Timeout (15s) (obsolete)	Timeout (15s) (obsolete)
	22. variant decrease		0.02	---	---	---
	23. precondition		0.02	---	---	---
	24. precondition		0.01	---	---	---
	25. precondition		0.01	---	---	---
	26. precondition		0.28	---	---	---
	27. assertion		Timeout (15s) (obsolete)	Timeout (15s) (obsolete)	Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs	0.02	---	---	---
		2. VC for dfs	0.01	---	---	---
		3. VC for dfs	0.24	29.41 (obsolete)	Timeout (15s) (obsolete)	---
	28. assertion		1.76	29.73 (obsolete)	Timeout (15s) (obsolete)	---
	29. postcondition		0.01	---	---	---
	30. postcondition		0.01	---	---	---
	31. postcondition		0.01	---	---	---
	32. postcondition		0.84	29.44 (obsolete)	Timeout (15s) (obsolete)	---