Why3 Proof Results for Project "scc"

Theory "scc.SCCTarjan72": fully verified in 2.63 s

Obligations						Alt-Ergo (2.2.0)	CVC3 (2.4.1)	CVC4 (1.5)	CVC4 (1.5-prerelease)	Coq (8.7.2)	Eprover (1.9)	Spass (3.5)	Z3 (4.6.2)
lmem_dec						0.00	---	---	---	---	---	---	---
list_simpl_r						---	---	---	---	---	---	---	---
induction_ty_lex
	list_simpl_r.1					---	---	---	---	---	---	---	---
	split_goal_wp
		list_simpl_r.1.1				0.01	---	---	---	---	---	---	---
		list_simpl_r.1.2				---	---	---	0.08	---	---	---	---
list_assoc_cons						---	---	---	0.06	---	---	---	---
rank_not_mem						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_not_mem.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_not_mem.1.1				0.01	---	---	---	---	---	---	---
		rank_not_mem.1.2				0.01	---	---	---	---	---	---	---
rank_range						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_range.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_range.1.1				0.01	---	---	---	---	---	---	---
		rank_range.1.2				0.01	---	---	---	---	---	---	---
		rank_range.1.3				0.01	---	---	---	---	---	---	---
		rank_range.1.4				0.01	---	---	---	---	---	---	---
rank_min						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_min.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_min.1.1				0.01	---	---	---	---	---	---	---
		rank_min.1.2				---	---	---	2.32	---	---	---	---
rank_app_l						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_app_l.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_app_l.1.1				0.01	---	---	---	---	---	---	---
		rank_app_l.1.2				0.10	---	---	---	---	---	---	---
rank_app_r						---	---	---	---	---	---	---	---
induction_ty_lex
	rank_app_r.1					---	---	---	---	---	---	---	---
	split_goal_wp
		rank_app_r.1.1				0.01	---	---	---	---	---	---	---
		rank_app_r.1.2				0.04	---	---	---	---	---	---	---
simplelist_tl						---	---	---	0.10	---	---	---	---
simplelist_split						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_split.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_split.1.1				---	---	0.10	---	---	---	---	---
		simplelist_split.1.2				---	---	0.11	---	---	---	---	---
		simplelist_split.1.3				---	---	---	0.64	---	---	---	---
		simplelist_split.1.4				---	---	---	0.57	---	---	---	---
simplelist_hd_max_rank						0.02	---	---	---	---	---	---	---
rank_before_suffix						0.18	---	---	---	---	---	---	---
inter_com						---	0.04	---	---	---	---	---	---
inter_add						0.03	---	---	---	---	---	---	---
set_elt						0.04	---	---	---	---	---	---	---
set_mem						---	---	---	---	---	0.03	---	---
inter_subset_inter						---	---	---	---	---	0.15	---	---
subset_add						0.04	---	---	---	---	---	---	---
union_add_l						0.01	---	---	---	---	---	---	---
union_add_r						0.01	---	---	---	---	---	---	---
elts_cons						0.03	---	---	---	---	---	---	---
elts_app						0.02	---	---	---	---	---	---	---
simplelist_app_inter						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_app_inter.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_app_inter.1.1				---	---	---	---	---	0.06	---	---
		simplelist_app_inter.1.2				---	---	1.41	---	---	---	---	---
simplelist_length						---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_length.1					---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_length.1.1				0.01	---	---	---	---	---	---	---
		simplelist_length.1.2				0.01	---	---	---	---	---	---	---
set_of_elt						---	---	---	---	---	---	---	---
split_goal_wp
	set_of_elt.1					0.02	---	---	---	---	---	---	---
	set_of_elt.2					---	---	---	---	---	---	0.73	---
elt_set_of						---	---	---	---	---	0.34	---	---
subset_set_of						0.04	---	---	---	---	---	---	---
reachable_trans						---	0.19	---	---	---	---	---	---
xset_path_xedge						---	---	---	---	---	---	---	---
induction_pr
	xset_path_xedge.1					0.01	---	---	---	---	---	---	---
	xset_path_xedge.2					---	---	---	---	---	0.04	---	---
same_scc_refl						---	---	---	---	---	0.07	---	---
same_scc_sym						0.01	---	---	---	---	---	---	---
same_scc_trans						0.02	---	---	---	---	---	---	---
subscc_add						0.04	---	---	---	---	---	---	---
scc_max						---	---	---	0.22	---	---	---	---
subscc_after_last_gray						---	---	---	---	---	---	---	---
split_goal_wp
	subscc_after_last_gray.1					---	---	---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.1.1				---	---	---	---	---	---	---	---
		split_goal_wp
			subscc_after_last_gray.1.1.1			0.16	---	---	---	---	---	---	---
			subscc_after_last_gray.1.1.2			0.06	---	---	---	---	---	---	---
	subscc_after_last_gray.2					2.58	---	---	---	---	---	---	---
	subscc_after_last_gray.3					---	---	---	1.08	---	---	---	---
	subscc_after_last_gray.4					---	---	---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.4.1				---	---	---	---	---	0.14	---	---
