Why3 Proof Results for Project "robdd"

Theory "robdd.BDDType": fully verified

Obligations	Z3 4.12.3
VC for true_branch	0.01
VC for false_branch	0.01
VC for var	0.01
VC for eq1	0.01
VC for value	0.01
VC for bool_to_leaf	0.01

Theory "robdd.Hashtbl": fully verified

Obligations	Z3 4.12.3
VC for t	0.03

Theory "robdd.BDD": fully verified

Obligations	Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
VC for hctable	0.02	0.03	0.01
bdd_is_unique	2.31	0.03	0.01
eq1_match_logic	0.06	0.03	0.01
eq0_match_logic	0.02	0.03	0.01
VC for create_hctable	0.02	0.03	0.01
VC for create_node	---	8.07	0.27

Theory "robdd.Not": fully verified

Obligations		Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
VC for memoMap		0.01	0.02	0.02
VC for init_memo_map		0.01	0.02	0.03
VC for apply		---	---	---
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.04
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.04
	postcondition	---	---	0.01
	postcondition	---	---	0.02
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	precondition	---	---	0.01
	variant decrease	---	---	0.02
	precondition	---	---	0.02
	precondition	---	---	0.01
	variant decrease	---	---	0.02
	precondition	---	---	0.01
	precondition	---	---	0.01
	precondition	---	---	0.02
	precondition	---	---	0.02
	precondition	---	---	0.01
	precondition	---	---	0.01
	type invariant	---	---	0.02
	type invariant	---	---	0.02
	type invariant	---	---	0.03
	type invariant	---	---	0.05
	type invariant	---	---	0.09
	postcondition	---	---	0.01
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02
	postcondition	---	---	0.02

Theory "robdd.Size": fully verified

Obligations		Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
true_branch_in_sub_nodes		---	---	0.03
false_branch_in_sub_nodes		---	---	0.04
sub_nodes_with_true_branch		---	---	---
induction_ty_lex
	sub_nodes_with_true_branch.0	0.03	---	---
sub_nodes_with_false_branch		---	---	---
induction_ty_lex
	sub_nodes_with_false_branch.0	0.03	---	---
bdd_in_their_subnodes		---	---	0.02
VC for top_bottom_not_in_subnodes		0.07	---	---
VC for size		---	---	---
split_vc
	precondition	---	---	0.10
	precondition	---	---	0.16
	variant decrease	---	---	0.24
	precondition	---	---	0.03
	precondition	---	---	0.02
	precondition	0.07	---	---
	precondition	---	---	0.02
	precondition	---	---	0.03
	precondition	---	---	0.51
	precondition	---	---	0.67
	variant decrease	---	---	0.49
	precondition	---	---	0.04
	precondition	---	---	0.04
	precondition	0.02	---	---
	precondition	---	---	0.04
	precondition	---	---	0.02
	postcondition	0.02	---	---
	postcondition	---	0.11	---
	postcondition	---	---	0.02
	postcondition	---	0.16	0.06
	postcondition	---	---	0.02
	postcondition	0.02	---	---
	postcondition	---	0.39	---
	postcondition	---	---	0.01
	postcondition	---	0.04	0.04
	postcondition	---	---	0.03
	precondition	---	---	0.19
	precondition	---	---	0.16
	variant decrease	---	---	0.24
	precondition	---	---	0.04
	precondition	---	---	0.03
	precondition	0.06	---	---
	precondition	---	---	0.02
	precondition	---	---	0.03
	postcondition	0.02	---	---
	postcondition	---	0.44	---
	postcondition	---	---	0.02
	postcondition	---	0.04	0.04
	postcondition	---	---	0.03
	postcondition	0.04	---	---
	postcondition	---	0.31	---
	postcondition	---	---	0.02
	postcondition	---	0.03	0.03
	postcondition	---	---	0.02
	precondition	---	---	0.18
	precondition	---	---	0.14
	variant decrease	---	---	0.23
	precondition	---	---	0.02
	precondition	---	---	0.03
	precondition	0.01	---	---
	precondition	---	---	0.03
	precondition	---	---	0.04
	precondition	---	---	0.64
	precondition	---	---	0.61
	variant decrease	---	---	0.77
	precondition	---	---	0.04
	precondition	---	---	0.04
	precondition	0.02	---	---
	precondition	---	---	0.02
	precondition	---	---	0.03
	postcondition	0.01	---	---
	postcondition	---	1.57	---
	postcondition	---	---	0.01
	postcondition	---	0.04	0.04
