Why3 Proof Results for Project "scc"

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

Obligations										Alt-Ergo (2.2.0)	Alt-Ergo (2.3.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	---	---	---	---	---	---	---
inter_com										---	---	0.05	---	---	---	---	---
inter_add_l										0.01	---	---	---	---	---	---	---
inter_not_add_l										0.01	---	---	---	---	---	---	---
diff_add_l										0.01	---	---	---	---	---	---	---
diff_add_r										0.02	---	---	---	---	---	---	---
subset_add_r										0.01	---	---	---	---	---	---	---
union_add_l										0.01	---	---	---	---	---	---	---
union_add_r										0.01	---	---	---	---	---	---	---
union_com										0.01	---	---	---	---	---	---	---
union_var_l										0.01	---	---	---	---	---	---	---
union_var_r										0.01	---	---	---	---	---	---	---
set_of_elt										---	---	---	---	---	---	---	---
split_goal_wp
	set_of_elt.1									0.02	---	---	---	---	---	---	---
	set_of_elt.2									---	---	---	---	---	2.50	---	---
elt_set_of										---	---	---	---	0.22	---	---	---
subset_set_of										0.04	---	---	---	---	---	---	---
elts_cons										0.03	---	---	---	---	---	---	---
elts_app										0.02	---	---	---	---	---	---	---
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.22	---	---	---	---	---
snoc_app										0.02	---	---	---	---	---	---	---
precedes_mem										0.05	---	---	---	---	---	---	---
head_precedes										---	---	0.10	---	---	---	---	---
precedes_tail										---	---	1.50	---	---	---	---	---
tail_not_precedes										0.02	---	---	---	---	---	---	---
split_list_precedes										---	---	7.88	---	---	---	---	---
precedes_refl										0.02	---	---	---	---	---	---	---
precedes_append_left										0.05	---	---	---	---	---	---	---
precedes_append_left_iff										---	---	---	---	---	---	---	---
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										0.80	---	---	---	---	---	---	---
precedes_append_right_iff										---	---	---	---	---	---	---	---
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.12	---	---	---	---	---
simplelist_split										---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_split.1									---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_split.1.1								---	---	0.59	---	---	---	---	---
		simplelist_split.1.2								---	---	0.62	---	---	---	---	---
		simplelist_split.1.3								---	---	0.91	---	---	---	---	---
		simplelist_split.1.4								---	---	0.73	---	---	---	---	---
simplelist_app_disjoint										---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_app_disjoint.1									---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_app_disjoint.1.1								---	---	---	---	0.09	---	---	---
		simplelist_app_disjoint.1.2								---	---	0.69	---	---	---	---	---
simplelist_length										---	---	---	---	---	---	---	---
induction_ty_lex
	simplelist_length.1									---	---	---	---	---	---	---	---
	split_goal_wp
		simplelist_length.1.1								0.01	---	---	---	---	---	---	---
		simplelist_length.1.2								0.01	---	---	---	---	---	---	---
precedes_antisym										0.34	---	---	---	---	---	---	---
precedes_trans										---	---	---	---	---	---	---	---
induction_ty_lex
	precedes_trans.1									---	---	---	---	---	---	---	---
	split_goal_wp
		precedes_trans.1.1								---	---	3.59	---	---	---	---	---
reachable_refl										---	---	---	---	0.03	---	---	---
reachable_trans										---	---	0.18	---	---	---	---	---
xpath_xedge										---	---	---	---	---	---	---	---
induction_pr
	xpath_xedge.1									0.01	---	---	---	---	---	---	---
	xpath_xedge.2									---	---	---	---	0.06	---	---	---
same_scc_refl										---	---	---	---	0.07	---	---	---
same_scc_sym										0.01	---	---	---	---	---	---	---
same_scc_trans										0.02	---	---	---	---	---	---	---
subscc_add										0.04	---	---	---	---	---	---	---
scc_max										---	---	0.32	---	---	---	---	---
subscc_after_last_gray										---	---	---	---	---	---	---	---
split_goal_wp
	subscc_after_last_gray.1									---	---	0.50	---	---	---	---	---
	subscc_after_last_gray.2									0.04	---	---	---	---	---	---	---
	subscc_after_last_gray.3									Timeout (45s) (obsolete)	---	19.29	---	---	---	---	---
	subscc_after_last_gray.4									Timeout (45s) (obsolete)	---	0.42	---	Timeout (45s) (obsolete)	---	Timeout (45s) (obsolete)	---
	subscc_after_last_gray.5									Timeout (45s) (obsolete)	---	2.42	---	Timeout (45s) (obsolete)	---	Timeout (45s) (obsolete)	---
	subscc_after_last_gray.6									---	---	---	---	---	---	---	---
	inline_goal
		subscc_after_last_gray.6.1								---	---	---	---	0.22	---	---	---
wf_color_postcond_split										---	---	0.36	---	---	---	---	---
wf_color_sccs										---	---	0.32	---	---	---	---	---
wf_color_3_cases										---	---	0.30	---	---	---	---	---
num_lmem										Timeout (45s) (obsolete)	---	2.88	---	---	---	---	---
num_rank_strict										---	---	---	---	---	---	---	---
split_goal_wp
	num_rank_strict.1									---	---	0.32	---	---	---	---	---
	num_rank_strict.2									0.03	---	---	---	---	---	---	---
	num_rank_strict.3									---	---	0.30	---	---	---	---	---
simplelist_x_prec_strict_y'										---	0.54	---	---	---	---	---	---
51. VC for split										---	---	---	---	---	---	---	---
split_goal_wp
	1. postcondition									---	0.01	---	---	---	---	---	---
	2. postcondition									---	0.01	---	---	---	---	---	---
	3. postcondition									---	0.01	---	---	---	---	---	---
	4. postcondition									---	---	0.29	---	---	---	---	---
	5. variant decrease									---	0.02	---	---	---	---	---	---
	6. postcondition									---	0.01	---	---	---	---	---	---
	7. postcondition									---	0.05	---	---	---	---	---	---
52. VC for add_stack_incr										---	0.01	---	---	---	---	---	---
53. VC for add_black										---	0.02	---	---	---	---	---	---
54. VC for set_infty										---	0.03	---	---	---	---	---	---
55. VC for dfs1										---	---	---	---	---	---	---	---
split_goal_wp
	1. variant decrease									---	0.07	---	---	---	---	---	---
	2. precondition									---	0.02	---	---	---	---	---	---
	3. precondition									---	---	---	---	---	---	---	---
	inline_goal
		1. precondition								---	---	---	---	1.69	---	---	---
	4. precondition									---	---	---	---	---	---	---	---
	introduce_premises
		1. precondition								---	---	---	---	---	---	---	---
		inline_goal
			1. precondition							---	---	---	---	---	---	---	---
			split_goal_wp
				1. precondition						---	1.08	---	---	---	---	---	---
				2. precondition						---	---	---	---	---	---	---	---
				introduce_premises
					1. precondition					---	---	---	---	---	---	---	---
					inline_goal
						1. precondition				---	---	---	---	---	---	---	---
						split_goal_wp
							1. precondition			Timeout (45s) (obsolete)	---	1.17	---	---	---	---	---
							2. precondition			---	0.06	---	---	---	---	---	---
							3. precondition			---	0.81	---	---	---	---	---	---
							4. precondition			---	0.22	---	---	---	---	---	---
							5. precondition			---	0.46	---	---	---	---	---	---
							6. precondition			---	0.27	---	---	---	---	---	---
							7. precondition			Timeout (45s) (obsolete)	---	1.20	---	---	---	---	---
							8. precondition			---	---	1.40	---	---	---	---	---
				3. precondition						---	0.06	---	---	---	---	---	---
				4. precondition						---	0.34	---	---	---	---	---	---
				5. precondition						---	---	16.17	---	---	---	---	---
				6. precondition						---	---	12.02	---	---	---	---	---
				7. precondition						---	0.03	---	---	---	---	---	---
				8. precondition						---	0.03	---	---	---	---	---	---
				9. precondition						---	0.03	---	---	---	---	---	---
	5. assertion									---	---	0.41	---	---	---	---	---
	6. assertion									---	---	13.38	---	---	---	---	---
	7. postcondition									---	---	---	---	---	---	---	---
	introduce_premises
		1. postcondition								---	---	---	---	---	---	---	---
		inline_goal
			1. postcondition							---	---	---	---	---	---	---	---
			split_goal_wp
				1. VC for dfs1						---	---	---	---	---	---	---	---
				introduce_premises
					1. VC for dfs1					---	---	---	---	---	---	---	---
					inline_goal
						1. VC for dfs1				---	---	---	---	---	---	---	---
						split_goal_wp
							1. VC for dfs1			---	1.08	---	---	---	---	---	---
							2. VC for dfs1			---	---	1.13	---	---	---	---	---
							3. VC for dfs1			---	3.92	---	---	---	---	---	---
							4. VC for dfs1			---	---	1.74	---	---	---	---	---
				2. VC for dfs1						---	---	29.09	---	---	---	---	---
				3. VC for dfs1						---	1.41	---	---	---	---	---	---
				4. VC for dfs1						---	0.07	---	---	---	---	---	---
				5. VC for dfs1						---	0.50	---	---	---	---	---	---
				6. VC for dfs1						---	---	5.92	---	---	---	---	---
				7. VC for dfs1						---	2.88	1.85	---	---	---	---	---
				8. VC for dfs1						---	0.31	0.33	---	---	---	---	---
				9. VC for dfs1						---	---	---	---	---	---	---	10.23
				10. VC for dfs1						---	---	---	1.19	---	---	---	---
				11. VC for dfs1						---	0.31	0.59	---	---	---	---	---
				12. VC for dfs1						---	0.03	0.28	---	---	---	---	---
				13. VC for dfs1						---	0.19	0.67	---	---	---	---	---
				14. VC for dfs1						---	1.22	0.81	---	---	---	---	---
8. postcondition									---	---	0.24	---	---	---	---	---
9. postcondition									---	---	0.63	---	---	---	---	---
10. postcondition									---	---	1.77	---	---	---	---	---
11. postcondition									---	---	---	---	---	---	---	---
inline_goal
	1. postcondition								---	4.85	---	---	---	---	---	---
12. assertion									---	---	---	---	---	---	---	---
split_goal_wp
	1. VC for dfs1								---	0.19	---	---	---	---	---	---
	2. VC for dfs1								---	0.23	---	---	---	---	---	---
	3. VC for dfs1								---	7.96	---	---	---	---	---	---
13. assertion									---	---	---	---	---	---	---	---
introduce_premises
	1. assertion								---	---	---	---	---	---	---	---
	inline_goal
		1. assertion							---	---	0.51	---	---	---	---	---
14. assertion									---	---	---	2.22	---	---	---	---
15. assertion									---	---	---	---	---	---	---	---
inline_goal
	1. assertion								---	---	---	---	---	---	---	---
	split_goal_wp
		1. VC for dfs1							---	---	2.80	---	---	---	---	---
		2. VC for dfs1							---	0.17	---	---	---	---	---	---
		3. VC for dfs1							---	---	---	---	7.88	---	---	---
16. assertion									---	---	---	---	---	---	---	---
split_goal_wp
	1. assertion								---	---	---	---	---	---	---	0.49
17. 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.93	---	---	---	---	---	---
					2. VC for dfs1				---	---	---	---	---	---	---	2.18
					3. VC for dfs1				---	---	---	---	---	---	---	---
					introduce_premises
						1. VC for dfs1			---	---	---	---	---	---	---	---
						inline_goal
							1. VC for dfs1		---	---	---	---	---	---	---	---
							split_goal_wp
								1. VC for dfs1	---	Timeout (45s)	50.25	---	---	---	---	Timeout (45s)
								2. VC for dfs1	---	28.84	---	---	---	---	---	---
					4. VC for dfs1				---	8.28	---	---	---	---	---	---
		2. postcondition							---	---	---	---	---	---	---	---
		introduce_premises
			1. VC for dfs1						---	---	---	---	---	---	---	---
			inline_goal
				1. VC for dfs1					---	---	---	---	---	---	---	---
				split_goal_wp
					1. VC for dfs1				---	13.09	---	---	---	---	---	---
					2. VC for dfs1				---	1.98	---	---	---	---	---	---
					3. VC for dfs1				---	3.49	---	---	---	---	---	---
					4. VC for dfs1				---	2.02	---	---	---	---	---	---
					5. VC for dfs1				---	---	17.01	---	---	---	---	---
					6. VC for dfs1				---	2.14	---	---	---	---	---	---
					7. VC for dfs1				---	---	---	---	---	---	---	---
					split_all_full
						1. VC for dfs1			---	13.12	---	---	---	---	---	---
					8. VC for dfs1				---	---	---	---	---	---	---	---
					split_all_full
						1. VC for dfs1			---	14.46	---	---	---	---	---	---
		3. postcondition							---	14.70	---	---	---	---	---	---
		4. postcondition							---	0.03	---	---	---	---	---	---
		5. postcondition							---	Timeout (45s)	43.41	---	---	---	---	Timeout (45s)
		6. postcondition							---	---	---	---	---	---	---	---
		split_all_full
			1. postcondition						---	---	---	---	---	---	---	---
			introduce_premises
				1. VC for dfs1					---	---	---	---	---	---	---	---
				inline_goal
					1. VC for dfs1				---	---	65.07	---	---	---	---	---
		7. postcondition							---	2.94	10.06	---	---	---	---	---
		8. postcondition							---	0.75	---	---	---	---	---	---
		9. postcondition							---	---	---	---	---	---	---	---
		split_all_full
			1. postcondition						---	---	---	---	---	---	---	---
			introduce_premises
				1. VC for dfs1					---	---	---	---	22.41	---	---	---
		10. postcondition							---	---	---	---	0.31	---	---	---
		11. postcondition							---	0.10	1.11	---	---	---	---	---
		12. postcondition							---	0.10	1.13	---	---	---	---	---
		13. postcondition							---	---	---	---	---	---	---	3.65
		14. postcondition							---	0.04	---	---	---	---	---	---
18. postcondition									---	0.02	---	---	---	---	---	---
19. postcondition									---	0.48	---	---	---	---	---	---
20. postcondition									---	---	---	---	---	---	---	---
inline_goal
	1. postcondition								---	0.01	---	---	---	---	---	---
21. postcondition									---	1.65	---	---	---	---	---	---
56. 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.35	---	---	---	---	---	---
				7. VC for dfs						---	0.02	---	---	---	---	---	---
				8. VC for dfs						---	0.02	---	---	---	---	---	---
				9. VC for dfs						---	0.03	---	---	---	---	---	---
				10. VC for dfs						---	---	0.24	---	---	---	---	---
				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.64	---	---	---	---	---	---
	6. variant decrease									---	---	0.27	---	---	---	---	---
	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.17	---	---	---	---	---	---
				6. VC for dfs						---	0.96	---	---	---	---	---	---
				7. VC for dfs						---	0.05	---	---	---	---	---	---
				8. VC for dfs						---	0.06	---	---	---	---	---	---
				9. VC for dfs						---	0.06	---	---	---	---	---	---
				10. VC for dfs						---	---	---	---	---	---	---	0.04
				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									---	2.31	---	---	---	---	---	---
	12. postcondition									---	---	1.74	---	---	---	---	---
	13. postcondition									---	---	---	---	---	---	---	---
	introduce_premises
		1. VC for dfs								---	---	---	---	---	---	---	---
		inline_goal
			1. VC for dfs							---	2.75	---	---	---	---	---	---
	14. postcondition									---	0.02	---	---	---	---	---	---
	15. variant decrease									---	---	0.06	---	---	---	---	---
	16. precondition									---	0.02	---	---	---	---	---	---
	17. precondition									---	0.02	---	---	---	---	---	---
	18. precondition									---	0.15	---	---	---	---	---	---
	19. precondition									---	0.02	---	---	---	---	---	---
	20. variant decrease									---	---	24.74 (obsolete)	---	---	---	---	---
	inline_all
		1. variant decrease								---	---	---	---	---	---	---	---
split_all_full
		1. variant decrease							---	0.24	---	---	---	---	---	---
		2. variant decrease							---	0.09	---	---	---	---	---	---
		3. variant decrease							---	0.09	---	---	---	---	---	---
		4. variant decrease							---	0.23	---	---	---	---	---	---
		5. variant decrease							---	0.24	---	---	---	---	---	---
		6. variant decrease							Timeout (25s) (obsolete)	---	---	---	---	---	---	0.56
		7. variant decrease							---	0.08	---	---	---	---	---	---
		8. variant decrease							---	0.08	---	---	---	---	---	---
		9. variant decrease							---	0.26	---	---	---	---	---	---
		10. variant decrease							---	0.76	---	---	---	---	---	---
21. precondition									---	0.02	---	---	---	---	---	---
22. precondition									---	0.04	---	---	---	---	---	---
23. precondition									---	0.02	---	---	---	---	---	---
24. 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.43
				2. VC for dfs					---	0.04	---	---	---	---	---	---
				3. VC for dfs					---	0.04	---	---	---	---	---	---
				4. VC for dfs					---	0.21	---	---	---	---	---	---
				5. VC for dfs					---	0.04	---	---	---	---	---	---
25. postcondition									---	0.10	---	---	---	---	---	---
26. postcondition									---	---	3.72	---	---	---	---	---
27. postcondition									---	1.13	---	---	---	---	---	---
28. postcondition									---	---	6.49	---	---	---	---	---
57. 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								---	1.66	---	---	---	---	---	---
		2. postcondition								---	0.02	---	---	---	---	---	---
		3. postcondition								---	0.15	---	---	---	---	---	---