Why3 Proof Results for Project "scc"

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

Obligations								Alt-Ergo (2.2.0)	CVC4 (1.5)	Coq (8.7.2)	Eprover (1.9)	Spass (3.5)	Z3 (4.6.2)	Z3 (4.6.3)
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.08	---	---	---	---	---
precedes_mem								0.05	---	---	---	---	---	---
head_precedes								Timeout (15s)	0.10	---	---	---	---	---
precedes_tail								Timeout (15s)	2.14	---	---	---	---	---
tail_not_precedes								0.02	---	---	---	---	---	---
split_list_precedes								Timeout (15s)	6.67	---	---	---	---	---
precedes_refl								0.02	---	---	---	---	---	---
precedes_append_left								0.05	---	---	---	---	---	---
precedes_append_left_iff								Timeout (15s)	13.79	---	Timeout (15s)	---	---	---
induction_ty_lex
	precedes_append_left_iff.1							---	---	---	---	---	---	---
	split_goal_wp
		precedes_append_left_iff.1.1						0.02	---	---	---	---	---	---
		precedes_append_left_iff.1.2						0.02	---	---	---	---	---	---
		precedes_append_left_iff.1.3						0.02	---	---	---	---	---	---
		precedes_append_left_iff.1.4						0.01	---	---	---	---	---	---
precedes_append_right								1.07	---	---	---	---	---	---
precedes_append_right_iff								Timeout (15s)	14.24	---	Timeout (15s)	---	---	---
induction_ty_lex
	precedes_append_right_iff.1							---	---	---	---	---	---	---
	split_goal_wp
		precedes_append_right_iff.1.1						0.02	---	---	---	---	---	---
		precedes_append_right_iff.1.2						0.02	---	---	---	---	---	---
		precedes_append_right_iff.1.3						0.06	---	---	---	---	---	---
		precedes_append_right_iff.1.4						0.01	---	---	---	---	---	---
simplelist_tl								---	0.26	---	---	---	---	---
simplelist_split								---	---	---	---	---	---	---
induction_ty_lex
	simplelist_split.1							---	---	---	---	---	---	---
	split_goal_wp
		simplelist_split.1.1						---	0.91	---	---	---	---	---
		simplelist_split.1.2						---	0.92	---	---	---	---	---
		simplelist_split.1.3						---	2.32	---	---	---	---	---
		simplelist_split.1.4						---	2.06	---	---	---	---	---
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	---	---	---	---	---	---
union_sym								0.01	---	---	---	---	---	---
union_var1								0.01	---	---	---	---	---	---
union_var2								0.01	---	---	---	---	---	---
simplelist_app_inter								---	---	---	---	---	---	---
induction_ty_lex
	simplelist_app_inter.1							---	---	---	---	---	---	---
	split_goal_wp
		simplelist_app_inter.1.1						---	---	---	0.19	---	---	---
		simplelist_app_inter.1.2						---	1.62	---	---	---	---	---
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							---	---	---	---	6.14	---	---
elt_set_of								---	---	---	0.48	---	---	---
subset_set_of								0.04	---	---	---	---	---	---
reachable_refl								Timeout (45s) (obsolete)	Timeout (45s) (obsolete)	---	0.03	---	Timeout (45s) (obsolete)	---
reachable_trans								---	0.18	---	---	---	---	---
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.72	---	---	---	---	---
subscc_after_last_gray								---	---	---	---	---	---	---
split_goal_wp
	subscc_after_last_gray.1							---	1.33	---	---	---	---	---
	subscc_after_last_gray.2							0.04	---	---	---	---	---	---
	subscc_after_last_gray.3							Timeout (15s)	28.82	---	Timeout (15s)	---	---	---
	subscc_after_last_gray.4							Timeout (15s)	14.29	---	Timeout (15s)	---	---	---
	subscc_after_last_gray.5							---	---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.5.1						---	---	---	5.51	---	---	---
wf_color_postcond_split								---	0.78	---	---	---	---	---
wf_color_sccs								---	0.74	---	---	---	---	---
wf_color_3_cases								---	0.30	---	---	---	---	---
subenv_num								Timeout (45s)	0.62	---	---	---	---	---
num_lmem								Timeout (45s) (obsolete)	5.73	---	---	---	---	---
num_inj								Timeout (45s) (obsolete)	0.26	---	---	---	---	---
num_rank								Timeout (45s) (obsolete)	0.44	---	---	---	---	---
50. VC for split								---	---	---	---	---	---	---
split_goal_wp
	1. postcondition							0.01	---	---	---	---	---	---
	2. postcondition							0.01	---	---	---	---	---	---
	3. postcondition							0.01	---	---	---	---	---	---
	4. postcondition							---	0.29	---	---	---	---	---
	5. postcondition							0.01	---	---	---	---	---	---
	6. postcondition							0.05	---	---	---	---	---	---
