Why3 Proof Results for Project "scc"

Theory "scc.Kosaraju": fully verified in 27.26 s

Obligations			Alt-Ergo (2.1.0)	CVC3 (2.4.1)	CVC4 (1.5)	Eprover (1.9)	Spass (3.5)	Z3 (4.6.2)
reachable_trans			Timeout (15s)	0.05	0.04	0.10	9.87	Timeout (15s)
access_from_extension			Timeout (45s)	---	43.46	Timeout (45s)	---	---
introduce_premises
	access_from_extension.1		---	---	---	---	---	---
	inline_goal
		access_from_extension.1.1	Timeout (15s)	---	13.38	0.02	0.03	Timeout (15s)
access_var			0.01	---	0.05	3.81	0.04	0.02
access_covar			0.01	---	0.04	3.52	0.04	0.02
access_trans			0.01	---	0.13	Timeout (15s)	Timeout (15s)	0.02
access_from_successors			Timeout (15s)	0.73	8.75	Timeout (15s)	Timeout (15s)	Timeout (15s)

Theory "scc.SCCK": fully verified in 42.31 s

Obligations									Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)	Spass (3.5)	Z3 (4.6.2)
rank_range									---	---	---	---	---
induction_ty_lex
	rank_range.1								0.03	0.07	0.09	Timeout (15s)	Timeout (15s)
simplelist_sub									Timeout (15s)	0.12	2.74	Timeout (15s)	Timeout (15s)
inter_assoc									0.02	0.06	Timeout (15s)	Timeout (15s)	9.71
inter_add									0.06	0.08	Timeout (15s)	Timeout (15s)	Timeout (15s)
inter_elt									0.03	14.15	0.04	Timeout (15s)	Timeout (15s)
set_elt									0.02	0.14	Timeout (15s)	Timeout (15s)	Timeout (15s)
elements_add									0.08	0.07	0.03	9.08	0.04
simplelist_inter									---	---	---	---	---
induction_ty_lex
	simplelist_inter.1								---	---	---	---	---
	split_goal_wp
		simplelist_inter.1.1							Timeout (15s)	14.24	0.18	Timeout (15s)	Timeout (15s)
		simplelist_inter.1.2							Timeout (15s)	0.50	Timeout (15s)	Timeout (15s)	Timeout (15s)
length_eq_cardinal									---	---	---	---	---
induction_ty_lex
	length_eq_cardinal.1								---	---	---	---	---
	split_goal_wp
		length_eq_cardinal.1.1							0.03	0.07	0.03	0.05	0.03
		length_eq_cardinal.1.2							0.07	0.10	12.44	Timeout (15s)	Timeout (15s)
elements_elt_exchange									0.03	2.55	Timeout (15s)	Timeout (15s)	Timeout (15s)
elements_append_comm									0.06	0.11	Timeout (15s)	Timeout (15s)	5.86
subset_inter_subset									Timeout (15s)	0.09	0.87	Timeout (15s)	0.04
same_scc_refl									Timeout (15s)	14.20	0.08	0.12	Timeout (15s)
same_scc_sym									0.02	0.06	0.04	0.05	0.03
same_scc_trans									0.03	0.06	0.04	0.09	0.03
cc_ext									0.07	6.59	Timeout (15s)	Timeout (15s)	Timeout (15s)
scc_max									Timeout (15s)	0.14	Timeout (15s)	Timeout (15s)	Timeout (15s)
disjoint_scc									---	---	---	---	---
inline_goal
	disjoint_scc.1								---	---	---	---	---
	split_goal_wp
		disjoint_scc.1.1							Timeout (15s)	14.26	4.37	1.37	Timeout (15s)
		disjoint_scc.1.2							Timeout (15s)	14.37	4.37	1.38	Timeout (15s)
wf_stack_white_extension									Timeout (15s)	14.13	0.09	Timeout (15s)	Timeout (15s)
reverse_path									---	---	---	---	---
induction_pr
	reverse_path.1								0.02	14.41	0.05	0.09	Timeout (15s)
	reverse_path.2								0.08	1.27	Timeout (15s)	Timeout (15s)	Timeout (15s)
reverse_pathG2									---	---	---	---	---
induction_pr
	reverse_pathG2.1								0.02	14.17	0.05	0.09	Timeout (15s)
	reverse_pathG2.2								0.07	0.87	5.09	Timeout (15s)	Timeout (15s)
