theory Why2 use array.Array as A use unit_inf.Unit use int.Int use int.ComputerDivision use real.Real use bool_inf.Bool predicate eq_unit Unit.unit Unit.unit predicate neq_unit Unit.unit Unit.unit predicate eq_bool Bool.bool Bool.bool predicate neq_bool Bool.bool Bool.bool predicate lt_int int int predicate le_int int int predicate gt_int int int predicate ge_int int int predicate eq_int int int predicate neq_int int int function add_int int int : int function sub_int int int : int function mul_int int int : int function div_int int int : int function mod_int int int : int function neg_int int : int predicate zwf_zero int int axiom Zwf_zero_def: (forall a0:int. (forall b0:int. (((Int.(<=) 0 b0) /\ (Int.(<) a0 b0)) <-> ((Int.(<=) 0 b0) /\ (Int.(<) a0 b0))))) function bool_and Bool.bool Bool.bool : Bool.bool function bool_or Bool.bool Bool.bool : Bool.bool function bool_xor Bool.bool Bool.bool : Bool.bool function bool_not Bool.bool : Bool.bool axiom Bool_and_def: (forall a:Bool.bool. (forall b:Bool.bool. (((bool_and a b : Bool.bool) = Bool.ttrue) <-> ((a = Bool.ttrue) /\ (b = Bool.ttrue))))) axiom Bool_or_def: (forall a:Bool.bool. (forall b:Bool.bool. (((bool_or a b : Bool.bool) = Bool.ttrue) <-> ((a = Bool.ttrue) \/ (b = Bool.ttrue))))) axiom Bool_xor_def: (forall a:Bool.bool. (forall b:Bool.bool. (((bool_xor a b : Bool.bool) = Bool.ttrue) <-> (a <> b)))) axiom Bool_not_def: (forall a:Bool.bool. (((bool_not a : Bool.bool) = Bool.ttrue) <-> (a = Bool.ffalse))) function ite Bool.bool 'a1 'a1 : 'a1 axiom Ite_true: (forall x:'a1. (forall y:'a1. ((ite Bool.ttrue x y : 'a1) = x))) axiom Ite_false: (forall x:'a1. (forall y:'a1. ((ite Bool.ffalse x y : 'a1) = y))) function lt_int_bool int int : Bool.bool function le_int_bool int int : Bool.bool function gt_int_bool int int : Bool.bool function ge_int_bool int int : Bool.bool function eq_int_bool int int : Bool.bool function neq_int_bool int int : Bool.bool axiom Lt_int_bool_axiom: (forall x:int. (forall y:int. (((lt_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(<) x y)))) axiom Le_int_bool_axiom: (forall x:int. (forall y:int. (((le_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(<=) x y)))) axiom Gt_int_bool_axiom: (forall x:int. (forall y:int. (((gt_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(>) x y)))) axiom Ge_int_bool_axiom: (forall x:int. (forall y:int. (((ge_int_bool x y : Bool.bool) = Bool.ttrue) <-> (Int.(>=) x y)))) axiom Eq_int_bool_axiom: (forall x:int. (forall y:int. (((eq_int_bool x y : Bool.bool) = Bool.ttrue) <-> (x = y)))) axiom Neq_int_bool_axiom: (forall x:int. (forall y:int. (((neq_int_bool x y : Bool.bool) = Bool.ttrue) <-> (x <> y)))) function abs_int int : int axiom Abs_int_pos: (forall x:int. ((Int.(>=) x 0) -> ((abs_int x : int) = x))) axiom Abs_int_neg: (forall x:int. ((Int.(<=) x 0) -> ((abs_int x : int) = (Int.(-_) x : int)))) function int_max int int : int function int_min int int : int axiom Int_max_is_ge: (forall x:int. (forall y:int. ((Int.(>=) (int_max x y : int) x) /\ (Int.(>=) (int_max x y : int) y)))) axiom Int_max_is_some: (forall x:int. (forall y:int. (((int_max x y : int) = x) \/ ((int_max x y : int) = y)))) axiom Int_min_is_le: (forall x:int. (forall y:int. ((Int.(<=) (int_min x y : int) x) /\ (Int.(<=) (int_min x y : int) y)))) axiom Int_min_is_some: (forall x:int. (forall y:int. (((int_min x y : int) = x) \/ ((int_min x y : int) = y)))) predicate lt_real real real predicate le_real real real predicate gt_real real real predicate ge_real real real predicate eq_real real real predicate neq_real real real function add_real real real : real function sub_real real real : real function mul_real real real : real function div_real real real : real function neg_real real : real function real_of_int int : real function int_of_real real : int function lt_real_bool real real : Bool.bool function le_real_bool real real : Bool.bool function gt_real_bool real real : Bool.bool function ge_real_bool real real : Bool.bool function eq_real_bool real real : Bool.bool function neq_real_bool real real : Bool.bool axiom Lt_real_bool_axiom: (forall x:real. (forall y:real. (((lt_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(<) x y)))) axiom Le_real_bool_axiom: (forall x:real. (forall y:real. (((le_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(<=) x y)))) axiom Gt_real_bool_axiom: (forall x:real. (forall y:real. (((gt_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(>) x y)))) axiom Ge_real_bool_axiom: (forall x:real. (forall y:real. (((ge_real_bool x y : Bool.bool) = Bool.ttrue) <-> (Real.(>=) x y)))) axiom Eq_real_bool_axiom: (forall x:real. (forall y:real. (((eq_real_bool x y : Bool.bool) = Bool.ttrue) <-> (x = y)))) axiom Neq_real_bool_axiom: (forall x:real. (forall y:real. (((neq_real_bool x y : Bool.bool) = Bool.ttrue) <-> (x <> y)))) function real_max real real : real function real_min real real : real axiom Real_max_is_ge: (forall x:real. (forall y:real. ((Real.(>=) (real_max x y : real) x) /\ (Real.(>=) (real_max x y : real) y)))) axiom Real_max_is_some: (forall x:real. (forall y:real. (((real_max x y : real) = x) \/ ((real_max x y : real) = y)))) axiom Real_min_is_le: (forall x:real. (forall y:real. ((Real.(<=) (real_min x y : real) x) /\ (Real.(<=) (real_min x y : real) y)))) axiom Real_min_is_some: (forall x:real. (forall y:real. (((real_min x y : real) = x) \/ ((real_min x y : real) = y)))) function sqrt_real real : real function pow_real real real : real function abs_real real : real axiom Abs_real_pos: (forall x:real [(abs_real x : real)]. ((Real.(>=) x 0.0) -> ((abs_real x : real) = x))) axiom Abs_real_neg: (forall x:real [(abs_real x : real)]. ((Real.(<=) x 0.0) -> ((abs_real x : real) = (Real.(-_) x : real)))) function exp real : real function log real : real function log10 real : real axiom Log_exp: (forall x:real. ((log (exp x : real) : real) = x)) function cos real : real function sin real : real function tan real : real function cosh real : real function sinh real : real function tanh real : real function acos real : real function asin real : real function atan real : real function atan2 real real : real function hypot real real : real type alloc_table 't type pointer 't type block 't function base_block (pointer 'a1) : (block 'a1) function pointer_address (pointer 'a1) : (pointer Unit.unit) function absolute_address int : (pointer Unit.unit) function address (pointer 'a1) : int function offset_max (alloc_table 'a1) (pointer 'a1) : int function offset_min (alloc_table 'a1) (pointer 'a1) : int predicate valid (alloc_table 'a1) (pointer 'a1) axiom Valid_def: (forall a0:(alloc_table 'a1). (forall p0:(pointer 'a1). ((valid a0 p0) <-> ((Int.(<=) (offset_min a0 p0 : int) 0) /\ (Int.(>=) (offset_max a0 p0 : int) 0))))) predicate same_block (pointer 'a1) (pointer 'a1) axiom Same_block_def: (forall p0:(pointer 'a1). (forall q0:(pointer 'a1). ((same_block p0 q0) <-> ((base_block p0 : (block 'a1)) = (base_block q0 : (block 'a1)))))) function sub_pointer (pointer 'a1) (pointer 'a1) : int function shift (pointer 'a1) int : (pointer 'a1) function null : (pointer 'a1) axiom Address_injective: (forall p:(pointer 'a1). (forall q:(pointer 'a1). ((p = q) <-> ((address p : int) = (address q : int))))) axiom Address_null: ((address (null : (pointer 'a1)) : int) = 0) axiom Address_positive: (forall p:(pointer 'a1). (Int.(<=) 0 (address p : int))) axiom Address_shift_lt: (forall p:(pointer 'a1). (forall i:int. (forall j:int [(address (shift p i : (pointer 'a1)) : int), (address (shift p j : (pointer 'a1)) : int)]. ((Int.(<) (address (shift p i : (pointer 'a1)) : int) (address (shift p j : (pointer 'a1)) : int)) <-> (Int.(<) i j))))) axiom Address_shift_le: (forall p:(pointer 'a1). (forall i:int. (forall j:int [(address (shift p i : (pointer 'a1)) : int), (address (shift p j : (pointer 'a1)) : int)]. ((Int.(<=) (address (shift p i : (pointer 'a1)) : int) (address (shift p j : (pointer 'a1)) : int)) <-> (Int.(<=) i j))))) axiom Shift_zero: (forall p:(pointer 'a1) [(shift p 0 : (pointer 'a1))]. ((shift p 0 : (pointer 'a1)) = p)) axiom Shift_shift: (forall p:(pointer 'a1). (forall i:int. (forall j:int [(shift (shift p i : (pointer 'a1)) j : (pointer 'a1))]. ((shift (shift p i : (pointer 'a1)) j : (pointer 'a1)) = (shift p (Int.(+) i j : int) : (pointer 'a1)))))) axiom Offset_max_shift: (forall a:(alloc_table 'a1). (forall p:(pointer 'a1). (forall i:int. ((offset_max a (shift p i : (pointer 'a1)) : int) = (Int.(-) (offset_max a p : int) i : int))))) axiom Offset_min_shift: (forall a:(alloc_table 'a1). (forall p:(pointer 'a1). (forall i:int. ((offset_min a (shift p i : (pointer 'a1)) : int) = (Int.(-) (offset_min a p : int) i : int))))) axiom Neq_shift: (forall p:(pointer 'a1). (forall i:int. (forall j:int [(shift p i : (pointer 'a1)), (shift p j : (pointer 'a1))]. ((i <> j) -> ((shift p i : (pointer 'a1)) <> (shift p j : (pointer 'a1))))))) axiom Null_not_valid: (forall a:(alloc_table 'a1). (not (valid a (null : (pointer 'a1))))) axiom Null_pointer: (forall a:(alloc_table 'a1). ((Int.(>=) (offset_min a (null : (pointer 'a1)) : int) 0) /\ (Int.(<=) (offset_max a (null : (pointer 'a1)) : int) (Int.(-_) 2 : int)))) function eq_pointer_bool (pointer 'a1) (pointer 'a1) : Bool.bool function neq_pointer_bool (pointer 'a1) (pointer 'a1) : Bool.bool axiom Eq_pointer_bool_def: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (((eq_pointer_bool p1 p2 : Bool.bool) = Bool.ttrue) <-> (p1 = p2)))) axiom Neq_pointer_bool_def: (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (((neq_pointer_bool p1 p2 : Bool.bool) = Bool.ttrue) <-> (p1 <> p2)))) axiom Same_block_shift_right: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(same_block p (shift q i : (pointer 'a1)))]. ((same_block p q) -> (same_block p (shift q i : (pointer 'a1))))))) axiom Same_block_shift_left: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(same_block (shift q i : (pointer 'a1)) p)]. ((same_block q p) -> (same_block (shift q i : (pointer 'a1)) p))))) axiom Sub_pointer_shift: (forall p:(pointer 'a1). (forall q:(pointer 'a1) [(sub_pointer p q : int)]. ((same_block p q) -> (p = (shift q (sub_pointer p q : int) : (pointer 'a1)))))) axiom Sub_pointer_self: (forall p:(pointer 'a1) [(sub_pointer p p : int)]. ((sub_pointer p p : int) = 0)) axiom Sub_pointer_zero: (forall p:(pointer 'a1). (forall q:(pointer 'a1) [(sub_pointer p q : int)]. ((same_block p q) -> (((sub_pointer p q : int) = 0) -> (p = q))))) axiom Sub_pointer_shift_left: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(sub_pointer (shift p i : (pointer 'a1)) q : int)]. ((sub_pointer (shift p i : (pointer 'a1)) q : int) = (Int.(+) (sub_pointer p q : int) i : int))))) axiom Sub_pointer_shift_right: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(sub_pointer p (shift q i : (pointer 'a1)) : int)]. ((sub_pointer p (shift q i : (pointer 'a1)) : int) = (Int.(-) (sub_pointer p q : int) i : int))))) type memory 't 'v = A.t (pointer 't) 'v function select (m:memory 'a1 'a2) (k:pointer 'a1) : 'a2 = A.get m k function store (m:memory 'a1 'a2) (k:pointer 'a1) (v:'a2) : (memory 'a1 'a2) = A.set m k v type pset 't function pset_empty : (pset 'a1) function pset_singleton (pointer 'a1) : (pset 'a1) function pset_deref (memory 'a2 (pointer 'a1)) (pset 'a2) : (pset 'a1) function pset_union (pset 'a1) (pset 'a1) : (pset 'a1) function pset_all (pset 'a1) : (pset 'a1) function pset_range (pset 'a1) int int : (pset 'a1) function pset_range_left (pset 'a1) int : (pset 'a1) function pset_range_right (pset 'a1) int : (pset 'a1) predicate in_pset (pointer 'a1) (pset 'a1) predicate valid_pset (alloc_table 'a1) (pset 'a1) predicate pset_disjoint (pset 'a1) (pset 'a1) axiom Pset_disjoint_def: (forall ps1_0:(pset 'a1). (forall ps2_0:(pset 'a1). ((pset_disjoint ps1_0 ps2_0) <-> (forall p:(pointer 'a1). (not ((in_pset p ps1_0) /\ (in_pset p ps2_0))))))) predicate pset_included (pset 'a1) (pset 'a1) axiom Pset_included_def: (forall ps1_0:(pset 'a1). (forall ps2_0:(pset 'a1). ((pset_included ps1_0 ps2_0) <-> (forall p:(pointer 'a1). ((in_pset p ps1_0) -> (in_pset p ps2_0)))))) axiom Pset_included_self: (forall ps:(pset 'a1). (pset_included ps ps)) axiom Pset_included_range: (forall ps:(pset 'a1). (forall a:int. (forall b:int. (forall c:int. (forall d:int [(pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1)))]. (((Int.(<=) c a) /\ (Int.(<=) b d)) -> (pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1))))))))) axiom Pset_included_range_all: (forall ps:(pset 'a1). (forall a:int. (forall b:int. (forall c:int. (forall d:int [(pset_included (pset_range ps a b : (pset 'a1)) (pset_range ps c d : (pset 'a1)))]. (pset_included (pset_range ps a b : (pset 'a1)) (pset_all ps : (pset 'a1)))))))) axiom In_pset_empty: (forall p:(pointer 'a1). (not (in_pset p (pset_empty : (pset 'a1))))) axiom In_pset_singleton: (forall p:(pointer 'a1). (forall q:(pointer 'a1). ((in_pset p (pset_singleton q : (pset 'a1))) <-> (p = q)))) axiom In_pset_deref: (forall p:(pointer 'a1). (forall m:(memory 'a2 (pointer 'a1)). (forall q:(pset 'a2). ((in_pset p (pset_deref m q : (pset 'a1))) <-> (exists r:(pointer 'a2). ((in_pset r q) /\ (p = (select m r : (pointer 'a1))))))))) axiom In_pset_all: (forall p:(pointer 'a1). (forall q:(pset 'a1). ((in_pset p (pset_all q : (pset 'a1))) <-> (exists i:int. (exists r:(pointer 'a1). ((in_pset r q) /\ (p = (shift r i : (pointer 'a1))))))))) axiom In_pset_range: (forall p:(pointer 'a1). (forall q:(pset 'a1). (forall a:int. (forall b:int. ((in_pset p (pset_range q a b : (pset 'a1))) <-> (exists i:int. (exists r:(pointer 'a1). ((Int.(<=) a i) /\ ((Int.(<=) i b) /\ ((in_pset r q) /\ (p = (shift r i : (pointer 'a1))))))))))))) axiom In_pset_range_left: (forall p:(pointer 'a1). (forall q:(pset 'a1). (forall b:int. ((in_pset p (pset_range_left q b : (pset 'a1))) <-> (exists i:int. (exists r:(pointer 'a1). ((Int.(<=) i b) /\ ((in_pset r q) /\ (p = (shift r i : (pointer 'a1))))))))))) axiom In_pset_range_right: (forall p:(pointer 'a1). (forall q:(pset 'a1). (forall a:int. ((in_pset p (pset_range_right q a : (pset 'a1))) <-> (exists i:int. (exists r:(pointer 'a1). ((Int.(<=) a i) /\ ((in_pset r q) /\ (p = (shift r i : (pointer 'a1))))))))))) axiom In_pset_union: (forall p:(pointer 'a1). (forall s1:(pset 'a1). (forall s2:(pset 'a1). ((in_pset p (pset_union s1 s2 : (pset 'a1))) <-> ((in_pset p s1) \/ (in_pset p s2)))))) axiom Valid_pset_empty: (forall a:(alloc_table 'a1). (valid_pset a (pset_empty : (pset 'a1)))) axiom Valid_pset_singleton: (forall a:(alloc_table 'a1). (forall p:(pointer 'a1). ((valid_pset a (pset_singleton p : (pset 'a1))) <-> (valid a p)))) axiom Valid_pset_deref: (forall a:(alloc_table 'a1). (forall m:(memory 'a2 (pointer 'a1)). (forall q:(pset 'a2). ((valid_pset a (pset_deref m q : (pset 'a1))) <-> (forall r:(pointer 'a2). (forall p:(pointer 'a1). (((in_pset r q) /\ (p = (select m r : (pointer 'a1)))) -> (valid a p)))))))) axiom Valid_pset_range: (forall a:(alloc_table 'a1). (forall q:(pset 'a1). (forall c:int. (forall d:int. ((valid_pset a (pset_range q c d : (pset 'a1))) <-> (forall i:int. (forall r:(pointer 'a1). (((in_pset r q) /\ ((Int.(<=) c i) /\ (Int.(<=) i d))) -> (valid a (shift r i : (pointer 'a1))))))))))) axiom Valid_pset_union: (forall a:(alloc_table 'a1). (forall s1:(pset 'a1). (forall s2:(pset 'a1). ((valid_pset a (pset_union s1 s2 : (pset 'a1))) <-> ((valid_pset a s1) /\ (valid_pset a s2)))))) predicate not_assigns (alloc_table 'a1) (memory 'a1 'a2) (memory 'a1 'a2) (pset 'a1) axiom Not_assigns_def: (forall a0:(alloc_table 'a1). (forall m1_0:(memory 'a1 'a2). (forall m2_0:(memory 'a1 'a2). (forall l0:(pset 'a1). ((not_assigns a0 m1_0 m2_0 l0) <-> (forall p:(pointer 'a1). (((valid a0 p) /\ (not (in_pset p l0))) -> ((select m2_0 p : 'a2) = (select m1_0 p : 'a2))))))))) axiom Not_assigns_refl: (forall a:(alloc_table 'a1). (forall m:(memory 'a1 'a2). (forall l:(pset 'a1). (not_assigns a m m l)))) axiom Not_assigns_trans: (forall a:(alloc_table 'a1). (forall m1:(memory 'a1 'a2). (forall m2:(memory 'a1 'a2). (forall m3:(memory 'a1 'a2). (forall l:(pset 'a1) [(not_assigns a m1 m2 l), (not_assigns a m1 m3 l)]. ((not_assigns a m1 m2 l) -> ((not_assigns a m2 m3 l) -> (not_assigns a m1 m3 l)))))))) predicate full_separated (pointer 'a1) (pointer 'a2) axiom Full_separated_shift1: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(full_separated p q), (shift q i : (pointer 'a1))]. ((full_separated p q) -> (full_separated p (shift q i : (pointer 'a1))))))) axiom Full_separated_shift2: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(full_separated p q), (shift q i : (pointer 'a1))]. ((full_separated p q) -> (full_separated (shift q i : (pointer 'a1)) p))))) axiom Full_separated_shift3: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(full_separated q p), (shift q i : (pointer 'a1))]. ((full_separated q p) -> (full_separated (shift q i : (pointer 'a1)) p))))) axiom Full_separated_shift4: (forall p:(pointer 'a1). (forall q:(pointer 'a1). (forall i:int [(full_separated q p), (shift q i : (pointer 'a1))]. ((full_separated q p) -> (full_separated p (shift q i : (pointer 'a1))))))) type tag_table 't type tag_id 't function int_of_tag (tag_id 'a1) : int function typeof (tag_table 'a1) (pointer 'a1) : (tag_id 'a1) predicate parenttag (tag_id 'a1) (tag_id 'a1) predicate subtag (tag_id 'a1) (tag_id 'a1) function subtag_bool (tag_id 'a1) (tag_id 'a1) : Bool.bool axiom Subtag_bool_def: (forall t1:(tag_id 'a1). (forall t2:(tag_id 'a1). (((subtag_bool t1 t2 : Bool.bool) = Bool.ttrue) <-> (subtag t1 t2)))) axiom Subtag_refl: (forall t:(tag_id 'a1). (subtag t t)) axiom Subtag_parent: (forall t1:(tag_id 'a1). (forall t2:(tag_id 'a1). (forall t3:(tag_id 'a1). ((subtag t1 t2) -> ((parenttag t2 t3) -> (subtag t1 t3)))))) predicate instanceof (tag_table 'a1) (pointer 'a1) (tag_id 'a1) axiom Instanceof_def: (forall a0:(tag_table 'a1). (forall p0:(pointer 'a1). (forall t0:(tag_id 'a1). ((instanceof a0 p0 t0) <-> (subtag (typeof a0 p0 : (tag_id 'a1)) t0))))) function downcast (tag_table 'a1) (pointer 'a1) (tag_id 'a1) : (pointer 'a1) axiom Downcast_instanceof: (forall a:(tag_table 'a1). (forall p:(pointer 'a1). (forall s:(tag_id 'a1). ((instanceof a p s) -> ((downcast a p s : (pointer 'a1)) = p))))) function bottom_tag : (tag_id 'a1) axiom Bottom_tag_axiom: (forall t:(tag_id 'a1). (subtag t (bottom_tag : (tag_id 'a1)))) predicate root_tag (tag_id 'a1) axiom Root_tag_def: (forall t0:(tag_id 'a1). ((root_tag t0) <-> (parenttag t0 (bottom_tag : (tag_id 'a1))))) axiom Root_subtag: (forall a:(tag_id 'a1). (forall b:(tag_id 'a1). (forall c:(tag_id 'a1). ((root_tag a) -> ((root_tag b) -> ((a <> b) -> ((subtag c a) -> (not (subtag c b))))))))) predicate fully_packed (tag_table 'a1) (memory 'a1 (tag_id 'a1)) (pointer 'a1) axiom Fully_packed_def: (forall tag_table0:(tag_table 'a1). (forall mutable0:(memory 'a1 (tag_id 'a1)). (forall this0:(pointer 'a1). ((fully_packed tag_table0 mutable0 this0) <-> ((select mutable0 this0 : (tag_id 'a1)) = (typeof tag_table0 this0 : (tag_id 'a1))))))) function bw_compl int : int function bw_and int int : int axiom Bw_and_not_null: (forall a:int. (forall b:int. (((bw_and a b : int) <> 0) -> ((a <> 0) /\ (b <> 0))))) function bw_xor int int : int function bw_or int int : int function lsl int int : int axiom Lsl_left_positive_returns_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (lsl a b : int))))) axiom Lsl_left_positive_monotone: (forall a1:int. (forall a2:int. (forall b:int. (((Int.(<=) 0 a1) /\ ((Int.(<=) a1 a2) /\ (Int.(<=) 0 b))) -> (Int.(<=) (lsl a1 b : int) (lsl a2 b : int)))))) function lsr int int : int axiom Lsr_left_positive_returns_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (lsr a b : int))))) axiom Lsr_left_positive_decreases: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) (lsr a b : int) a)))) function asr int int : int axiom Asr_positive_on_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) 0 (asr a b : int))))) axiom Asr_decreases_on_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) (asr a b : int) a)))) axiom Asr_lsr_same_on_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> ((asr a b : int) = (lsr a b : int))))) axiom Lsl_of_lsr_decreases_on_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> (Int.(<=) (lsl (lsr a b : int) b : int) a)))) axiom Lsr_of_lsl_identity_on_positive: (forall a:int. (forall b:int. (((Int.(<=) 0 a) /\ (Int.(<=) 0 b)) -> ((lsr (lsl a b : int) b : int) = a)))) predicate alloc_extends (alloc_table 'a1) (alloc_table 'a1) predicate alloc_fresh (alloc_table 'a1) (pointer 'a1) int axiom Alloc_fresh_def: (forall a0:(alloc_table 'a1). (forall p0:(pointer 'a1). (forall n0:int. ((alloc_fresh a0 p0 n0) <-> (forall i:int. (((Int.(<=) 0 i) /\ (Int.(<) i n0)) -> (not (valid a0 (shift p0 i : (pointer 'a1)))))))))) axiom Alloc_extends_offset_min: (forall a1:(alloc_table 'a1). (forall a2:(alloc_table 'a1) [(alloc_extends a1 a2)]. ((alloc_extends a1 a2) -> (forall p:(pointer 'a1). ((valid a1 p) -> ((offset_min a1 p : int) = (offset_min a2 p : int))))))) axiom Alloc_extends_offset_max: (forall a1:(alloc_table 'a1). (forall a2:(alloc_table 'a1) [(alloc_extends a1 a2)]. ((alloc_extends a1 a2) -> (forall p:(pointer 'a1). ((valid a1 p) -> ((offset_max a1 p : int) = (offset_max a2 p : int))))))) axiom Alloc_extends_not_assigns_empty: (forall a1:(alloc_table 'a1). (forall a2:(alloc_table 'a1). (forall m1:(memory 'a1 'a2). (forall m2:(memory 'a1 'a2). (forall l:(pset 'a1). (forall p:(pointer 'a1). (forall n:int [(alloc_extends a1 a2), (alloc_fresh a1 p n), (not_assigns a2 m1 m2 l)]. (((alloc_extends a1 a2) /\ ((alloc_fresh a1 p n) /\ ((not_assigns a2 m1 m2 l) /\ (pset_included l (pset_all (pset_singleton p : (pset 'a1)) : (pset 'a1)))))) -> (not_assigns a1 m1 m2 (pset_empty : (pset 'a1))))))))))) predicate alloc_extends_except (alloc_table 'a1) (alloc_table 'a1) (pset 'a1) axiom Alloc_extends_except_offset_min: (forall a1:(alloc_table 'a1). (forall a2:(alloc_table 'a1). (forall l:(pset 'a1) [(alloc_extends_except a1 a2 l)]. ((alloc_extends_except a1 a2 l) -> (forall p:(pointer 'a1). (((valid a1 p) /\ (not (in_pset p l))) -> ((offset_min a1 p : int) = (offset_min a2 p : int)))))))) axiom Alloc_extends_except_offset_max: (forall a1:(alloc_table 'a1). (forall a2:(alloc_table 'a1). (forall l:(pset 'a1) [(alloc_extends_except a1 a2 l)]. ((alloc_extends_except a1 a2 l) -> (forall p:(pointer 'a1). (((valid a1 p) /\ (not (in_pset p l))) -> ((offset_max a1 p : int) = (offset_max a2 p : int)))))))) type bitvector function concat_bitvector bitvector bitvector : bitvector function offset_min_bytes (alloc_table 'a1) (pointer 'a1) int : int function offset_max_bytes (alloc_table 'a1) (pointer 'a1) int : int axiom Offset_min_bytes_def: (forall a:(alloc_table 'a1). (forall p:(pointer 'a1). (forall s:int [(offset_min_bytes a p s : int)]. ((Int.(<) 0 s) -> ((Int.(<=) (offset_min a p : int) (Int.(*) s (offset_min_bytes a p s : int) : int)) /\ (Int.(<) (Int.(-) (Int.(*) s (offset_min_bytes a p s : int) : int) s : int) (offset_min a p : int))))))) axiom Offset_max_bytes_def: (forall a:(alloc_table 'a1). (forall p:(pointer 'a1). (forall s:int [(offset_max_bytes a p s : int)]. ((Int.(<) 0 s) -> ((Int.(<=) (Int.(-) (Int.(+) (Int.(*) s (offset_max_bytes a p s : int) : int) s : int) 1 : int) (offset_max a p : int)) /\ (Int.(<) (offset_max a p : int) (Int.(-) (Int.(+) (Int.(+) (Int.(*) s (offset_max_bytes a p s : int) : int) s : int) s : int) 1 : int))))))) function extract_bytes bitvector int int : bitvector function replace_bytes bitvector int int bitvector : bitvector axiom Select_store_eq_union: (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector [(extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector)]. (((o1 = o2) /\ (s1 = s2)) -> ((extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector) = v2)))))))) axiom Select_store_neq_union: (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector [(extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector)]. (((Int.(<=) (Int.(+) o2 s2 : int) o1) \/ (Int.(<=) (Int.(+) o1 s2 : int) o2)) -> ((extract_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 : bitvector) = (extract_bytes v1 o2 s2 : bitvector))))))))) axiom Concat_replace_bytes_up: (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector. (forall v3:bitvector [(replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector)]. (((Int.(+) o1 s1 : int) = o2) -> ((replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector) = (replace_bytes v1 o1 (Int.(+) s1 s2 : int) (concat_bitvector v2 v3 : bitvector) : bitvector)))))))))) axiom Concat_replace_bytes_down: (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector. (forall v3:bitvector [(replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector)]. (((Int.(+) o2 s2 : int) = o1) -> ((replace_bytes (replace_bytes v1 o1 s1 v2 : bitvector) o2 s2 v3 : bitvector) = (replace_bytes v1 o2 (Int.(+) s1 s2 : int) (concat_bitvector v3 v2 : bitvector) : bitvector)))))))))) axiom Concat_extract_bytes: (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v:bitvector [(concat_bitvector (extract_bytes v o1 s1 : bitvector) (extract_bytes v o2 s2 : bitvector) : bitvector)]. (((Int.(+) o1 s1 : int) = o2) -> ((concat_bitvector (extract_bytes v o1 s1 : bitvector) (extract_bytes v o2 s2 : bitvector) : bitvector) = (extract_bytes v o1 (Int.(+) s1 s2 : int) : bitvector)))))))) function select_bytes (memory 'a1 bitvector) (pointer 'a1) int int : bitvector function store_bytes (memory 'a1 bitvector) (pointer 'a1) int int bitvector : (memory 'a1 bitvector) axiom Select_store_eq_bytes: (forall m:(memory 'a1 bitvector). (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v:bitvector [(select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector)]. (((p1 = p2) /\ ((o1 = o2) /\ (s1 = s2))) -> ((select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector) = v)))))))))) axiom Select_store_neq_bytes: (forall m:(memory 'a1 bitvector). (forall p1:(pointer 'a1). (forall p2:(pointer 'a1). (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v:bitvector [(select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector)]. ((pset_disjoint (pset_range (pset_singleton p1 : (pset 'a1)) o1 (Int.(+) o1 s1 : int) : (pset 'a1)) (pset_range (pset_singleton p2 : (pset 'a1)) o2 (Int.(+) o2 s2 : int) : (pset 'a1))) -> ((select_bytes (store_bytes m p1 o1 s1 v : (memory 'a1 bitvector)) p2 o2 s2 : bitvector) = (select_bytes m p2 o2 s2 : bitvector))))))))))) axiom Shift_store_bytes: (forall m:(memory 'a1 bitvector). (forall p:(pointer 'a1). (forall i:int. (forall o:int. (forall s:int. (forall v:bitvector [(store_bytes m (shift p i : (pointer 'a1)) o s v : (memory 'a1 bitvector))]. ((store_bytes m (shift p i : (pointer 'a1)) o s v : (memory 'a1 bitvector)) = (store_bytes m p (Int.(+) o i : int) s v : (memory 'a1 bitvector))))))))) axiom Shift_select_bytes: (forall m:(memory 'a1 bitvector). (forall p:(pointer 'a1). (forall i:int. (forall o:int. (forall s:int. (forall v:bitvector [(select_bytes m (shift p i : (pointer 'a1)) o s : bitvector)]. ((select_bytes m (shift p i : (pointer 'a1)) o s : bitvector) = (select_bytes m p (Int.(+) o i : int) s : bitvector)))))))) axiom Concat_store_bytes_up: (forall m:(memory 'a1 bitvector). (forall p:(pointer 'a1). (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector [(store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector))]. (((Int.(+) o1 s1 : int) = o2) -> ((store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector)) = (store_bytes m p o1 (Int.(+) s1 s2 : int) (concat_bitvector v1 v2 : bitvector) : (memory 'a1 bitvector)))))))))))) axiom Concat_store_bytes_down: (forall m:(memory 'a1 bitvector). (forall p:(pointer 'a1). (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int. (forall v1:bitvector. (forall v2:bitvector [(store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector))]. (((Int.(+) o2 s2 : int) = o1) -> ((store_bytes (store_bytes m p o1 s1 v1 : (memory 'a1 bitvector)) p o2 s2 v2 : (memory 'a1 bitvector)) = (store_bytes m p o2 (Int.(+) s1 s2 : int) (concat_bitvector v2 v1 : bitvector) : (memory 'a1 bitvector)))))))))))) axiom Concat_select_bytes: (forall m:(memory 'a1 bitvector). (forall p:(pointer 'a1). (forall o1:int. (forall s1:int. (forall o2:int. (forall s2:int [(concat_bitvector (select_bytes m p o1 s1 : bitvector) (select_bytes m p o2 s2 : bitvector) : bitvector)]. (((Int.(+) o1 s1 : int) = o2) -> ((concat_bitvector (select_bytes m p o1 s1 : bitvector) (select_bytes m p o2 s2 : bitvector) : bitvector) = (select_bytes m p o1 (Int.(+) s1 s2 : int) : bitvector))))))))) type char_P type mybag type node type padding type void_P predicate mybag_add (pointer node) mybag mybag predicate in_mybag (pointer node) mybag axiom U_mybag_add: (forall s_1:mybag. (forall t_0:mybag. (forall p_3:(pointer node). ((mybag_add p_3 t_0 s_1) <-> (forall n_1:(pointer node). ((in_mybag n_1 s_1) <-> ((n_1 = p_3) \/ (in_mybag n_1 t_0)))))))) function mybag_all : mybag axiom U_mybag_all: (forall p_2_0:(pointer node). (in_mybag p_2_0 (mybag_all : mybag))) function mybag_empty : mybag axiom U_mybag_empty: (forall p_1_0:(pointer node). (not (in_mybag p_1_0 (mybag_empty : mybag)))) predicate mybag_rem (pointer node) mybag mybag axiom U_mybag_rem: (forall s_3:mybag. (forall t_2:mybag. (forall p_4:(pointer node). ((mybag_rem p_4 t_2 s_3) <-> (forall n_0_0:(pointer node). ((in_mybag n_0_0 s_3) <-> ((n_0_0 <> p_4) /\ (in_mybag n_0_0 t_2)))))))) function bitvector_of_char_P (pointer char_P) : bitvector function char_P_of_bitvector bitvector : (pointer char_P) axiom Bitvector_of_char_P_of_char_P_of_bitvector: (forall x:bitvector. ((bitvector_of_char_P (char_P_of_bitvector x : (pointer char_P)) : bitvector) = x)) function bitvector_of_node (pointer node) : bitvector function node_of_bitvector bitvector : (pointer node) axiom Bitvector_of_node_of_node_of_bitvector: (forall x:bitvector. ((bitvector_of_node (node_of_bitvector x : (pointer node)) : bitvector) = x)) function bitvector_of_void_P (pointer void_P) : bitvector function void_P_of_bitvector bitvector : (pointer void_P) axiom Bitvector_of_void_P_of_void_P_of_bitvector: (forall x:bitvector. ((bitvector_of_void_P (void_P_of_bitvector x : (pointer void_P)) : bitvector) = x)) function char_P_tag : (tag_id char_P) axiom Char_P_int: ((int_of_tag (char_P_tag : (tag_id char_P)) : int) = 1) axiom Char_P_of_bitvector_of_bitvector_of_char_P: (forall x:(pointer char_P). ((char_P_of_bitvector (bitvector_of_char_P x : bitvector) : (pointer char_P)) = x)) function char_P_of_pointer_address (pointer Unit.unit) : (pointer char_P) axiom Char_P_of_pointer_address_of_pointer_addr: (forall p:(pointer char_P). (p = (char_P_of_pointer_address (pointer_address p : (pointer Unit.unit)) : (pointer char_P)))) axiom Char_P_parenttag_bottom: (parenttag (char_P_tag : (tag_id char_P)) (bottom_tag : (tag_id char_P))) axiom Char_P_tags: (forall x:(pointer char_P). (forall char_P_tag_table:(tag_table char_P). (instanceof char_P_tag_table x (char_P_tag : (tag_id char_P))))) predicate ilist (pointer node) (alloc_table node) (memory node (pointer node)) axiom Ilist_inversion: (forall aux_1_0:(pointer node). (forall aux_2_0:(alloc_table node). (forall aux_3_0:(memory node (pointer node)). ((ilist aux_1_0 aux_2_0 aux_3_0) -> ((exists node_alloc_table_at_L:(alloc_table node). (exists node_tl_at_L:(memory node (pointer node)). ((aux_1_0 = (null : (pointer node))) /\ ((aux_2_0 = node_alloc_table_at_L) /\ (aux_3_0 = node_tl_at_L))))) \/ (exists node_alloc_table_at_L:(alloc_table node). (exists node_tl_at_L:(memory node (pointer node)). (exists p_0_0:(pointer node). ((p_0_0 <> (null : (pointer node))) /\ (((Int.(<=) (offset_min node_alloc_table_at_L p_0_0 : int) 0) /\ (Int.(>=) (offset_max node_alloc_table_at_L p_0_0 : int) 0)) /\ ((ilist (select node_tl_at_L p_0_0 : (pointer node)) node_alloc_table_at_L node_tl_at_L) /\ ((aux_1_0 = p_0_0) /\ ((aux_2_0 = node_alloc_table_at_L) /\ (aux_3_0 = node_tl_at_L)))))))))))))) axiom Nil: (forall node_alloc_table_at_L:(alloc_table node). (forall node_tl_at_L:(memory node (pointer node)). (ilist (null : (pointer node)) node_alloc_table_at_L node_tl_at_L))) axiom Cons: (forall node_alloc_table_at_L:(alloc_table node). (forall node_tl_at_L:(memory node (pointer node)). (forall p_0_0:(pointer node). ((p_0_0 <> (null : (pointer node))) -> (((Int.(<=) (offset_min node_alloc_table_at_L p_0_0 : int) 0) /\ (Int.(>=) (offset_max node_alloc_table_at_L p_0_0 : int) 0)) -> ((ilist (select node_tl_at_L p_0_0 : (pointer node)) node_alloc_table_at_L node_tl_at_L) -> (ilist p_0_0 node_alloc_table_at_L node_tl_at_L))))))) predicate ilist_FT (pointer node) (memory node (pointer node)) (memory node (pointer node)) goal Ilist_frame: (forall node_alloc_table_at_L2:(alloc_table node). (forall node_alloc_table_at_L1:(alloc_table node). (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_17:(pointer node). ((ilist_FT p_17 node_tl_at_L2 node_tl_at_L1) -> ((ilist p_17 node_alloc_table_at_L1 node_tl_at_L1) -> (ilist p_17 node_alloc_table_at_L2 node_tl_at_L2)))))))) axiom Ilist_frame_as_axiom: (forall node_alloc_table_at_L2:(alloc_table node). (forall node_alloc_table_at_L1:(alloc_table node). (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_17:(pointer node). ((ilist_FT p_17 node_tl_at_L2 node_tl_at_L1) -> ((ilist p_17 node_alloc_table_at_L1 node_tl_at_L1) -> (ilist p_17 node_alloc_table_at_L2 node_tl_at_L2)))))))) predicate ilist_in_list_notin (pointer node) mybag (memory node (pointer node)) goal Ilist_ilist_in_list_notin_frame: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall s_7:mybag. (forall p_18:(pointer node). ((ilist_FT p_18 node_tl_at_L2 node_tl_at_L1) -> ((ilist_in_list_notin p_18 s_7 node_tl_at_L1) -> (ilist_in_list_notin p_18 s_7 node_tl_at_L2))))))) axiom Ilist_ilist_in_list_notin_frame_as_axiom: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall s_7:mybag. (forall p_18:(pointer node). ((ilist_FT p_18 node_tl_at_L2 node_tl_at_L1) -> ((ilist_in_list_notin p_18 s_7 node_tl_at_L1) -> (ilist_in_list_notin p_18 s_7 node_tl_at_L2))))))) predicate ilist_notin_node (pointer node) (pointer node) (memory node (pointer node)) goal Ilist_ilist_notin_node_frame: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_19:(pointer node). (forall n_3:(pointer node). ((ilist_FT p_19 node_tl_at_L2 node_tl_at_L1) -> ((ilist_notin_node p_19 n_3 node_tl_at_L1) -> (ilist_notin_node p_19 n_3 node_tl_at_L2))))))) axiom Ilist_ilist_notin_node_frame_as_axiom: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_19:(pointer node). (forall n_3:(pointer node). ((ilist_FT p_19 node_tl_at_L2 node_tl_at_L1) -> ((ilist_notin_node p_19 n_3 node_tl_at_L1) -> (ilist_notin_node p_19 n_3 node_tl_at_L2))))))) axiom Ilist_in_list_notin_def1: (forall node_tl_at_L:(memory node (pointer node)). (forall p_6:(pointer node). (forall s_5:mybag. ((p_6 = (null : (pointer node))) -> (ilist_in_list_notin p_6 s_5 node_tl_at_L))))) axiom Ilist_in_list_notin_def2: (forall node_tl_at_L:(memory node (pointer node)). (forall p_7:(pointer node). (forall s_6:mybag. ((ilist_in_list_notin p_7 s_6 node_tl_at_L) <-> ((p_7 <> (null : (pointer node))) -> ((ilist_in_list_notin (select node_tl_at_L p_7 : (pointer node)) s_6 node_tl_at_L) /\ (in_mybag p_7 s_6))))))) axiom Ilist_in_list_notin_def3: (forall node_tl_at_L:(memory node (pointer node)). (forall p_8:(pointer node). (ilist_in_list_notin p_8 (mybag_all : mybag) node_tl_at_L))) function ilist_notin (pointer node) (memory node (pointer node)) : mybag axiom Ilist_notin1: (forall node_tl_at_L:(memory node (pointer node)). (forall p_13:(pointer node). ((p_13 = (null : (pointer node))) -> ((ilist_notin p_13 node_tl_at_L : mybag) = (mybag_all : mybag))))) axiom Ilist_notin2: (forall node_tl_at_L:(memory node (pointer node)). (forall p_14:(pointer node). (forall n_1_0:(pointer node). ((p_14 <> (null : (pointer node))) -> (mybag_rem p_14 (ilist_notin (select node_tl_at_L p_14 : (pointer node)) node_tl_at_L : mybag) (ilist_notin p_14 node_tl_at_L : mybag)))))) axiom Ilist_notin_FT: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_16:(pointer node). ((forall n_2:(pointer node). (((select node_tl_at_L1 n_2 : (pointer node)) <> (select node_tl_at_L2 n_2 : (pointer node))) -> (in_mybag n_2 (ilist_notin p_16 node_tl_at_L1 : mybag)))) -> (ilist_FT p_16 node_tl_at_L2 node_tl_at_L1))))) goal Ilist_notin_frame: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_20:(pointer node). ((ilist_FT p_20 node_tl_at_L2 node_tl_at_L1) -> ((ilist_notin p_20 node_tl_at_L1 : mybag) = (ilist_notin p_20 node_tl_at_L2 : mybag)))))) axiom Ilist_notin_frame_as_axiom: (forall node_tl_at_L2:(memory node (pointer node)). (forall node_tl_at_L1:(memory node (pointer node)). (forall p_20:(pointer node). ((ilist_FT p_20 node_tl_at_L2 node_tl_at_L1) -> ((ilist_notin p_20 node_tl_at_L1 : mybag) = (ilist_notin p_20 node_tl_at_L2 : mybag)))))) axiom Ilist_notin_node_def1: (forall node_tl_at_L:(memory node (pointer node)). (forall p_10:(pointer node). (forall q_0_0:(pointer node). ((p_10 = (null : (pointer node))) -> (ilist_notin_node p_10 q_0_0 node_tl_at_L))))) axiom Ilist_notin_node_def2: (forall node_tl_at_L:(memory node (pointer node)). (forall p_11:(pointer node). (forall q_1_0:(pointer node). ((p_11 <> (null : (pointer node))) -> ((ilist_notin_node p_11 q_1_0 node_tl_at_L) <-> ((ilist_notin_node (select node_tl_at_L p_11 : (pointer node)) q_1_0 node_tl_at_L) /\ (p_11 <> q_1_0))))))) predicate inc_ilist_ilist (pointer node) (pointer node) (memory node (pointer node)) axiom Inc_ilist_ilist_def: (forall p1_0:(pointer node). (forall p2_0:(pointer node). (forall node_tl_at_L0:(memory node (pointer node)). ((inc_ilist_ilist p1_0 p2_0 node_tl_at_L0) <-> (ilist_in_list_notin p1_0 (ilist_notin p2_0 node_tl_at_L0 : mybag) node_tl_at_L0))))) predicate left_valid_struct_char_P (pointer char_P) int (alloc_table char_P) axiom Left_valid_struct_char_P_def: (forall p0:(pointer char_P). (forall a0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((left_valid_struct_char_P p0 a0 char_P_alloc_table0) <-> (Int.(<=) (offset_min char_P_alloc_table0 p0 : int) a0))))) predicate left_valid_struct_node (pointer node) int (alloc_table node) axiom Left_valid_struct_node_def: (forall p0:(pointer node). (forall a0:int. (forall node_alloc_table0:(alloc_table node). ((left_valid_struct_node p0 a0 node_alloc_table0) <-> (Int.(<=) (offset_min node_alloc_table0 p0 : int) a0))))) predicate left_valid_struct_void_P (pointer void_P) int (alloc_table void_P) axiom Left_valid_struct_void_P_def: (forall p0:(pointer void_P). (forall a0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((left_valid_struct_void_P p0 a0 void_P_alloc_table0) <-> (Int.(<=) (offset_min void_P_alloc_table0 p0 : int) a0))))) predicate sep_node_ilist (pointer node) (pointer node) (memory node (pointer node)) axiom Sep_node_ilist_def: (forall n_4_0:(pointer node). (forall p_21_0:(pointer node). (forall node_tl_at_L0:(memory node (pointer node)). ((sep_node_ilist n_4_0 p_21_0 node_tl_at_L0) <-> ((in_mybag n_4_0 (ilist_notin p_21_0 node_tl_at_L0 : mybag)) /\ (ilist_notin_node p_21_0 n_4_0 node_tl_at_L0)))))) goal List_sep: (forall node_alloc_table_at_L:(alloc_table node). (forall node_tl_at_L:(memory node (pointer node)). (forall p_22:(pointer node). ((ilist p_22 node_alloc_table_at_L node_tl_at_L) -> (sep_node_ilist p_22 (select node_tl_at_L p_22 : (pointer node)) node_tl_at_L))))) axiom List_sep_as_axiom: (forall node_alloc_table_at_L:(alloc_table node). (forall node_tl_at_L:(memory node (pointer node)). (forall p_22:(pointer node). ((ilist p_22 node_alloc_table_at_L node_tl_at_L) -> (sep_node_ilist p_22 (select node_tl_at_L p_22 : (pointer node)) node_tl_at_L))))) function node_tag : (tag_id node) axiom Node_int: ((int_of_tag (node_tag : (tag_id node)) : int) = 1) axiom Node_of_bitvector_of_bitvector_of_node: (forall x:(pointer node). ((node_of_bitvector (bitvector_of_node x : bitvector) : (pointer node)) = x)) function node_of_pointer_address (pointer Unit.unit) : (pointer node) axiom Node_of_pointer_address_of_pointer_addr: (forall p:(pointer node). (p = (node_of_pointer_address (pointer_address p : (pointer Unit.unit)) : (pointer node)))) axiom Node_parenttag_bottom: (parenttag (node_tag : (tag_id node)) (bottom_tag : (tag_id node))) axiom Node_tags: (forall x:(pointer node). (forall node_tag_table:(tag_table node). (instanceof node_tag_table x (node_tag : (tag_id node))))) axiom Pointer_addr_of_char_P_of_pointer_address: (forall p:(pointer Unit.unit). (p = (pointer_address (char_P_of_pointer_address p : (pointer char_P)) : (pointer Unit.unit)))) axiom Pointer_addr_of_node_of_pointer_address: (forall p:(pointer Unit.unit). (p = (pointer_address (node_of_pointer_address p : (pointer node)) : (pointer Unit.unit)))) function void_P_of_pointer_address (pointer Unit.unit) : (pointer void_P) axiom Pointer_addr_of_void_P_of_pointer_address: (forall p:(pointer Unit.unit). (p = (pointer_address (void_P_of_pointer_address p : (pointer void_P)) : (pointer Unit.unit)))) predicate right_valid_struct_char_P (pointer char_P) int (alloc_table char_P) axiom Right_valid_struct_char_P_def: (forall p0:(pointer char_P). (forall b0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((right_valid_struct_char_P p0 b0 char_P_alloc_table0) <-> (Int.(>=) (offset_max char_P_alloc_table0 p0 : int) b0))))) predicate right_valid_struct_node (pointer node) int (alloc_table node) axiom Right_valid_struct_node_def: (forall p0:(pointer node). (forall b0:int. (forall node_alloc_table0:(alloc_table node). ((right_valid_struct_node p0 b0 node_alloc_table0) <-> (Int.(>=) (offset_max node_alloc_table0 p0 : int) b0))))) predicate right_valid_struct_void_P (pointer void_P) int (alloc_table void_P) axiom Right_valid_struct_void_P_def: (forall p0:(pointer void_P). (forall b0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((right_valid_struct_void_P p0 b0 void_P_alloc_table0) <-> (Int.(>=) (offset_max void_P_alloc_table0 p0 : int) b0))))) predicate sep_ilist_ilist (pointer node) (pointer node) (memory node (pointer node)) axiom Sep_ilist_ilist_def: (forall p1_0_0:(pointer node). (forall p2_0_0:(pointer node). (forall node_tl_at_L0:(memory node (pointer node)). ((sep_ilist_ilist p1_0_0 p2_0_0 node_tl_at_L0) <-> ((inc_ilist_ilist p1_0_0 p2_0_0 node_tl_at_L0) /\ (inc_ilist_ilist p2_0_0 p1_0_0 node_tl_at_L0)))))) predicate strict_valid_root_char_P (pointer char_P) int int (alloc_table char_P) axiom Strict_valid_root_char_P_def: (forall p0:(pointer char_P). (forall a0:int. (forall b0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((strict_valid_root_char_P p0 a0 b0 char_P_alloc_table0) <-> (((offset_min char_P_alloc_table0 p0 : int) = a0) /\ ((offset_max char_P_alloc_table0 p0 : int) = b0))))))) predicate strict_valid_root_node (pointer node) int int (alloc_table node) axiom Strict_valid_root_node_def: (forall p0:(pointer node). (forall a0:int. (forall b0:int. (forall node_alloc_table0:(alloc_table node). ((strict_valid_root_node p0 a0 b0 node_alloc_table0) <-> (((offset_min node_alloc_table0 p0 : int) = a0) /\ ((offset_max node_alloc_table0 p0 : int) = b0))))))) predicate strict_valid_root_void_P (pointer void_P) int int (alloc_table void_P) axiom Strict_valid_root_void_P_def: (forall p0:(pointer void_P). (forall a0:int. (forall b0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((strict_valid_root_void_P p0 a0 b0 void_P_alloc_table0) <-> (((offset_min void_P_alloc_table0 p0 : int) = a0) /\ ((offset_max void_P_alloc_table0 p0 : int) = b0))))))) predicate strict_valid_struct_char_P (pointer char_P) int int (alloc_table char_P) axiom Strict_valid_struct_char_P_def: (forall p0:(pointer char_P). (forall a0:int. (forall b0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((strict_valid_struct_char_P p0 a0 b0 char_P_alloc_table0) <-> (((offset_min char_P_alloc_table0 p0 : int) = a0) /\ ((offset_max char_P_alloc_table0 p0 : int) = b0))))))) predicate strict_valid_struct_node (pointer node) int int (alloc_table node) axiom Strict_valid_struct_node_def: (forall p0:(pointer node). (forall a0:int. (forall b0:int. (forall node_alloc_table0:(alloc_table node). ((strict_valid_struct_node p0 a0 b0 node_alloc_table0) <-> (((offset_min node_alloc_table0 p0 : int) = a0) /\ ((offset_max node_alloc_table0 p0 : int) = b0))))))) predicate strict_valid_struct_void_P (pointer void_P) int int (alloc_table void_P) axiom Strict_valid_struct_void_P_def: (forall p0:(pointer void_P). (forall a0:int. (forall b0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((strict_valid_struct_void_P p0 a0 b0 void_P_alloc_table0) <-> (((offset_min void_P_alloc_table0 p0 : int) = a0) /\ ((offset_max void_P_alloc_table0 p0 : int) = b0))))))) predicate valid_bitvector_struct_char_P (pointer Unit.unit) int int (alloc_table Unit.unit) axiom Valid_bitvector_struct_char_P_def: (forall p0:(pointer Unit.unit). (forall a0:int. (forall b0:int. (forall bitvector_alloc_table0:(alloc_table Unit.unit). ((valid_bitvector_struct_char_P p0 a0 b0 bitvector_alloc_table0) <-> (((offset_min bitvector_alloc_table0 p0 : int) = a0) /\ ((offset_max bitvector_alloc_table0 p0 : int) = b0))))))) predicate valid_bitvector_struct_node (pointer Unit.unit) int int (alloc_table Unit.unit) axiom Valid_bitvector_struct_node_def: (forall p0:(pointer Unit.unit). (forall a0:int. (forall b0:int. (forall bitvector_alloc_table0:(alloc_table Unit.unit). ((valid_bitvector_struct_node p0 a0 b0 bitvector_alloc_table0) <-> (((offset_min bitvector_alloc_table0 p0 : int) = a0) /\ ((offset_max bitvector_alloc_table0 p0 : int) = b0))))))) predicate valid_bitvector_struct_void_P (pointer Unit.unit) int int (alloc_table Unit.unit) axiom Valid_bitvector_struct_void_P_def: (forall p0:(pointer Unit.unit). (forall a0:int. (forall b0:int. (forall bitvector_alloc_table0:(alloc_table Unit.unit). ((valid_bitvector_struct_void_P p0 a0 b0 bitvector_alloc_table0) <-> (((offset_min bitvector_alloc_table0 p0 : int) = a0) /\ ((offset_max bitvector_alloc_table0 p0 : int) = b0))))))) predicate valid_root_char_P (pointer char_P) int int (alloc_table char_P) axiom Valid_root_char_P_def: (forall p0:(pointer char_P). (forall a0:int. (forall b0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((valid_root_char_P p0 a0 b0 char_P_alloc_table0) <-> ((Int.(<=) (offset_min char_P_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max char_P_alloc_table0 p0 : int) b0))))))) predicate valid_root_node (pointer node) int int (alloc_table node) axiom Valid_root_node_def: (forall p0:(pointer node). (forall a0:int. (forall b0:int. (forall node_alloc_table0:(alloc_table node). ((valid_root_node p0 a0 b0 node_alloc_table0) <-> ((Int.(<=) (offset_min node_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max node_alloc_table0 p0 : int) b0))))))) predicate valid_root_void_P (pointer void_P) int int (alloc_table void_P) axiom Valid_root_void_P_def: (forall p0:(pointer void_P). (forall a0:int. (forall b0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((valid_root_void_P p0 a0 b0 void_P_alloc_table0) <-> ((Int.(<=) (offset_min void_P_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max void_P_alloc_table0 p0 : int) b0))))))) predicate valid_struct_char_P (pointer char_P) int int (alloc_table char_P) axiom Valid_struct_char_P_def: (forall p0:(pointer char_P). (forall a0:int. (forall b0:int. (forall char_P_alloc_table0:(alloc_table char_P). ((valid_struct_char_P p0 a0 b0 char_P_alloc_table0) <-> ((Int.(<=) (offset_min char_P_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max char_P_alloc_table0 p0 : int) b0))))))) predicate valid_struct_node (pointer node) int int (alloc_table node) axiom Valid_struct_node_def: (forall p0:(pointer node). (forall a0:int. (forall b0:int. (forall node_alloc_table0:(alloc_table node). ((valid_struct_node p0 a0 b0 node_alloc_table0) <-> ((Int.(<=) (offset_min node_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max node_alloc_table0 p0 : int) b0))))))) predicate valid_struct_void_P (pointer void_P) int int (alloc_table void_P) axiom Valid_struct_void_P_def: (forall p0:(pointer void_P). (forall a0:int. (forall b0:int. (forall void_P_alloc_table0:(alloc_table void_P). ((valid_struct_void_P p0 a0 b0 void_P_alloc_table0) <-> ((Int.(<=) (offset_min void_P_alloc_table0 p0 : int) a0) /\ (Int.(>=) (offset_max void_P_alloc_table0 p0 : int) b0))))))) function void_P_tag : (tag_id void_P) axiom Void_P_int: ((int_of_tag (void_P_tag : (tag_id void_P)) : int) = 1) axiom Void_P_of_bitvector_of_bitvector_of_void_P: (forall x:(pointer void_P). ((void_P_of_bitvector (bitvector_of_void_P x : bitvector) : (pointer void_P)) = x)) axiom Void_P_of_pointer_address_of_pointer_addr: (forall p:(pointer void_P). (p = (void_P_of_pointer_address (pointer_address p : (pointer Unit.unit)) : (pointer void_P)))) axiom Void_P_parenttag_bottom: (parenttag (void_P_tag : (tag_id void_P)) (bottom_tag : (tag_id void_P))) axiom Void_P_tags: (forall x:(pointer void_P). (forall void_P_tag_table:(tag_table void_P). (instanceof void_P_tag_table x (void_P_tag : (tag_id void_P))))) goal Inconsistent_ensures_default_po_1: (forall p_2:(pointer node). (forall q_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_64" (("JC_60" (ilist p_2 node_alloc_table node_tl)) /\ (("JC_61" (ilist q_1 node_alloc_table node_tl)) /\ (("JC_62" (inc_ilist_ilist p_2 q_1 node_tl)) /\ ("JC_63" (p_2 <> (null : (pointer node))))))))) -> (forall node_tl0:(memory node (pointer node)). ((node_tl0 = (store node_tl p_2 q_1 : (memory node (pointer node)))) -> ("JC_66" (Bool.ffalse = Bool.ttrue))))))))) goal Inconsistent_safety_po_1: (forall p_2:(pointer node). (forall q_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (("JC_64" (("JC_60" (ilist p_2 node_alloc_table node_tl)) /\ (("JC_61" (ilist q_1 node_alloc_table node_tl)) /\ (("JC_62" (inc_ilist_ilist p_2 q_1 node_tl)) /\ ("JC_63" (p_2 <> (null : (pointer node)))))))) -> (Int.(<=) (offset_min node_alloc_table p_2 : int) 0)))))) goal Inconsistent_safety_po_2: (forall p_2:(pointer node). (forall q_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (("JC_64" (("JC_60" (ilist p_2 node_alloc_table node_tl)) /\ (("JC_61" (ilist q_1 node_alloc_table node_tl)) /\ (("JC_62" (inc_ilist_ilist p_2 q_1 node_tl)) /\ ("JC_63" (p_2 <> (null : (pointer node)))))))) -> (Int.(<=) 0 (offset_max node_alloc_table p_2 : int))))))) goal Rev_ensures_default_po_1: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> ("JC_41" ("JC_39" ("JC_39" (ilist q_1_1 node_alloc_table node_tl)))))))))) goal Rev_ensures_default_po_2: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> ("JC_41" ("JC_40" ("JC_40" (inc_ilist_ilist p_1 q_1_1 node_tl)))))))))) goal Rev_ensures_default_po_3: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> ("JC_47" ("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)))))))))))))))))) goal Rev_ensures_default_po_4: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> ("JC_50" ("JC_48" ("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)))))))))))))))))))) goal Rev_ensures_default_po_5: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> ("JC_50" ("JC_49" ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))))))))))))))))))) goal Rev_ensures_default_po_6: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> ("JC_51" ("JC_51" (ilist_FT tmp node_tl1 node_tl0)))))))))))))))))))))))))) goal Rev_ensures_default_po_7: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> (("JC_51" (ilist_FT tmp node_tl1 node_tl0)) -> ("JC_52" ("JC_52" (ilist_FT q_1_1_0 node_tl1 node_tl0))))))))))))))))))))))))))) goal Rev_ensures_default_po_8: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> (("JC_51" (ilist_FT tmp node_tl1 node_tl0)) -> (("JC_52" (ilist_FT q_1_1_0 node_tl1 node_tl0)) -> ("JC_53" ("JC_53" (ilist q_1_1_0 node_alloc_table node_tl1)))))))))))))))))))))))))))) goal Rev_ensures_default_po_9: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> (("JC_51" (ilist_FT tmp node_tl1 node_tl0)) -> (("JC_52" (ilist_FT q_1_1_0 node_tl1 node_tl0)) -> (("JC_53" (ilist q_1_1_0 node_alloc_table node_tl1)) -> (forall q_1_1_1:(pointer node). ((q_1_1_1 = mutable_p_1) -> (forall mutable_p_1_0:(pointer node). ((mutable_p_1_0 = tmp) -> ("JC_41" ("JC_38" ("JC_38" (ilist mutable_p_1_0 node_alloc_table node_tl1)))))))))))))))))))))))))))))))))) goal Rev_ensures_default_po_10: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> (("JC_51" (ilist_FT tmp node_tl1 node_tl0)) -> (("JC_52" (ilist_FT q_1_1_0 node_tl1 node_tl0)) -> (("JC_53" (ilist q_1_1_0 node_alloc_table node_tl1)) -> (forall q_1_1_1:(pointer node). ((q_1_1_1 = mutable_p_1) -> (forall mutable_p_1_0:(pointer node). ((mutable_p_1_0 = tmp) -> ("JC_41" ("JC_39" ("JC_39" (ilist q_1_1_1 node_alloc_table node_tl1)))))))))))))))))))))))))))))))))) goal Rev_ensures_default_po_11: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_47" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_50" (("JC_48" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_49" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (forall result0:(pointer node). ((result0 = (select node_tl0 mutable_p_1 : (pointer node))) -> (forall tmp:(pointer node). ((tmp = result0) -> (forall node_tl1:(memory node (pointer node)). ((node_tl1 = (store node_tl0 mutable_p_1 q_1_1_0 : (memory node (pointer node)))) -> (("JC_51" (ilist_FT tmp node_tl1 node_tl0)) -> (("JC_52" (ilist_FT q_1_1_0 node_tl1 node_tl0)) -> (("JC_53" (ilist q_1_1_0 node_alloc_table node_tl1)) -> (forall q_1_1_1:(pointer node). ((q_1_1_1 = mutable_p_1) -> (forall mutable_p_1_0:(pointer node). ((mutable_p_1_0 = tmp) -> ("JC_41" ("JC_40" ("JC_40" (inc_ilist_ilist mutable_p_1_0 q_1_1_1 node_tl1)))))))))))))))))))))))))))))))))) goal Rev_ensures_default_po_12: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (((Bool.ttrue = Bool.ttrue) /\ ("JC_13" (ilist p_1 node_alloc_table node_tl))) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_41" (("JC_38" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_39" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_40" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 = 0) -> (forall return:(pointer node). ((return = q_1_1_0) -> ("JC_15" (ilist return node_alloc_table node_tl0))))))))))))))))))) goal Rev_safety_po_1: (forall p_1:(pointer node). (forall node_alloc_table:(alloc_table node). (forall node_tl:(memory node (pointer node)). (("JC_13" (ilist p_1 node_alloc_table node_tl)) -> (forall q_1_1:(pointer node). ((q_1_1 = (null : (pointer node))) -> (forall mutable_p_1:(pointer node). (forall node_tl0:(memory node (pointer node)). (forall q_1_1_0:(pointer node). (("JC_24" true) -> (("JC_22" (("JC_19" (ilist mutable_p_1 node_alloc_table node_tl0)) /\ (("JC_20" (ilist q_1_1_0 node_alloc_table node_tl0)) /\ ("JC_21" (inc_ilist_ilist mutable_p_1 q_1_1_0 node_tl0))))) -> (forall result:int. (((Bool.ttrue = Bool.ttrue) -> ("JC_7" (if (neq_int_bool result 0 : Bool.bool) = Bool.ttrue then (mutable_p_1 <> (null : (pointer node))) else (mutable_p_1 = (null : (pointer node)))))) -> (forall tmp_0:int. ((tmp_0 = result) -> ((tmp_0 <> 0) -> (("JC_28" (ilist (select node_tl0 mutable_p_1 : (pointer node)) node_alloc_table node_tl0)) -> (("JC_31" (("JC_29" (Int.(<=) (offset_min node_alloc_table mutable_p_1 : int) 0)) /\ ("JC_30" (Int.(>=) (offset_max node_alloc_table mutable_p_1 : int) 0)))) -> (Int.(<=) 0 (offset_max node_alloc_table mutable_p_1 : int)))))))))))))))))))) end