51. VC for add_stack_incr								0.01	---	---	---	---	---	---
52. VC for add_blacks								0.01	---	---	---	---	---	---
53. VC for set_infty								0.03	---	---	---	---	---	---
54. VC for dfs1								---	---	---	---	---	---	---
split_goal_wp
	1. precondition							0.03	---	---	---	---	---	---
	2. precondition							---	---	---	---	---	---	---
	inline_goal
		1. precondition						---	---	---	1.73	---	---	---
	3. precondition							---	---	---	---	---	---	---
	introduce_premises
		1. precondition						---	---	---	---	---	---	---
		inline_goal
			1. precondition					---	---	---	---	---	---	---
			split_goal_wp
				1. precondition				0.32	---	---	---	---	---	---
				2. precondition				---	---	---	---	---	---	---
				introduce_premises
					1. precondition			---	---	---	---	---	---	---
					inline_goal
						1. precondition		---	---	---	---	---	---	---
						split_goal_wp
							1. precondition	---	1.03	---	---	---	---	---
							2. precondition	0.10	---	---	---	---	---	---
							3. precondition	0.62	---	---	---	---	---	---
							4. precondition	0.13	---	---	---	---	---	---
							5. precondition	0.36	---	---	---	---	---	---
							6. precondition	0.21	---	---	---	---	---	---
							7. precondition	---	1.24	---	---	---	---	---
							8. precondition	---	1.37	---	---	---	---	---
							9. precondition	---	0.62	---	---	---	---	---
				3. precondition				0.16	---	---	---	---	---	---
				4. precondition				0.23	---	---	---	---	---	---
				5. precondition				Timeout (45s) (obsolete)	33.16	---	Timeout (45s) (obsolete)	---	---	---
				6. precondition				---	22.18	High Failure (obsolete)	---	---	---	---
				7. precondition				0.03	---	---	---	---	---	---
				8. precondition				0.03	---	---	---	---	---	---
				9. precondition				0.03	---	---	---	---	---	---
	4. assertion							---	---	1.54 (obsolete)	---	---	---	---
	5. postcondition							---	---	---	---	---	---	---
	introduce_premises
		1. postcondition						---	---	---	---	---	---	---
		inline_goal
			1. postcondition					---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1				---	7.47	---	---	---	---	---
				2. VC for dfs1				---	24.35	---	---	---	---	---
				3. VC for dfs1				1.66	---	---	---	---	---	---
				4. VC for dfs1				0.07	---	---	---	---	---	---
				5. VC for dfs1				0.41	---	---	---	---	---	---
				6. VC for dfs1				---	7.05	---	---	---	---	---
				7. VC for dfs1				---	1.70	---	---	---	---	---
				8. VC for dfs1				---	0.33	---	---	---	---	---
				9. VC for dfs1				---	---	---	---	---	---	---
				split_all_full
					1. VC for dfs1			---	20.90	---	---	---	---	---
				10. VC for dfs1				---	---	1.49	---	---	---	---
				11. VC for dfs1				0.25	---	---	---	---	---	---
				12. VC for dfs1				0.05	---	---	---	---	---	---
				13. VC for dfs1				0.27	---	---	---	---	---	---
				14. VC for dfs1				0.95	---	---	---	---	---	---
	6. postcondition							0.01	---	---	---	---	---	---
	7. postcondition							0.14	---	---	---	---	---	---
	8. postcondition							---	1.84	---	---	---	---	---
	9. postcondition							---	---	---	---	---	---	---
	inline_goal
		1. postcondition						5.58	---	---	---	---	---	---
	10. assertion							---	---	---	---	---	---	---
	split_goal_wp
	1. VC for dfs1						0.16	---	---	---	---	---	---
	2. VC for dfs1						0.22	---	---	---	---	---	---
	3. VC for dfs1						10.32	---	---	---	---	---	---
11. assertion							---	---	---	---	---	---	---
introduce_premises
	1. assertion						---	---	---	---	---	---	---
	inline_goal
		1. assertion					---	0.50	---	---	---	---	---
