Why3 Proof Results for Project "challenge2_complete"

Theory "challenge2_complete.BDDModel": fully verified

Obligations		Alt-Ergo 2.4.2	CVC5 1.0.3	Z3 4.11.2
VC for size		0.01	---	---
VC for ordered_congruence		0.12	---	---
VC for eval_constant_distinguisher		---	---	---
split_vc
	variant decrease	0.01	---	---
	precondition	0.01	---	---
	variant decrease	0.00	---	---
	precondition	0.01	---	---
	unreachable point	0.00	---	---
	precondition	0.01	---	---
	precondition	0.00	---	---
	precondition	0.01	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	postcondition	---	0.06	0.04
VC for eval_distinguisher		---	---	---
split_vc
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	variant decrease	0.01	---	---
	precondition	0.03	---	---
	unreachable point	0.01	---	---
	precondition	0.01	---	---
	precondition	0.01	---	---
	precondition	0.02	---	---
	precondition	0.01	---	---
	assertion	0.01	---	---
	precondition	0.02	---	---
	precondition	0.01	---	---
	postcondition	0.61	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.01	---	---
	variant decrease	0.00	---	---
	precondition	0.02	---	---
	variant decrease	0.01	---	---
	precondition	0.02	---	---
	precondition	0.01	---	---
	precondition	0.01	---	---
	precondition	0.00	---	---
	precondition	0.01	---	---
	precondition	0.01	---	---
	precondition	0.00	---	---
	precondition	0.01	---	---
	precondition	0.01	---	---
	precondition	0.00	---	---
	precondition	0.00	---	---
	precondition	0.01	---	---
	precondition	0.01	---	---
	postcondition	---	0.07	---
VC for eval_injective		0.01	---	---

Theory "challenge2_complete.BDDNode": fully verified

Obligations	Alt-Ergo 2.4.2
VC for project_cons	0.01
VC for project	0.00
equal_refl	0.01
equal_symm	0.01
equal_trans	0.18
hash_congr	0.01

Theory "challenge2_complete.BDD": fully verified

Obligations			Alt-Ergo 2.4.2	CVC5 1.0.3	Z3 4.11.2
VC for nodes_in_table			0.00	---	---
VC for nodes_cons_in_table			0.01	---	---
sub_table_partial_order			0.01	---	---
VC for nodes_in_table_monotonic			0.01	---	---
VC for nodes_cons_in_table_monotonic			0.02	---	---
VC for empty_witness			0.01	---	---
VC for bdd			0.01	---	---
VC for mk_node			---	---	---
split_vc
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.05	---	---
	precondition		0.00	---	---
	type invariant		0.01	---	---
	type invariant		---	---	---
	split_vc
		type invariant	0.01	---	---
		type invariant	0.02	---	---
		type invariant	---	---	0.04
		type invariant	0.01	---	---
	type invariant		0.04	---	---
	type invariant		4.11	---	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.01	---	---
VC for mk_true			0.02	---	---
VC for mk_false			0.02	---	---
VC for mk_if_challenge			0.32	---	---
VC for mk_if			0.09	---	---
VC for mk_var			1.12	---	---
VC for mk_not			---	---	---
split_vc
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.08	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	variant decrease		0.04	---	---
	precondition		0.01	---	---
	variant decrease		0.03	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.21	---	---
	precondition		0.21	---	---
	postcondition		---	0.05	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.04	---	---
VC for compare			0.01	---	---
VC for mk_and_challenge			---	---	---
split_vc
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.12	---	---
	postcondition		0.01	---	---
	variant decrease		0.09	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	variant decrease		0.09	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.25	---	---
	precondition		2.45	---	---
	postcondition		---	0.07	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.07	---	---
	variant decrease		0.05	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	variant decrease		0.08	---	---
	precondition		0.02	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.41	---	---
	precondition		0.88	---	---
	postcondition		---	0.07	---
	postcondition		0.01	---	---
	postcondition		0.36	---	---
	postcondition		0.05	---	---
	variant decrease		0.06	---	---
	precondition		0.01	---	---
	precondition		0.02	---	---
	variant decrease		0.09	---	---
precondition		0.01	---	---
precondition		0.02	---	---
precondition		0.01	---	---
precondition		0.01	---	---
precondition		0.35	---	---
precondition		2.56	---	---
postcondition		---	0.06	---
postcondition		0.01	---	---
postcondition		0.03	---	---
postcondition		0.06	---	---
unreachable point		0.01	---	---
VC for mk_and			---	---	---
split_vc
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.11	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.02	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.01	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.02	---	---
	precondition		0.40	---	---
	precondition		2.82	---	---
	postcondition		---	0.07	---
	postcondition		0.01	---	---
	postcondition		0.02	---	---
	postcondition		0.06	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.02	---	---
	precondition		0.00	---	---
	precondition		0.01	---	---
	precondition		0.21	---	---
	precondition		0.62	---	---
	postcondition		---	0.06	---
	postcondition		0.01	---	---
	postcondition		0.21	---	---
	postcondition		0.06	---	---
	precondition		0.00	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.28	---	---
	precondition		2.74	---	---
postcondition		---	0.06	---
postcondition		0.01	---	---
postcondition		0.02	---	---
postcondition		0.06	---	---
VC for mk_or			---	---	---
split_vc
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	postcondition		0.00	---	---
	postcondition		0.01	---	---
	postcondition		0.01	---	---
	variant decrease		0.04	---	---
	precondition		0.01	---	---
	precondition		0.00	---	---
	variant decrease		0.07	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.28	---	---
	precondition		1.80	---	---
	postcondition		---	0.06	---
	postcondition		0.01	---	---
	postcondition		0.10	---	---
	postcondition		0.06	---	---
	variant decrease		0.04	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	variant decrease		0.06	---	---
	precondition		0.02	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.01	---	---
	precondition		0.39	---	---
	precondition		0.58	---	---
	postcondition		---	0.07	---
	postcondition		0.00	---	---
	postcondition		0.39	---	---
	postcondition		0.05	---	---
	variant decrease		0.04	---	---
	precondition		0.00	---	---
	precondition		0.01	---	---
	variant decrease		0.12	---	---
precondition		0.01	---	---
precondition		0.02	---	---
precondition		0.00	---	---
precondition		0.01	---	---
precondition		0.26	---	---
precondition		2.14	---	---
postcondition		---	0.06	---
postcondition		0.01	---	---
postcondition		0.09	---	---
postcondition		0.06	---	---

Theory "challenge2_complete.BDDCheck": fully verified

Obligations		Alt-Ergo 2.4.2	CVC5 1.0.3
VC for lookup_is_member		0.01	---
VC for member_congruent		0.02	---
VC for lookup_congruent		0.03	---
VC for assoc_list		0.01	---
VC for model_eval		---	---
split_vc
	unreachable point	0.00	---
	variant decrease	0.01	---
	precondition	0.01	---
	precondition	0.00	---
	postcondition	---	0.02
	postcondition	---	0.04
	precondition	0.00	---
	precondition	0.00	---
	postcondition	0.00	---
	postcondition	---	0.04
VC for create		0.01	---
VC for find_opt		0.03	---
VC for add		0.06	---
VC for model_mem_congr'refn		0.01	---
VC for model_eval'refn		0.00	---
VC for model_eval_congr'refn		0.01	---
VC for find_opt'refn		0.01	---
VC for create'refn		0.00	---
VC for add'refn		0.00	---