postcondition	---	---	0.03
postcondition	0.02	---	---
postcondition	---	0.61	---
postcondition	---	---	0.01
postcondition	---	0.02	0.02
postcondition	---	---	0.03
precondition	---	---	0.18
precondition	---	---	0.24
variant decrease	---	---	0.21
precondition	---	---	0.03
precondition	---	---	0.03
precondition	0.02	---	---
precondition	---	---	0.02
precondition	---	---	0.03
postcondition	0.02	---	---
postcondition	---	0.63	---
postcondition	---	---	0.02
postcondition	---	0.03	0.03
postcondition	---	---	0.02
postcondition	0.02	---	---
postcondition	---	0.36	---
postcondition	---	---	0.02
postcondition	---	0.02	0.01
postcondition	---	---	0.03
precondition	---	---	0.02
precondition	---	---	0.03
precondition	---	---	0.04
precondition	---	---	0.03
precondition	---	---	0.03
assertion	0.02	---	---
postcondition	---	---	0.01
assertion	---	---	0.42
postcondition	---	---	0.03

Theory "robdd.BinOp": fully verified

Obligations		Z3 4.12.3
VC for memoMap		0.03
VC for init_memo_map		0.02
VC for apply		---
split_vc
	unreachable point	0.02
	unreachable point	0.03
	unreachable point	0.02
	postcondition	0.03
	postcondition	0.03
	postcondition	0.02
	postcondition	0.02
	postcondition	0.03
	postcondition	0.02
	postcondition	0.02
	postcondition	0.03
	postcondition	0.02
	postcondition	0.01
	postcondition	0.08
	postcondition	0.02
	postcondition	0.02
	postcondition	0.02
	postcondition	0.02
	postcondition	0.02
	postcondition	0.03
	postcondition	0.03
	postcondition	0.02
	postcondition	0.01
	postcondition	0.02
	postcondition	0.02
	VC for apply	0.01
	precondition	0.02
	variant decrease	0.02
	precondition	0.02
	precondition	0.02
	variant decrease	0.02
	precondition	0.02
	precondition	0.02
	precondition	0.02
	precondition	0.02
	precondition	0.01
	precondition	0.02
	type invariant	0.04
	type invariant	0.05
	type invariant	0.28
	type invariant	0.20
	type invariant	0.11
	type invariant	0.25
	type invariant	0.11
	postcondition	0.02
	postcondition	0.03
	postcondition	0.11
	postcondition	0.05
	postcondition	0.01
	postcondition	0.02
	postcondition	0.03
	postcondition	0.03
	postcondition	0.02
	postcondition	0.01
	postcondition	0.03
	precondition	0.02
	variant decrease	0.02
	precondition	0.02
	precondition	0.02
	variant decrease	0.02
	precondition	0.02
	precondition	0.02
	precondition	0.02
	precondition	0.02
precondition	0.01
precondition	0.02
type invariant	0.05
type invariant	0.05
type invariant	0.10
type invariant	0.18
type invariant	0.12
type invariant	0.16
type invariant	0.07
postcondition	0.01
postcondition	0.02
postcondition	0.07
postcondition	0.06
postcondition	0.02
postcondition	0.01
postcondition	0.02
postcondition	0.02
postcondition	0.02
postcondition	0.01
postcondition	0.02
precondition	0.01
precondition	0.02
precondition	0.02
precondition	0.03
variant decrease	0.01
precondition	0.02
precondition	0.01
precondition	0.02
variant decrease	0.02
precondition	0.01
precondition	0.01
precondition	0.14
precondition	0.07
precondition	0.01
precondition	0.01
type invariant	0.02
type invariant	0.15
type invariant	0.53
type invariant	0.36
type invariant	0.50
type invariant	0.69
type invariant	0.23
postcondition	0.02
postcondition	0.03
postcondition	0.33
postcondition	0.30
postcondition	0.02
postcondition	0.01
postcondition	0.03
postcondition	0.03
postcondition	0.04
postcondition	0.02
postcondition	0.03
precondition	0.01
precondition	0.01
precondition	0.02
variant decrease	0.02
precondition	0.03
precondition	0.02
variant decrease	0.03
precondition	0.02
precondition	0.02
precondition	0.06
precondition	0.05
precondition	0.02
precondition	0.01
type invariant	0.03
type invariant	0.12
type invariant	0.52
type invariant	0.58
type invariant	0.57
type invariant	0.29
type invariant	0.09
postcondition	0.02
postcondition	0.02
postcondition	0.17
postcondition	0.12
postcondition	0.02
postcondition	0.01
postcondition	0.03
postcondition	0.02
postcondition	0.04
postcondition	0.01
postcondition	0.02
precondition	0.02
variant decrease	0.02
precondition	0.02
precondition	0.02
variant decrease	0.01
precondition	0.02
precondition	0.02
precondition	0.06
precondition	0.04
precondition	0.02
precondition	0.01
type invariant	0.14
type invariant	0.22
type invariant	0.32
type invariant	0.31
type invariant	0.25
type invariant	0.19
type invariant	0.12
postcondition	0.02
postcondition	0.02
postcondition	0.17
postcondition	0.11
postcondition	0.01
postcondition	0.01
postcondition	0.03
postcondition	0.03
postcondition	0.04
postcondition	0.01
postcondition	0.03