12. assertion							---	---	1.69 (obsolete)	---	---	---	---
13. assertion							---	---	---	---	---	---	---
inline_goal
	1. assertion						---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1					---	2.68	---	---	---	---	---
		2. VC for dfs1					0.17	---	---	---	---	---	---
		3. VC for dfs1					---	---	---	14.39	---	---	---
14. assertion							---	---	---	---	---	---	---
split_goal_wp
	1. VC for dfs1						---	---	---	---	---	---	---
	inline_goal
		1. VC for dfs1					---	---	---	---	---	---	---
		split_goal_wp
			1. VC for dfs1				1.86	---	---	---	---	---	---
			2. VC for dfs1				0.04	---	---	---	---	---	---
	2. VC for dfs1						0.02	---	---	---	---	---	---
15. postcondition							---	---	---	---	---	---	---
inline_goal
	1. postcondition						---	---	---	---	---	---	---
	split_goal_wp
		1. postcondition					---	---	---	---	---	---	---
		introduce_premises
			1. VC for dfs1				---	---	---	---	---	---	---
			inline_goal
				1. VC for dfs1			---	---	---	---	---	---	---
				split_goal_wp
					1. VC for dfs1		1.74	---	---	---	---	---	---
					2. VC for dfs1		---	---	---	25.94	---	---	---
					3. VC for dfs1		28.94	4.10	---	---	---	---	---
					4. VC for dfs1		11.42	---	---	---	---	---	---
		2. postcondition					---	---	---	---	---	---	---
		introduce_premises
			1. VC for dfs1				---	---	---	---	---	---	---
			inline_goal
				1. VC for dfs1			---	---	---	---	---	---	---
				split_goal_wp
					1. VC for dfs1		7.63	---	---	---	---	---	---
					2. VC for dfs1		1.74	---	---	---	---	---	---
					3. VC for dfs1		1.71	---	---	---	---	---	---
					4. VC for dfs1		1.92	---	---	---	---	---	---
					5. VC for dfs1		---	15.74	---	---	---	---	---
					6. VC for dfs1		1.76	---	---	---	---	---	---
					7. VC for dfs1		---	---	---	---	---	---	---
					split_all_full
						1. VC for dfs1	4.62	---	---	---	---	---	---
					8. VC for dfs1		---	---	---	---	---	---	---
					split_all_full
						1. VC for dfs1	5.72	---	---	---	---	---	---
					9. VC for dfs1		---	---	---	---	---	---	---
					split_all_full
						1. VC for dfs1	4.60	---	---	---	---	---	---
		3. postcondition					8.95	---	---	---	---	---	---
		4. postcondition					0.03	---	---	---	---	---	---
		5. postcondition					---	20.56	---	---	---	---	---
		6. postcondition					---	---	---	---	---	---	---
		split_all_full
			1. postcondition				---	---	---	---	---	---	---
			introduce_premises
				1. VC for dfs1			Timeout (45s) (obsolete)	---	---	Timeout (45s) (obsolete)	---	---	---
				inline_goal
					1. VC for dfs1		Timeout (45s)	59.69	---	Timeout (45s)	Timeout (45s)	---	Timeout (45s)
		7. postcondition					2.15	6.69	---	---	---	---	---
		8. postcondition					0.55	---	---	---	---	---	---
		9. postcondition					---	---	---	---	---	---	---
		split_all_full
			1. postcondition				---	---	---	---	---	---	---
			introduce_premises
				1. VC for dfs1			---	---	---	23.50	---	---	---
		10. postcondition					---	---	---	0.26	---	---	---
		11. postcondition					0.10	1.13	---	Timeout (45s) (obsolete)	---	---	---
		12. postcondition					0.10	1.13	---	Timeout (45s) (obsolete)	---	---	---
		13. postcondition					---	23.17	---	---	---	---	---
		14. postcondition					0.04	---	---	---	---	---	---
16. postcondition							0.02	---	---	---	---	---	---
17. postcondition							0.33	---	---	---	---	---	---
18. postcondition							---	---	---	---	---	---	---
inline_goal
	1. postcondition						0.01	---	---	---	---	---	---