wf_color_postcond_split						---	---	---	---	---	---	---	---
inline_goal
	wf_color_postcond_split.1					---	---	---	---	---	---	---	---
	split_goal_wp
		wf_color_postcond_split.1.1				---	---	---	---	---	0.09	---	---
		wf_color_postcond_split.1.2				---	---	---	---	---	2.11	---	---
wf_color_sccs						---	---	---	0.76	---	---	---	---
wf_color_3_cases						---	---	---	0.17	---	---	---	---
39. VC for split						---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---	---	---
	2. postcondition					0.01	---	---	---	---	---	---	---
	3. postcondition					0.01	---	---	---	---	---	---	---
	4. postcondition					---	0.34	---	---	---	---	---	---
	5. postcondition					0.01	---	---	---	---	---	---	---
	6. postcondition					0.07	---	---	---	---	---	---	---
40. VC for add_stack_incr						---	---	---	---	---	---	---	---
split_goal_wp
	1. index in array bounds					0.01	---	---	---	---	---	---	---
	2. type invariant					0.01	---	---	---	---	---	---	---
	3. postcondition					0.01	---	---	---	---	---	---	---
41. VC for add_blacks						0.01	---	---	---	---	---	---	---
42. VC for set_max_int						---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.02	---	---	---	---	---	---	---
	2. precondition					---	0.50	---	---	---	---	---	---
	3. index in array bounds					---	2.27	---	---	---	---	---	---
	4. postcondition					0.04	---	---	---	---	---	---	---
	5. postcondition					0.04	---	---	---	---	---	---	---
43. VC for dfs1						---	---	---	---	---	---	---	---
split_goal_wp
	1. assertion					---	---	---	---	---	---	---	---
	inline_goal
		1. assertion				---	---	---	---	---	---	---	---
		inline_goal
			1. assertion			---	---	---	30.87	---	---	---	---
	2. index in array bounds					---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.01	---	---	---	---	---	---	---
		2. VC for dfs1				0.01	---	---	---	---	---	---	---
	3. type invariant					0.01	---	---	---	---	---	---	---
	4. precondition					0.02	---	---	---	---	---	---	---
	5. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	0.85	---	---
	6. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. precondition			0.26	---	---	---	---	---	---	---
			2. precondition			---	---	---	---	---	---	---	---
			inline_goal
				1. precondition		---	---	---	---	---	---	---	---
				split_goal_wp
					1. precondition	0.18	---	---	---	---	---	---	---
					2. precondition	0.08	---	---	---	---	---	---	---
					3. precondition	0.09	---	---	---	---	---	---	---
					4. precondition	0.04	---	---	---	---	---	---	---
					5. precondition	0.12	---	---	---	---	---	---	---
					6. precondition	0.10	---	---	---	---	---	---	---
					7. precondition	0.51	---	---	---	---	---	---	---
					8. precondition	0.49	---	---	---	---	---	---	---
					9. precondition	0.02	---	---	---	---	---	---	---
			3. precondition			0.03	---	---	---	---	---	---	---
			4. precondition			0.08	---	---	---	---	---	---	---
			5. precondition			0.89	---	---	---	---	---	---	---
			6. precondition			---	---	---	---	0.89	---	---	---
	7. precondition					---	---	---	---	---	---	---	---
	split_goal_wp
		1. precondition				0.01	---	---	---	---	---	---	---
		2. precondition				0.01	---	---	---	---	---	---	---
		3. precondition				0.01	---	---	---	---	---	---	---
	8. assertion					---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.12	---	---	---	---	---	---	---
		2. VC for dfs1				0.13	---	---	---	---	---	---	---
		3. VC for dfs1				1.80	---	---	---	---	---	---	---
	9. assertion					---	---	---	---	---	2.24	---	---
	10. assertion					---	---	---	---	1.03	---	---	---
	11. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. postcondition			---	---	---	---	---	---	---	---
			inline_goal
				1. postcondition		---	---	---	---	---	---	---	---
				split_goal_wp
					1. postcondition	0.31	---	---	---	---	---	---	---
					2. postcondition	4.50	---	---	---	---	---	---	---
					3. postcondition	0.80	---	---	0.46	---	---	---	---
					4. postcondition	0.68	---	---	---	---	---	---	---
			2. postcondition			---	---	---	---	---	---	---	---
			inline_goal
				1. postcondition		---	---	---	---	---	---	---	---
				split_goal_wp
				1. postcondition	0.04	---	---	---	---	---	---	---
				2. postcondition	0.27	---	---	1.59	---	---	---	---
				3. postcondition	0.06	---	---	---	---	---	---	---
				4. postcondition	0.03	---	---	0.58	---	---	---	---
				5. postcondition	0.28	---	---	1.51	---	---	---	---
				6. postcondition	0.28	---	---	0.98	---	---	---	---
				7. postcondition	0.07	---	---	---	---	---	---	---
				8. postcondition	0.04	---	---	---	---	---	---	---
				9. postcondition	0.03	---	---	0.26	---	---	---	---
