Why3 Proof Results for Project "code"

Theory "code.BAchar": fully verified

Obligations			Alt-Ergo 2.3.0	Z3 4.8.6
VC for one_bit			---	---
split_vc
	assertion		---	0.03
	assertion		---	0.03
	integer overflow		0.07	---
	assertion		0.02	---
	assertion		---	0.03
	postcondition		0.08	---
	postcondition		0.08	---
	postcondition		0.06	---
VC for bit_set			---	---
split_vc
	precondition		0.02	---
	assertion		0.14	---
	split_vc
		assertion	0.11	---
		assertion	0.13	---
	assertion		0.23	---
	assertion		0.17	---
	postcondition		0.14	---
VC for set_bit			---	---
split_vc
	precondition		0.02	---
	postcondition		0.12	---
	postcondition		0.18	---
VC for t			---	---
split_vc
	precondition		0.02	---
	type invariant		0.09	---
	type invariant		0.02	---
	type invariant		0.02	---
	type invariant		0.02	---
	type invariant		0.11	---
VC for create			---	---
split_vc
	integer overflow		0.06	---
	division by zero		0.02	---
	integer overflow		0.11	---
	integer overflow		0.09	---
	precondition		0.09	---
	integer overflow		0.05	---
	loop invariant init		0.03	---
	precondition		---	---
	split_vc
		precondition	0.10	---
	precondition		0.03	---
	precondition		0.03	---
	loop invariant preservation		0.15	---
	precondition		0.03	---
	precondition		0.07	---
	precondition		0.02	---
	precondition		0.03	---
	precondition		0.03	---
	precondition		0.22	---
	postcondition		0.03	---
	postcondition		0.15	---
	out of loop bounds		0.06	---
VC for get			0.23	---
VC for set			---	0.28
VC for create'refn			0.06	---
VC for get'refn			0.02	---
VC for set'refn			0.02	---

Obligations		Alt-Ergo 2.3.0	CVC4 1.7	Z3 4.8.6
VC for bit		0.09	---	---
split_vc
	precondition	0.03	---	---
	division by zero	0.04	---	---
	integer overflow	0.09	---	---
VC for filter		0.03	---	---
VC for bloom_filter		---	---	---
split_vc
	precondition	0.03	---	---
	precondition	0.05	---	---
	precondition	0.05	---	---
	postcondition	0.02	---	---
VC for add		---	---	---
split_vc
	integer overflow	0.01	---	---
	loop invariant init	---	---	0.13
	loop invariant init	0.01	---	---
	loop invariant init	---	---	0.04
	precondition	0.03	---	---
	precondition	0.05	---	---
	precondition	0.05	---	---
	loop invariant preservation	0.07	---	---
	loop invariant preservation	0.27	---	---
	loop invariant preservation	---	0.25	---
	type invariant	0.01	---	---
	type invariant	0.03	---	---
	postcondition	0.01	---	---
	out of loop bounds	0.01	---	---
VC for mem		0.14	---	---
VC for create'refn		0.01	---	---
VC for add'refn		0.01	---	---
VC for mem'refn		0.01	---	---

Obligations	Alt-Ergo 2.3.0
VC for main	0.09