Why3 Proof Results for Project "pqueue"

Theory "pqueue.Top": fully verified

Obligations				Alt-Ergo 2.3.0	CVC4 1.7
VC for t				---	---
split_vc
	array creation size			0.01	---
	type invariant			---	---
	split_vc
		type invariant		0.00	---
		type invariant		0.01	---
		type invariant		0.00	---
	type invariant			---	0.05
VC for create				0.02	---
VC for first_is_min				0.05	---
VC for move_down				---	---
split_vc
	index in array bounds			---	0.08
	index in array bounds			---	0.08
	index in array bounds			---	---
	unfold heap_order
		index in array bounds		---	---
		split_vc
			index in array bounds	0.05	---
			index in array bounds	0.02	---
	index in array bounds			---	0.05
	index in array bounds			---	0.05
	variant decrease			---	0.04
	precondition			0.60	---
	precondition			---	0.06
	precondition			0.06	---
	postcondition			0.02	---
	index in array bounds			---	0.09
	postcondition			---	---
	unfold heap_order
		VC for move_down		---	---
		split_vc
			VC for move_down	0.21	---
			VC for move_down	0.30	---
	index in array bounds			---	0.07
	postcondition			0.09	---
VC for extract_min_exn				---	---
split_vc
	exceptional postcondition			---	---
	unfold heap_order
		exceptional postcondition		---	---
		split_vc
			exceptional postcondition	0.01	---
	index in array bounds			---	0.05
	index in array bounds			---	0.06
	precondition			0.03	---
	precondition			---	0.07
	precondition			---	0.06
	type invariant			---	0.17
	type invariant			0.01	---
	postcondition			---	0.07
	postcondition			0.01	---
	type invariant			0.02	---
	type invariant			---	0.04
	postcondition			0.10	---
	postcondition			0.05	---
VC for move_up				---	---
split_vc
	index in array bounds			0.02	---
	postcondition			0.05	---
	check division by zero			0.01	---
	index in array bounds			0.00	---
	index in array bounds			0.01	---
	variant decrease			0.03	---
	precondition			0.02	---
	precondition			0.86	---
	precondition			0.12	---
	precondition			0.02	---
	postcondition			0.02	---
	index in array bounds			0.01	---
	postcondition			0.25	---
VC for insert				---	---
split_vc
	exceptional postcondition			0.01	0.05
	index in array bounds			0.03	---
	type invariant			0.04	---
	type invariant			0.02	---
	postcondition			---	---
	split_vc
		postcondition		0.02	0.06
	check division by zero			0.01	0.04
	index in array bounds			0.02	0.07
	index in array bounds			0.03	0.07
	precondition			0.03	---
	precondition			0.19	---
	precondition			0.11	---
	precondition			0.05	---
	type invariant			0.04	---
	type invariant			0.02	0.08
	postcondition			0.01	0.07
	index in array bounds			0.03	0.08
	type invariant			0.02	---
	type invariant			0.16	---
	postcondition			0.02	0.04