3. postcondition			---	---	---	2.30	---	---	---	---
4. postcondition			0.02	---	---	---	---	---	---	---
5. postcondition			0.55	---	---	0.24	---	---	---	---
6. postcondition			---	---	---	3.60	---	---	---	---
12. postcondition					---	---	---	---	---	---	---	---
split_goal_wp
			1. postcondition				0.46	---	---	---	---	---	---	---
			2. postcondition				0.02	---	---	---	---	---	---	---
			3. postcondition				---	---	---	11.70	---	---	---	---
13. postcondition					0.58	---	---	---	---	---	---	---
14. postcondition					---	---	3.32	---	---	---	---	---
15. postcondition					24.15	---	---	---	---	---	---	---
16. postcondition					0.02	---	---	0.13	---	0.06	---	---
17. postcondition					---	---	---	---	---	---	---	---
inline_goal
			1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			2.64	---	---	---	---	---	---	---
		2. VC for dfs1			0.64	---	---	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---	---	---
		4. VC for dfs1			0.45	---	---	---	---	---	---	---
18. assertion					---	---	---	---	1.25	---	---	---
19. assertion					---	---	---	---	---	---	---	---
inline_goal
	1. assertion				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	0.35	---	---	---	---	---
		2. VC for dfs1			0.03	---	---	---	---	---	---	---
		3. VC for dfs1			---	---	---	---	---	4.00	---	---
20. assertion					---	---	---	---	---	---	---	---
split_goal_wp
	1. VC for dfs1				1.47	---	---	---	---	---	---	---
	2. VC for dfs1				0.02	---	---	---	---	---	---	---
21. assertion					0.01	---	---	---	---	---	---	---
22. assertion					---	---	---	---	---	---	---	1.40
23. precondition					0.28	---	---	---	---	---	---	---
24. assertion					---	---	---	---	---	---	---	---
split_goal_wp
	1. assertion				0.02	---	---	---	---	---	---	---
	2. assertion				---	---	---	---	---	---	---	---
	inline_goal
		1. assertion			---	---	---	---	---	---	---	31.64
25. type invariant					0.01	---	---	---	---	---	---	---
26. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. postcondition			---	---	---	---	---	---	---	---
		inline_goal
			1. postcondition		---	---	---	---	---	---	---	---
			split_goal_wp
				1. postcondition	0.28	---	---	---	---	---	---	---
				2. postcondition	1.19	---	---	---	---	---	---	---
				3. postcondition	---	---	---	15.48	---	---	---	---
				4. postcondition	1.17	---	---	---	---	---	---	---
		2. postcondition			---	---	---	---	---	---	---	---
		inline_goal
			1. postcondition		---	---	---	---	---	---	---	---
			split_goal_wp
				1. postcondition	---	---	---	1.80	---	---	---	---
				2. postcondition	0.19	---	---	---	---	---	---	---
				3. postcondition	---	---	---	2.11	---	---	---	---
				4. postcondition	---	---	---	2.66	---	---	---	---
				5. postcondition	---	---	---	2.31	---	---	---	---
				6. postcondition	---	---	---	6.63	---	---	---	---
				7. postcondition	0.21	---	---	---	---	---	---	---
				8. postcondition	0.20	---	---	---	---	---	---	---
				9. postcondition	0.03	---	---	0.30	---	---	---	---
		3. postcondition			2.07	---	---	1.28	---	---	---	---
		4. postcondition			0.02	---	---	---	---	---	---	---
		5. postcondition			0.03	---	---	0.23	---	---	---	---
		6. postcondition			0.10	---	---	0.41	---	---	---	---
27. postcondition					---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition				0.51	---	---	---	---	---	---	---
	2. postcondition				0.03	---	---	---	---	---	---	---
	3. postcondition				---	---	---	---	---	12.35	---	---
28. postcondition					0.28	---	---	0.29	---	0.24	---	---
29. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	0.08	---	---	---	---
30. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				0.05	---	---	0.22	---	---	---	---
31. postcondition					0.02	---	---	0.13	---	0.16	---	---
32. postcondition					---	---	---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	---	---	0.14	---	---
		2. VC for dfs1			0.29	---	---	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---	---	---
		4. VC for dfs1			---	---	---	0.24	---	---	---	---
