Why3 Proof Results for Project "uf"

Theory "uf.Top": fully verified

Obligations			Alt-Ergo 2.3.0	CVC4 1.7	Z3 4.4.1	Z3 4.8.6
VC for uf			---	0.06	---	---
VC for create			---	---	---	---
split_vc
	array creation size		0.00	---	---	---
	loop invariant init		0.00	---	---	---
	index in array bounds		0.00	---	---	---
	loop invariant preservation		0.01	---	---	---
	array creation size		0.00	---	---	---
	array creation size		0.00	---	---	---
	precondition		0.00	---	---	---
	precondition		0.01	---	---	---
	precondition		0.00	---	---	---
	precondition		0.01	---	---	---
	precondition		0.00	---	---	---
	precondition		0.00	---	---	---
	precondition		0.00	---	---	---
	precondition		0.01	---	---	---
	out of loop bounds		0.00	---	---	---
VC for find			---	---	---	---
split_vc
	index in array bounds		0.01	---	---	---
	postcondition		0.01	---	---	---
	postcondition		0.01	---	---	---
	variant decrease		0.01	---	---	---
	precondition		0.01	---	---	---
	index in array bounds		0.01	---	---	---
	type invariant		0.02	---	---	---
	type invariant		0.33	---	---	---
	type invariant		0.01	---	---	---
	type invariant		0.01	---	---	---
	type invariant		0.12	---	---	---
	type invariant		0.44	---	---	---
	type invariant		0.01	---	---	---
	type invariant		0.01	---	---	---
	postcondition		0.03	---	---	---
	postcondition		0.03	---	---	---
VC for same			---	0.09	---	---
VC for inc_dst			---	---	---	---
split_vc
	postcondition		---	0.04	---	---
	postcondition		---	0.04	---	---
VC for union			---	---	---	---
split_vc
	precondition		0.01	---	---	---
	precondition		0.01	---	---	---
	postcondition		0.01	---	---	---
	postcondition		0.01	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	type invariant		0.03	---	---	---
	type invariant		---	---	---	---
	split_vc
		type invariant	9.53	---	---	---
		type invariant	9.32	---	---	---
	type invariant		0.70	---	---	---
	type invariant		0.28	---	---	---
	type invariant		---	---	---	0.10
	type invariant		---	---	0.05	---
	type invariant		0.03	---	---	---
	type invariant		---	---	---	0.05
	postcondition		0.01	---	---	---
	postcondition		0.09	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.02	---	---	---
	index in array bounds		0.03	---	---	---
	type invariant		0.04	---	---	---
	type invariant		---	---	---	---
	split_vc
		type invariant	9.36	---	---	---
		type invariant	5.73	---	---	---
	type invariant		0.72	---	---	---
	type invariant		0.31	---	---	---
	type invariant		---	---	---	0.22
	type invariant		---	---	0.04	---
	type invariant		0.03	---	---	---
	type invariant		---	---	---	0.05
	postcondition		0.01	---	---	---
	postcondition		0.10	---	---	---
	type invariant		0.04	---	---	---
	type invariant		---	---	---	---
	split_vc
		type invariant	5.06	---	---	---
		type invariant	5.56	---	---	---
	type invariant		0.71	---	---	---
	type invariant		0.29	---	---	---
	type invariant		---	---	---	---
	split_vc
		type invariant	1.84	---	---	---
		type invariant	0.98	---	---	---
	type invariant		---	---	---	0.14
	type invariant		0.03	---	---	---
	type invariant		---	---	---	---
	split_vc
		type invariant	5.33	---	---	---
	postcondition		0.01	---	---	---
	postcondition		0.08	---	---	---
VC for path_rep			0.03	---	---	---