Theory "robdd.Sat": fully verified

Obligations	Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
VC for value_match	0.32	---	---
top_is_sat	---	---	0.04
VC for nodes_are_sat	---	0.13	---
VC for is_sat	0.03	---	---

Theory "robdd.AnySat": fully verified

Obligations		Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
VC for array_value		0.16	---	---
VC for array_value_same_eval		0.68	---	---
VC for any_sat		---	---	---
split_vc
	array creation size	---	---	0.01
	postcondition	---	---	0.03
	postcondition	---	---	0.01
	postcondition	---	---	0.01
	unreachable point	---	---	0.03
	index in array bounds	0.21	---	---
	variant decrease	---	---	0.01
	precondition	0.13	---	---
	precondition	0.46	---	---
	precondition	0.16	---	---
	precondition	---	0.91	---
	postcondition	0.63	---	---
	postcondition	0.36	---	---
	postcondition	---	---	0.02
	variant decrease	---	---	0.02
	precondition	0.13	---	---
	precondition	0.40	---	---
	precondition	0.13	---	---
	precondition	0.10	---	---
	postcondition	0.51	---	---
	postcondition	0.04	---	---
	postcondition	---	---	0.02
	precondition	---	---	0.02
	precondition	---	---	0.02
	precondition	---	---	0.04
	precondition	---	---	0.03
	postcondition	---	---	0.02
	postcondition	---	---	0.04

Theory "robdd.CountSat": fully verified

Obligations				Alt-Ergo 2.4.3	CVC5 1.0.5	Z3 4.12.3
VC for seq_value				0.03	---	---
VC for array_value_same_eval				0.39	---	---
VC for all_sat				---	---	---
split_vc
	precondition			---	---	0.04
	precondition			---	---	0.03
	integer overflow			---	---	0.02
	variant decrease			---	---	0.02
	precondition			---	---	0.05
	precondition			---	---	0.01
	precondition			---	---	0.01
	precondition			---	---	0.03
	precondition			---	---	0.01
	integer overflow			---	---	0.03
	variant decrease			---	---	0.03
	precondition			---	---	0.06
	precondition			---	---	0.01
	precondition			---	---	0.01
	precondition			---	---	0.02
	precondition			---	---	0.03
	assertion			---	---	0.05
	assertion			---	---	0.02
	precondition			---	---	0.02
	precondition			---	---	0.02
	integer overflow			---	---	0.11
	variant decrease			---	---	0.01
	precondition			---	---	0.02
	precondition			0.06	---	---
	precondition			---	---	0.31
	precondition			---	---	0.36
	precondition			---	---	0.01
	integer overflow			---	---	0.03
	variant decrease			---	---	0.02
	precondition			---	---	0.04
	precondition			---	---	1.35
	precondition			---	---	0.50
	precondition			---	---	0.39
	precondition			---	---	0.01
	assertion			---	---	0.04
	integer overflow			---	---	0.11
	variant decrease			---	---	0.02
	precondition			---	---	0.03
	precondition			---	---	0.01
	precondition			---	---	0.02
	precondition			0.02	---	---
	precondition			---	---	0.02
	integer overflow			---	---	0.03
	variant decrease			---	---	0.02
	precondition			---	---	0.03
	precondition			---	---	0.02
	precondition			---	---	0.01
	precondition			0.02	---	---
	precondition			---	---	0.02
	assertion			---	---	0.03
	postcondition			0.97	---	---
	postcondition			---	---	---
	split_vc
		postcondition		---	---	0.02
		postcondition		---	---	0.03
		postcondition		0.10	---	---
	postcondition			---	---	---
	split_vc
		postcondition		---	---	0.02
		postcondition		---	0.08	---
		postcondition		---	0.54	---
	postcondition			---	---	---
	split_vc
		postcondition		---	---	0.03
postcondition		---	---	---
split_vc
		postcondition	---	---	0.03
		postcondition	---	1.26	---
postcondition		---	---	---
split_vc
		postcondition	---	0.42	---
		postcondition	0.57	---	---
postcondition			0.93	---	---
postcondition			---	---	0.02
postcondition			0.03	---	---
VC for count_sat				---	0.15	---