Why3 Proof Results for Project "scc"

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

Obligations						Alt-Ergo (2.2.0)	CVC4 (1.5)	Coq (8.7.2)	Eprover (1.9)	Spass (3.5)	Z3 (4.4.0)
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.11	---	---	---	---
list_assoc_cons						---	0.07	---	---	---	---
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				---	0.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.11	---	---	---	---
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.80	---	---	---	---
		simplelist_split.1.4				---	0.57	---	---	---	---
simplelist_hd_max_rank						0.02	---	---	---	---	---
rank_before_suffix						0.18	---	---	---	---	---
inter_com						---	0.05	---	---	---	---
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.18	---	---
		simplelist_app_inter.1.2				---	1.38	---	---	---	---
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					---	---	---	---	3.21	---
elt_set_of						---	---	---	0.17	---	---
subset_set_of						0.04	---	---	---	---	---
reachable_trans						---	0.07	---	---	---	---
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.27	---	---	---	---
subscc_after_last_gray						---	---	---	---	---	---
split_goal_wp
	subscc_after_last_gray.1					---	0.51	---	---	---	---
	subscc_after_last_gray.2					2.28	---	---	---	---	---
	subscc_after_last_gray.3					---	1.03	---	---	---	---
	subscc_after_last_gray.4					---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.4.1				---	---	---	0.14	---	---
wf_color_postcond_split						---	0.32	---	---	---	---
wf_color_sccs						---	0.33	---	---	---	---
wf_color_3_cases						---	0.15	---	---	---	---
39. VC for split						---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---
	2. postcondition					0.01	---	---	---	---	---
	3. postcondition					0.01	---	---	---	---	---
	4. postcondition					---	0.14	---	---	---	---
	5. postcondition					0.01	---	---	---	---	---
	6. postcondition					0.05	---	---	---	---	---
40. VC for add_stack_incr						0.01	---	---	---	---	---
41. VC for add_blacks						0.01	---	---	---	---	---
42. VC for set_max_int						0.02	---	---	---	---	---
43. VC for dfs1						---	---	---	---	---	---
split_goal_wp
	1. precondition					0.03	---	---	---	---	---
	2. precondition					---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	0.83	---	---
	3. precondition					---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---
		split_goal_wp
			1. precondition			---	---	---	---	---	---
			inline_goal
				1. precondition		---	---	---	---	---	---
				split_goal_wp
					1. precondition	0.02	---	---	---	---	---
					2. precondition	0.07	---	---	---	---	---
					3. precondition	0.03	---	---	---	---	---
					4. precondition	0.03	---	---	---	---	---
			2. precondition			---	---	---	---	---	---
			inline_goal
				1. precondition		---	---	---	---	---	---
				split_goal_wp
					1. precondition	0.14	---	---	---	---	---
					2. precondition	0.06	---	---	---	---	---
					3. precondition	0.11	---	---	---	---	---
					4. precondition	0.02	---	---	---	---	---
					5. precondition	0.11	---	---	---	---	---
					6. precondition	0.05	---	---	---	---	---
					7. precondition	0.39	---	---	---	---	---
					8. precondition	0.25	---	---	---	---	---
			3. precondition			0.02	---	---	---	---	---
			4. precondition			0.11	---	---	---	---	---
			5. precondition			2.55	---	---	---	---	---
			6. precondition			---	2.25	---	---	---	---
	4. precondition					---	---	---	---	---	---
	split_goal_wp
		1. precondition				0.01	---	---	---	---	---
		2. precondition				0.01	---	---	---	---	---
		3. precondition				0.01	---	---	---	---	---
	5. assertion					---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1				0.68	---	---	---	---	---
		2. VC for dfs1				0.70	---	---	---	---	---
		3. VC for dfs1				2.06	---	---	---	---	---
	6. assertion					---	---	---	1.61	---	---
	7. assertion					---	---	1.08	---	---	---
	8. postcondition					---	---	---	---	---	---
	inline_goal
		1. postcondition				---	---	---	---	---	---
		split_goal_wp
			1. postcondition			---	---	---	---	---	---
			inline_goal
				1. postcondition		---	---	---	---	---	---
				split_goal_wp
					1. postcondition	0.07	---	---	---	---	---
					2. postcondition	6.05	---	---	---	---	---
					3. postcondition	---	0.26	---	---	---	---
					4. postcondition	0.16	---	---	---	---	---
			2. postcondition			---	---	---	---	---	---
			inline_goal
				1. postcondition		---	---	---	---	---	---
				split_goal_wp
					1. postcondition	---	0.27	---	---	---	---
					2. postcondition	0.16	---	---	---	---	---
					3. postcondition	---	0.23	---	---	---	---
					4. postcondition	---	0.23	---	---	---	---