19. postcondition							1.63	---	---	---	---	---	---
55. VC for dfs								---	---	---	---	---	---	---
split_goal_wp
	1. postcondition							---	---	---	---	---	---	---
	introduce_premises
		1. postcondition						---	---	---	---	---	---	---
		inline_goal
			1. postcondition					---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs				0.02	---	---	---	---	---	---
				2. VC for dfs				0.02	---	---	---	---	---	---
				3. VC for dfs				0.02	---	---	---	---	---	---
				4. VC for dfs				0.02	---	---	---	---	---	---
				5. VC for dfs				0.05	---	---	---	---	---	---
				6. VC for dfs				0.25	---	---	---	---	---	---
				7. VC for dfs				0.02	---	---	---	---	---	---
				8. VC for dfs				0.02	---	---	---	---	---	---
				9. VC for dfs				0.03	---	---	---	---	---	---
				10. VC for dfs				---	0.31	---	---	---	---	---
				11. VC for dfs				0.02	---	---	---	---	---	---
				12. VC for dfs				0.02	---	---	---	---	---	---
				13. VC for dfs				0.01	---	---	---	---	---	---
				14. VC for dfs				0.02	---	---	---	---	---	---
	2. postcondition							0.02	---	---	---	---	---	---
	3. postcondition							0.02	---	---	---	---	---	---
	4. postcondition							0.02	---	---	---	---	---	---
	5. postcondition							0.55	---	---	---	---	---	---
	6. assertion							---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs						0.04	---	---	---	---	---	---
		2. VC for dfs						---	---	---	---	---	---	0.09
	7. precondition							0.02	---	---	---	---	---	---
	8. precondition							0.02	---	---	---	---	---	---
	9. precondition							0.02	---	---	---	---	---	---
	10. postcondition							---	---	---	---	---	---	---
	introduce_premises
		1. VC for dfs						---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs					---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs				0.03	---	---	---	---	---	---
				2. VC for dfs				0.03	---	---	---	---	---	---
				3. VC for dfs				0.03	---	---	---	---	---	---
				4. VC for dfs				0.03	---	---	---	---	---	---
				5. VC for dfs				0.14	---	---	---	---	---	---
				6. VC for dfs				0.63	---	---	---	---	---	---
				7. VC for dfs				0.06	---	---	---	---	---	---
				8. VC for dfs				0.06	---	---	---	---	---	---
				9. VC for dfs				0.06	---	---	---	---	---	---
				10. VC for dfs				---	---	---	---	---	---	0.05
				11. VC for dfs				0.04	---	---	---	---	---	---
				12. VC for dfs				0.04	---	---	---	---	---	---
				13. VC for dfs				0.04	---	---	---	---	---	---
				14. VC for dfs				0.04	---	---	---	---	---	---
	11. postcondition							0.63	---	---	---	---	---	---
	12. postcondition							---	0.50	---	---	---	---	---
	13. postcondition							---	---	---	---	---	---	---
	introduce_premises
		1. VC for dfs						---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs					1.81	---	---	---	---	---	---
	14. postcondition							0.02	---	---	---	---	---	---
	15. precondition							0.02	---	---	---	---	---	---
	16. precondition							0.02	---	---	---	---	---	---
	17. precondition							0.03	---	---	---	---	---	---
	18. precondition							0.02	---	---	---	---	---	---
	19. precondition							0.02	---	---	---	---	---	---
20. precondition							0.04	---	---	---	---	---	---
21. precondition							0.02	---	---	---	---	---	---
22. postcondition							---	---	---	---	---	---	---
split_goal_wp
	1. postcondition						0.02	---	---	---	---	---	---
	2. postcondition						---	---	---	---	---	---	---
	introduce_premises
		1. VC for dfs					---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs				---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs			---	---	---	---	---	---	---
				inline_goal
					1. VC for dfs		---	---	---	---	---	---	---
					inline_all
						1. VC for dfs	---	---	---	---	---	---	0.41
				2. VC for dfs			0.04	---	---	---	---	---	---
				3. VC for dfs			0.04	---	---	---	---	---	---
				4. VC for dfs			0.21	---	---	---	---	---	---
				5. VC for dfs			0.04	---	---	---	---	---	---
23. postcondition							0.10	---	---	---	---	---	---
24. postcondition							---	0.57	---	---	---	---	---
25. postcondition							0.95	---	---	---	---	---	---
26. postcondition							---	4.54	---	---	---	---	---
56. 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	---	---	---	---	---	---
			7. precondition					0.02	---	---	---	---	---	---
			8. precondition					0.02	---	---	---	---	---	---
			9. precondition					0.02	---	---	---	---	---	---
	4. assertion							0.15	---	---	---	---	---	---
	5. postcondition							---	---	---	---	---	---	---
	split_goal_wp
		1. postcondition						0.52	---	---	---	---	---	---
		2. postcondition						0.02	---	---	---	---	---	---
		3. postcondition						0.15	---	---	---	---	---	---