reachable_before_pop									0.31	0.83	Timeout (15s)	Timeout (15s)	Timeout (15s)
reachable_before_push									0.03	0.21	Timeout (15s)	Timeout (15s)	Timeout (15s)
reachable_before_reverse									---	---	---	---	---
split_goal_wp
	reachable_before_reverse.1								0.02	15.32	Timeout (15s)	Timeout (15s)	Timeout (15s)
	reachable_before_reverse.2								---	---	---	---	---
	introduce_premises
		reachable_before_reverse.2.1							---	---	---	---	---
		inline_goal
			reachable_before_reverse.2.1.1						---	---	---	---	---
			inline_goal
				reachable_before_reverse.2.1.1.1					0.35	0.15	Timeout (15s)	Timeout (15s)	Timeout (15s)
no_edge_out_push									Timeout (15s)	0.30	Timeout (15s)	Timeout (15s)	Timeout (15s)
path_cross_sets									---	---	---	---	---
induction_pr
	path_cross_sets.1								Timeout (15s)	0.23	0.57	Timeout (15s)	0.07
	path_cross_sets.2								Timeout (15s)	3.08	0.71	Timeout (15s)	Timeout (15s)
no_edge_out_no_path_out									0.02	1.05	Timeout (15s)	Timeout (15s)	0.05
no_black_to_white_no_path_out_of_blacksG2									---	---	---	---	---
induction_pr
	no_black_to_white_no_path_out_of_blacksG2.1								0.01	0.04	0.02	0.09	0.03
	no_black_to_white_no_path_out_of_blacksG2.2								0.04	0.14	0.07	0.20	Timeout (15s)
no_black_to_white_convex_diffG2									0.04	Timeout (15s)	Timeout (15s)	Timeout (15s)	Timeout (15s)
convex_paths_closed_in_sccG2									---	---	---	---	---
introduce_premises
	convex_paths_closed_in_sccG2.1								---	---	---	---	---
	split_goal_wp
		convex_paths_closed_in_sccG2.1.1							0.02	0.15	0.05	0.28	0.03
		convex_paths_closed_in_sccG2.1.2							Timeout (15s)	0.22	Timeout (15s)	Timeout (15s)	Timeout (15s)
31. VC for dfs1									---	---	---	---	---
split_goal_wp
	1. postcondition								0.02	0.04	0.02	0.08	0.03
	2. postcondition								0.02	0.08	0.05	0.11	0.03
	3. postcondition								Timeout (15s)	0.11	0.07	0.12	Timeout (15s)
	4. postcondition								0.03	0.06	0.02	0.08	0.03
	5. precondition								0.03	0.08	0.06	0.11	0.04
	6. precondition								0.03	0.04	0.02	0.08	0.03
	7. postcondition								0.03	0.04	0.02	0.09	0.02
	8. postcondition								0.04	0.13	Timeout (15s)	Timeout (15s)	0.06
	9. postcondition								0.02	0.10	0.12	5.68	0.04
	10. postcondition								0.03	0.04	0.02	0.09	0.02
	11. precondition								0.04	0.08	0.06	0.11	0.03
	12. precondition								---	---	---	---	---
	inline_goal
		1. precondition							---	---	---	---	---
		split_goal_wp
			1. VC for dfs1						0.06	0.89	Timeout (15s)	Timeout (15s)	Timeout (15s)
			2. VC for dfs1						0.02	0.04	0.02	0.08	0.02
			3. VC for dfs1						0.02	0.04	0.02	0.08	0.02
			4. VC for dfs1						0.02	0.04	0.02	0.08	0.02
			5. VC for dfs1						0.02	0.04	0.02	0.08	0.02
	13. assertion								0.16	0.21	1.69	Timeout (15s)	Timeout (15s)
	14. assertion								---	---	---	---	---
	split_goal_wp
		1. VC for dfs1							0.03	0.19	0.04	0.44	4.71
		2. VC for dfs1							0.06	0.16	0.20	Timeout (15s)	Timeout (15s)
	15. assertion								---	---	---	---	---
	split_goal_wp
		1. VC for dfs1							Timeout (15s)	4.18	Timeout (15s)	Timeout (15s)	Timeout (15s)
		2. VC for dfs1							Timeout (15s)	4.18	Timeout (15s)	Timeout (15s)	Timeout (15s)
	16. precondition								0.04	0.10	0.09	0.13	0.04
	17. precondition								---	---	---	---	---
	introduce_premises
		1. precondition							---	---	---	---	---
		inline_goal
			1. precondition						---	---	---	---	---
			split_goal_wp
				1. VC for dfs1					---	---	---	---	---
				inline_goal
					1. VC for dfs1				---	---	---	---	---
					split_goal_wp
						1. VC for dfs1			0.07	0.30	Timeout (15s)	Timeout (15s)	0.08
						2. VC for dfs1			0.03	0.09	0.05	0.10	0.04
						3. VC for dfs1			0.03	0.11	0.06	0.36	0.05
						4. VC for dfs1			Timeout (15s)	5.34	Timeout (15s)	Timeout (15s)	Timeout (15s)
				2. VC for dfs1					0.09	1.07	Timeout (15s)	Timeout (15s)	0.54
				3. VC for dfs1					0.03	0.12	0.07	0.51	0.07
				4. VC for dfs1					0.07	5.67	Timeout (15s)	Timeout (15s)	0.57
				5. VC for dfs1					---	---	---	---	---
				inline_goal
					1. VC for dfs1				---	---	---	---	---
					introduce_premises
						1. VC for dfs1			---	---	---	---	---
						inline_goal
							1. VC for dfs1		---	---	---	---	---
							split_goal_wp
								1. VC for dfs1	0.04	0.09	0.06	0.28	0.05
								2. VC for dfs1	High Failure	50.06	Timeout (55s)	Timeout (55s)	Timeout (55s)
	18. postcondition								0.03	0.05	0.02	0.09	0.02
	19. postcondition								0.29	0.29	Timeout (15s)	Timeout (15s)	0.13
	20. postcondition								High Failure	51.44	Timeout (55s)	Timeout (55s)	29.80
	21. postcondition								0.06	0.28	8.91	0.28	0.06
