Why3 Proof Results for Project "dfs33"

Theory "dfs33.DfsWhitePathSoundness": not fully verified

Obligations					Alt-Ergo (2.1.0)	CVC4 (1.4)	CVC4 (1.5)	Eprover (1.9)	Z3 (4.6.3)
whiteaccess_var					0.01 (obsolete)	---	---	---	---
whiteaccess_covar1					0.01 (obsolete)	---	---	---	---
wpath_covar2					Timeout (15s) (obsolete)	---	---	---	---
whiteaccess_covar2					Timeout (15s) (obsolete)	---	---	---	---
wpath_trans					Timeout (15s) (obsolete)	---	---	---	---
whiteaccess_trans					Timeout (15s) (obsolete)	---	---	---	---
whiteaccess_cons					Timeout (15s) (obsolete)	---	---	---	---
whiteaccess_union					0.02 (obsolete)	---	---	---	---
path_wpathempty					Timeout (15s) (obsolete)	---	---	---	---
diff_inc					---	---	---	---	---
split_goal_wp
	diff_inc.1				0.02 (obsolete)	---	---	---	---
	diff_inc.2				0.01 (obsolete)	---	---	---	---
11. VC for dfs1					---	---	---	---	---
split_goal_wp
	1. assertion				0.01	---	---	---	---
	2. index in array bounds				0.01	---	0.07	---	---
	3. index in array bounds				0.01	---	---	---	---
	4. loop invariant init				0.01	---	---	---	---
	5. loop invariant init				0.01	---	---	---	---
	6. loop invariant init				0.02	---	---	---	---
	7. loop invariant init				0.02	---	---	---	---
	8. loop invariant init				0.01	---	---	---	---
	9. loop invariant init				0.01	---	---	---	---
	10. type invariant				0.01	---	0.04	---	---
	11. index in array bounds				Timeout (15s) (obsolete)	---	14.20 (obsolete)	0.11	---
	12. precondition				0.01	---	---	---	---
	13. precondition				0.01	---	---	---	---
	14. precondition				0.01	---	---	---	---
	15. precondition				0.02	---	---	---	---
	16. loop invariant preservation				Timeout (15s) (obsolete)	---	0.55	0.40	---
	17. loop invariant preservation				0.03	---	---	---	---
	18. loop invariant preservation				0.02	---	---	---	---
	19. loop invariant preservation				Not yet run	---	29.89 (obsolete)	Timeout (15s) (obsolete)	Timeout (15s) (obsolete)
	20. loop invariant preservation				0.01	---	---	---	---
	21. loop invariant preservation				Timeout (15s) (obsolete)	---	0.20	0.09	---
	22. loop invariant preservation				Timeout (15s) (obsolete)	---	0.33	0.39	---
	23. loop invariant preservation				0.01	---	---	---	---
	24. loop invariant preservation				0.02	---	---	---	---
	25. loop invariant preservation				0.06	---	---	---	---
	26. loop invariant preservation				0.02	---	---	---	---
	27. loop invariant preservation				Timeout (15s) (obsolete)	---	0.16	0.09	---
	28. assertion				Timeout (15s) (obsolete)	---	14.06 (obsolete)	Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs1			0.03	---	---	---	---
		2. VC for dfs1			0.09	---	---	---	---
	29. assertion				0.01	---	0.09	---	---
	30. assertion				---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			0.03	---	---	---	---
		2. VC for dfs1			0.12	---	---	---	---
		3. VC for dfs1			0.09	---	---	---	---
	31. type invariant				0.01	---	---	---	---
	32. index in array bounds				0.01	---	---	---	---
	33. postcondition				0.06	---	0.13	---	---
	34. postcondition				Not yet run	14.86	---	Timeout (15s)	---
	35. postcondition				0.04	---	0.13	---	---
	36. postcondition				0.01	---	0.04	0.02	---
12. VC for dfs_main					Timeout (15s) (obsolete)	---	---	---	---
split_goal_wp
	1. array creation size				0.01	---	---	---	---
	2. assertion				0.01	---	---	---	---
	3. assertion				Timeout (15s)	---	15.41 (obsolete)	---	---
	4. postcondition				Timeout (15s) (obsolete)	---	28.94 (obsolete)	Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs_main			0.01	---	15.46 (obsolete)	Timeout (15s) (obsolete)	---
		2. VC for dfs_main			0.01	---	0.10	---	---
	5. loop invariant init				0.01	---	---	---	---
	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				0.01	---	---	---	---
	12. precondition				0.01	---	---	---	---
	13. precondition				0.01	---	13.82 (obsolete)	Timeout (15s) (obsolete)	---
	14. precondition				0.01	---	---	---	---
	15. precondition				0.01	---	---	---	---
	16. loop invariant preservation				0.02	---	---	---	---
	17. loop invariant preservation				0.02	---	---	---	---
	18. loop invariant preservation				0.01	---	---	---	---
	19. loop invariant preservation				---	---	---	---	---
	introduce_premises
		1. loop invariant preservation			---	---	---	---	---
		inline_goal
			1. loop invariant preservation		---	---	---	0.90	---
	20. loop invariant preservation				0.07	---	---	---	---
	21. loop invariant preservation				0.01	---	---	---	---
	22. loop invariant preservation				0.01	---	---	---	---
	23. loop invariant preservation				0.01	---	---	---	---
	24. loop invariant preservation				0.03	---	---	---	---
	25. loop invariant preservation				0.05	---	---	---	---
	26. assertion				0.01	---	---	---	---
	27. assertion				Timeout (15s)	---	29.87	Timeout (15s)	---
	28. type invariant				0.01	---	---	---	---
	29. postcondition				Timeout (15s) (obsolete)	---	26.71 (obsolete)	Timeout (15s) (obsolete)	---
	split_goal_wp
		1. VC for dfs_main			0.01	14.55 (obsolete)	29.46 (obsolete)	Timeout (15s) (obsolete)	---
		2. VC for dfs_main			0.02	---	---	---	---
13. VC for test					---	---	---	---	---
split_goal_wp
	1. array creation size				0.01	---	---	---	---
	2. assertion				0.01	---	---	---	---
	3. assertion				Timeout (15s) (obsolete)	---	---	---	---
	introduce_premises
		1. assertion			---	---	---	---	---
		inline_goal
			1. assertion		---	---	---	---	---
			split_goal_wp
				1. assertion	Timeout (15s)	---	Timeout (15s)	Timeout (15s)	Timeout (15s) (obsolete)
				2. assertion	0.01	---	---	---	---