Why3 Proof Results for Project "dfs_stack2"

Theory "dfs_stack2.Dfs_stack2": fully verified in 6.22 s

Obligations		Alt-Ergo (2.0.0)	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	---	Timeout (35s) (obsolete)	34.63 (obsolete)	0.04
path_inv		---	0.01	---	---
whitepath_suffix		---	0.02	---	---
whitepath_inv		---	Timeout (35s) (obsolete)	5.60	Timeout (35s) (obsolete)
whitepath_split_lst_occ		---	Timeout (35s) (obsolete)	0.47	Timeout (35s) (obsolete)
6. VC for push_set		0.24 (obsolete)	0.12	---	---
7. VC for dfs		---	---	---	---
split_goal_wp
	1. postcondition	0.02 (obsolete)	0.01	---	---
	2. postcondition	0.01 (obsolete)	0.01	---	---
	3. postcondition	0.02 (obsolete)	0.01	---	---
	4. postcondition	0.01 (obsolete)	0.01	---	---
	5. variant decrease	0.01 (obsolete)	0.01	---	---
	6. precondition	0.02 (obsolete)	0.01	---	---
	7. precondition	0.01 (obsolete)	0.01	---	---
	8. postcondition	0.01 (obsolete)	0.01	---	---
	9. postcondition	0.01 (obsolete)	0.01	---	---
	10. postcondition	0.01 (obsolete)	0.01	---	---
	11. postcondition	0.05 (obsolete)	0.17	---	---
	12. assertion	0.09 (obsolete)	0.10	14.92 (obsolete)	Timeout (15s) (obsolete)
	13. variant decrease	0.02 (obsolete)	0.01	---	---
	14. precondition	---	Timeout (35s) (obsolete)	0.15	---
	15. precondition	0.02 (obsolete)	0.02	---	---
	16. postcondition	0.01 (obsolete)	0.02	---	---
	17. postcondition	0.01 (obsolete)	0.01	---	---
	18. postcondition	0.01 (obsolete)	0.02	---	---
	19. postcondition	12.07 (obsolete)	1.57	29.88 (obsolete)	---
8. VC for dfs_main		---	---	---	---
split_goal_wp
	1. precondition	0.01 (obsolete)	0.01	---	---
	2. precondition	0.01 (obsolete)	0.01	---	---
	3. postcondition	Timeout (15s) (obsolete)	Timeout (35s) (obsolete)	---	0.20