5. postcondition					---	0.72	---	---	---	---
6. postcondition					---	0.76	---	---	---	---
7. postcondition					---	---	---	3.69	---	---
8. postcondition					---	---	---	3.64	---	---
3. postcondition			---	1.21	---	---	---	---
4. postcondition			0.02	---	---	---	---	---
5. postcondition			---	0.23	---	---	---	---
6. postcondition			---	1.74	---	---	---	---
9. postcondition					---	---	---	---	---	---
split_goal_wp
			1. postcondition				0.30	---	---	---	---	---
			2. postcondition				0.03	---	---	---	---	---
			3. postcondition				---	---	---	---	---	10.74
10. postcondition					0.51	---	---	---	---	---
11. postcondition					---	0.79	---	---	---	---
12. postcondition					---	---	---	---	---	---
inline_goal
			1. postcondition				0.80	---	---	---	---	---
13. postcondition					0.01	---	---	---	---	---
14. postcondition					---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	1.47	---	---
		2. VC for dfs1			0.15	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---
		4. VC for dfs1			---	---	---	0.33	---	---
15. assertion					---	---	1.31	---	---	---
16. assertion					---	---	---	---	---	---
inline_goal
	1. assertion				---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	0.35	---	---	---	---
		2. VC for dfs1			0.03	---	---	---	---	---
		3. VC for dfs1			---	---	---	7.19	---	---
17. assertion					---	---	---	---	---	---
split_goal_wp
	1. VC for dfs1				1.33	---	---	---	---	---
	2. VC for dfs1				0.02	---	---	---	---	---
18. postcondition					---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---
	split_goal_wp
		1. postcondition			---	---	---	---	---	---
		inline_goal
			1. postcondition		---	---	---	---	---	---
			split_goal_wp
				1. postcondition	0.06	---	---	---	---	---
				2. postcondition	0.93	---	---	---	---	---
				3. postcondition	---	2.02	---	---	---	---
				4. postcondition	0.78	---	---	---	---	---
		2. postcondition			---	---	---	---	---	---
		inline_goal
			1. postcondition		---	---	---	---	---	---
			split_goal_wp
				1. postcondition	0.14	---	---	---	---	---
				2. postcondition	0.11	---	---	---	---	---
				3. postcondition	0.40	---	---	---	---	---
				4. postcondition	---	---	---	2.19	---	---
				5. postcondition	0.25	---	---	---	---	---
				6. postcondition	0.23	---	---	---	---	---
				7. postcondition	---	---	---	12.63	---	---
				8. postcondition	---	---	---	12.43	---	---
		3. postcondition			1.27	---	---	---	---	---
		4. postcondition			0.01	---	---	---	---	---
		5. postcondition			0.02	---	---	---	---	---
		6. postcondition			0.09	---	---	---	---	---
19. postcondition					---	---	---	---	---	---
split_goal_wp
	1. postcondition				0.52	---	---	---	---	---
	2. postcondition				0.02	---	---	---	---	---
	3. postcondition				---	---	---	5.19	---	---
20. postcondition					0.22	---	---	---	---	---
21. postcondition					---	---	---	---	---	---
inline_goal
	1. postcondition				---	0.06	---	---	---	---