32. VC for dfs2									---	---	---	---	---
split_goal_wp
	1. postcondition								0.03	0.04	0.02	0.08	0.03
	2. postcondition								0.10	0.08	0.06	0.10	0.03
	3. postcondition								0.02	0.09	0.07	Timeout (15s)	0.03
	4. postcondition								0.03	0.06	0.02	0.08	0.03
	5. precondition								0.03	0.08	0.06	0.10	0.03
	6. precondition								0.03	0.04	0.02	0.08	0.03
	7. assertion								0.12	0.16	Timeout (15s)	Timeout (15s)	Timeout (15s)
	8. postcondition								0.03	0.04	0.02	0.08	0.03
	9. postcondition								0.05	0.11	Timeout (15s)	Timeout (15s)	0.04
	10. postcondition								0.04	0.09	0.10	0.11	0.04
	11. postcondition								0.03	0.04	0.02	0.08	0.03
	12. precondition								0.04	0.08	0.06	0.10	0.03
	13. precondition								0.03	0.04	0.02	0.08	0.03
	14. precondition								0.03	0.09	0.06	0.11	0.04
	15. precondition								---	---	---	---	---
	inline_goal
		1. precondition							---	---	---	---	---
		split_goal_wp
			1. VC for dfs2						0.01	0.11	Timeout (15s)	Timeout (15s)	0.05
			2. VC for dfs2						0.04	0.04	0.02	0.09	0.02
			3. VC for dfs2						0.02	0.12	0.07	0.75	Timeout (15s)
			4. VC for dfs2						0.06	0.25	Timeout (15s)	Timeout (15s)	Timeout (15s)
	16. assertion								0.04	0.25	Timeout (15s)	Timeout (15s)	Timeout (15s)
	17. postcondition								0.03	0.04	0.02	0.09	0.03
	18. postcondition								0.03	0.15	Timeout (15s)	Timeout (15s)	0.05
	19. postcondition								0.24	14.61	Timeout (15s)	Timeout (15s)	Timeout (15s)
	20. postcondition								0.04	0.15	0.12	0.18	0.05