44. VC for dfs'						---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---	---	---
	2. postcondition					0.01	---	---	---	---	---	---	---
	3. postcondition					0.02	---	---	---	---	---	---	---
	4. postcondition					0.01	---	---	---	---	---	---	---
	5. postcondition					0.02	---	---	---	---	---	---	---
	6. postcondition					0.01	---	---	---	---	---	---	---
	7. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs'			---	0.23	---	---	---	---	---	---
			2. VC for dfs'			0.01	---	---	---	---	---	---	---
			3. VC for dfs'			0.01	---	---	---	---	---	---	---
			4. VC for dfs'			0.01	---	---	---	---	---	---	---
	8. assertion					2.26	---	---	---	---	---	---	---
	9. index in array bounds					0.02	---	---	---	---	---	---	---
	10. index in array bounds					0.01	---	---	---	---	---	---	---
	11. assertion					0.06	---	---	---	---	---	---	---
	12. precondition					0.01	---	---	---	---	---	---	---
	13. precondition					0.02	---	---	---	---	---	---	---
	14. precondition					0.01	---	---	---	---	---	---	---
	15. precondition					0.01	---	---	---	---	---	---	---
	16. postcondition					0.01	---	---	---	---	---	---	---
	17. postcondition					0.01	---	---	---	---	---	---	---
	18. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	15.42	---	0.69	---	---	---	---
	19. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	16.71	---	---	---	---	---	---
	20. postcondition					---	---	---	0.18	---	---	---	---
	21. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				0.33	---	---	---	---	---	---	---
	22. postcondition					0.01	---	---	---	---	---	---	---
	23. precondition					0.01	---	---	---	---	---	---	---
	24. precondition					0.02	---	---	---	---	---	---	---
	25. precondition					0.03	---	---	---	---	---	---	---
	26. precondition					0.01	---	---	---	---	---	---	---
	27. precondition					0.01	---	---	---	---	---	---	---
	28. assertion					---	---	---	---	---	---	---	0.37
	29. precondition					0.01	---	---	---	---	---	---	---
	30. precondition					0.01	---	---	---	---	---	---	---
	31. precondition					0.01	---	---	---	---	---	---	---
	32. precondition					0.01	---	---	---	---	---	---	---
	33. postcondition					0.01	---	---	---	---	---	---	---
	34. postcondition					0.01	---	---	---	---	---	---	---
	35. postcondition					1.02	---	---	---	---	---	---	---
	36. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	0.24	---	---	---	---
	37. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				0.51	---	---	---	---	---	---	---
	38. postcondition					0.02	---	---	---	---	---	---	---
	39. postcondition					---	---	---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs'			---	---	---	---	---	---	---	0.30
			2. VC for dfs'			0.02	---	---	---	---	---	---	---
			3. VC for dfs'			0.02	---	---	---	---	---	---	---
			4. VC for dfs'			0.04	---	---	---	---	---	---	---
45. VC for tarjan						---	---	---	---	---	---	---	---
split_goal_wp
	1. array creation size					0.01	---	---	---	---	---	---	---
	2. precondition					0.01	---	---	---	---	---	---	---
	3. precondition					0.01	---	---	---	---	---	---	---
	4. precondition					---	---	---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---	---	---
		split_goal_wp
			1. precondition			0.05	---	---	---	---	---	---	---
			2. precondition			---	---	---	---	---	---	---	---
			inline_goal
				1. precondition		---	---	---	---	---	---	---	---
				split_goal_wp
					1. precondition	0.02	---	---	---	---	---	---	---
					2. precondition	0.02	---	---	---	---	---	---	---
					3. precondition	0.02	---	---	---	---	---	---	---
					4. precondition	0.02	---	---	0.13	---	---	---	---
					5. precondition	0.02	---	---	0.14	---	---	---	---
					6. precondition	0.02	---	---	---	---	---	---	---
					7. precondition	0.02	---	---	0.12	---	---	---	---
					8. precondition	0.02	---	---	0.13	---	---	---	---
					9. precondition	0.01	---	---	---	---	---	---	---
			3. precondition			0.01	---	---	---	---	---	---	---
			4. precondition			0.01	---	---	---	---	---	---	---
			5. precondition			0.01	---	---	---	---	---	---	---
			6. precondition			0.01	---	---	---	---	---	---	---
	5. precondition					0.01	---	---	---	---	---	---	---
	6. assertion					0.02	---	---	---	---	---	---	---
	7. postcondition					---	---	---	---	---	---	---	---
	split_goal_wp
		1. postcondition				0.29	---	---	---	---	---	---	---
		2. postcondition				0.02	---	---	---	---	---	---	---
		3. postcondition				0.02	---	---	---	---	---	---	---