22. postcondition					0.03	---	---	---	---	---
23. postcondition					0.02	---	---	---	---	---
24. postcondition					---	---	---	---	---	---
inline_goal
	1. postcondition				---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1			---	---	---	0.10	---	---
		2. VC for dfs1			0.02	---	---	---	---	---
		3. VC for dfs1			0.02	---	---	---	---	---
		4. VC for dfs1			---	---	---	1.61	---	---
44. VC for dfs						---	---	---	---	---	---
split_goal_wp
	1. postcondition					0.01	---	---	---	---	---
	2. postcondition					0.02	---	---	---	---	---
	3. postcondition					0.02	---	---	---	---	---
	4. postcondition					0.01	---	---	---	---	---
	5. postcondition					0.02	---	---	---	---	---
	6. postcondition					0.02	---	---	---	---	---
	7. postcondition					---	---	---	---	---	---
	introduce_premises
		1. postcondition				---	---	---	---	---	---
		inline_goal
			1. postcondition			---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs		---	0.12	---	---	---	---
				2. VC for dfs		0.02	---	---	---	---	---
				3. VC for dfs		0.01	---	---	---	---	---
				4. VC for dfs		0.01	---	---	---	---	---
	8. assertion					2.21	---	---	---	---	---
	9. precondition					0.02	---	---	---	---	---
	10. precondition					0.02	---	---	---	---	---
	11. precondition					0.01	---	---	---	---	---
	12. precondition					0.02	---	---	---	---	---
	13. postcondition					0.02	---	---	---	---	---
	14. postcondition					0.02	---	---	---	---	---
	15. postcondition					1.64	---	---	---	---	---
	16. postcondition					---	---	---	---	---	---
	introduce_premises
		1. VC for dfs				---	---	---	---	---	---
		inline_goal
			1. VC for dfs			4.41	---	---	---	---	---
	17. postcondition					0.02	---	---	---	---	---
	18. postcondition					0.42	---	---	---	---	---
	19. postcondition					0.02	---	---	---	---	---
	20. precondition					0.02	---	---	---	---	---
	21. precondition					0.02	---	---	---	---	---
	22. precondition					0.04	---	---	---	---	---
	23. precondition					0.01	---	---	---	---	---
	24. precondition					0.02	---	---	---	---	---
	25. precondition					0.02	---	---	---	---	---
	26. precondition					0.02	---	---	---	---	---
	27. precondition					0.02	---	---	---	---	---
	28. precondition					0.02	---	---	---	---	---
	29. postcondition					0.02	---	---	---	---	---
	30. postcondition					0.02	---	---	---	---	---
	31. postcondition					13.30	4.99	---	---	---	---
	32. postcondition					0.57	---	---	---	---	---
	33. postcondition					3.24	---	---	---	---	---
	34. postcondition					0.08	---	---	---	---	---
	35. postcondition					12.68	---	---	---	---	---
45. VC for tarjan						---	---	---	---	---	---
split_goal_wp
	1. precondition					0.01	---	---	---	---	---
	2. precondition					0.01	---	---	---	---	---
	3. precondition					---	---	---	---	---	---
	inline_goal
		1. precondition				---	---	---	---	---	---
		split_goal_wp
			1. precondition			0.05	---	---	---	---	---
			2. precondition			0.04	---	---	---	---	---
			3. precondition			0.01	---	---	---	---	---
			4. precondition			0.01	---	---	---	---	---
			5. precondition			0.01	---	---	---	---	---
			6. precondition			0.01	---	---	---	---	---
	4. precondition					0.01	---	---	---	---	---
	5. assertion					0.02	---	---	---	---	---
	6. postcondition					---	---	---	---	---	---
	split_goal_wp
		1. postcondition				0.22	---	---	---	---	---
		2. postcondition				0.02	---	---	---	---	---
		3. postcondition				0.02	---	---	---	---	---