33. VC for iter2									---	---	---	---	---
split_goal_wp
	1. postcondition								0.03	0.05	0.02	0.09	0.04
	2. postcondition								0.03	0.08	0.07	0.12	0.04
	3. postcondition								0.02	0.10	0.07	0.12	0.04
	4. postcondition								0.01	0.08	0.02	0.09	0.04
	5. precondition								0.07	0.19	Timeout (15s)	Timeout (15s)	0.06
	6. precondition								0.08	0.57	4.48	Timeout (15s)	Timeout (15s)
	7. precondition								0.03	0.08	0.07	0.14	0.04
	8. postcondition								0.02	0.05	0.02	0.10	0.02
	9. postcondition								0.03	0.08	0.07	0.14	0.04
	10. postcondition								0.03	0.15	0.11	Timeout (15s)	0.05
	11. postcondition								0.01	0.05	0.02	0.10	0.02
	12. precondition								---	---	---	---	---
	split_goal_wp
		1. precondition							0.06	0.41	3.88	Timeout (15s)	0.14
	13. precondition								0.02	0.08	0.04	0.13	0.04
	14. assertion								---	---	---	---	---
	split_goal_wp
		1. assertion							0.13	0.49	Timeout (15s)	Timeout (15s)	0.41
		2. assertion							0.05	0.25	Timeout (15s)	Timeout (15s)	0.09
		3. assertion							0.02	0.11	0.07	0.15	0.04
		4. VC for iter2							0.41	14.49	Timeout (15s)	Timeout (15s)	Timeout (15s)
		5. VC for iter2							0.02	0.09	0.04	0.14	0.04
	15. assertion								---	---	---	---	---
	split_goal_wp
		1. VC for iter2							0.12	14.70	4.25	1.99	0.51
		2. VC for iter2							0.04	0.19	0.17	0.17	0.06
	16. assertion								0.03	0.12	Timeout (15s)	0.15	0.05
	17. assertion								---	---	---	---	---
	inline_goal
		1. assertion							---	---	---	---	---
		split_goal_wp
			1. VC for iter2						0.02	0.09	0.04	0.16	0.04
			2. VC for iter2						0.03	0.12	0.08	Timeout (15s)	0.04
			3. VC for iter2						Timeout (15s)	1.30	2.53	Timeout (15s)	Timeout (15s)
	18. precondition								---	---	---	---	---
	inline_goal
		1. precondition							Timeout (15s)	14.35	Timeout (15s)	Timeout (15s)	1.16
	19. precondition								---	---	---	---	---
	introduce_premises
		1. precondition							---	---	---	---	---
		inline_goal
			1. precondition						---	---	---	---	---
			split_goal_wp
				1. VC for iter2					0.01	0.04	0.02	0.08	0.02
				2. VC for iter2					0.02	0.08	0.05	0.10	0.04
				3. VC for iter2					0.08	0.28	0.27	Timeout (15s)	0.11
				4. VC for iter2					0.08	0.17	0.06	0.35	0.09
	20. precondition								---	---	---	---	---
	split_goal_wp
		1. precondition							---	---	---	---	---
		inline_goal
			1. precondition						---	---	---	---	---
			split_goal_wp
				1. precondition					0.01	0.12	0.08	0.18	0.04
				2. precondition					0.08	0.12	0.08	0.18	0.04
				3. precondition					0.07	0.28	0.75	0.17	Timeout (15s)
		2. precondition							0.06	0.22	0.08	0.16	Timeout (15s)
		3. precondition							Timeout (15s)	2.05	2.76	2.72	Timeout (15s)
	21. postcondition								0.03	0.05	0.02	0.10	0.02
	22. postcondition								0.04	0.09	0.07	0.15	0.04
	23. postcondition								0.03	0.19	1.30	Timeout (15s)	0.06
	24. postcondition								0.02	0.09	0.09	0.16	0.04
34. VC for scc_main									---	---	---	---	---
split_goal_wp
	1. precondition								0.01	0.06	0.02	0.07	0.03
	2. precondition								---	---	---	---	---
	introduce_premises
		1. precondition							---	---	---	---	---
		inline_goal
			1. precondition						---	---	---	---	---
			split_goal_wp
				1. VC for scc_main					0.02	0.09	0.14	Timeout (15s)	Timeout (15s)
				2. VC for scc_main					0.01	0.08	0.03	0.09	0.04
				3. VC for scc_main					0.01	0.09	0.06	0.09	0.04
				4. VC for scc_main					0.01	0.09	0.05	0.10	0.04
				5. VC for scc_main					Timeout (15s)	0.17	0.44	Timeout (15s)	0.05
	3. precondition								0.06	0.13	Timeout (15s)	6.29	0.06
	4. precondition								0.07	0.12	0.06	4.39	0.05
	5. precondition								---	---	---	---	---
	split_goal_wp
		1. precondition							0.01	0.08	0.02	0.10	0.04
		2. precondition							0.01	0.08	0.02	0.09	0.04
		3. precondition							0.02	0.14	0.07	0.13	0.05
	6. postcondition								---	---	---	---	---
	split_goal_wp
		1. postcondition							0.02	0.08	0.04	0.12	0.04
		2. postcondition							0.02	0.12	0.08	0.48	0.06
		3. postcondition							0.49	0.74	0.14	1.75	0.06