//
// Translation of Viper program.
//
// Date: 2024-07-11 15:14:43
// Tool: carbon 1.0
// Arguments: : /Users/jkai/Dropbox/SURE-2024/ViperScratchpad/arrayTestChainIrrel3.vpr --print /Users/jkai/ViperTests/arrayTestChainIrrel3.bpl --boogieExe /Users/jkai/.dotnet/tools/boogie --boogieOpt /vcsCores:1 --timeout 1 --z3Exe /opt/homebrew/bin/z3
// Dependencies:
// Boogie , located at /Users/jkai/.dotnet/tools/boogie.
// Z3 4.13.0 - 64 bit, located at /opt/homebrew/bin/z3.
//
// ==================================================
// Preamble of State module.
// ==================================================
function state(Heap: HeapType, Mask: MaskType): bool;
axiom state(dummyHeap, ZeroMask);
// ==================================================
// Preamble of Heap module.
// ==================================================
type Ref;
var Heap: HeapType;
const null: Ref;
type Field A B;
type NormalField;
const dummyHeap: HeapType;
type HeapType = [Ref, Field A B]B;
const unique $allocated: Field NormalField bool;
axiom (forall o: Ref, f: (Field NormalField Ref), Heap: HeapType ::
{ Heap[o, f] }
Heap[o, $allocated] ==> Heap[Heap[o, f], $allocated]
);
function succHeap(Heap0: HeapType, Heap1: HeapType): bool;
function succHeapTrans(Heap0: HeapType, Heap1: HeapType): bool;
function IdenticalOnKnownLocations(Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType): bool;
function IsPredicateField(f_1: (Field A B)): bool;
function IsWandField(f_1: (Field A B)): bool;
function getPredWandId(f_1: (Field A B)): int;
// Frame all locations with direct permissions
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, o_1: Ref, f_2: (Field A B) ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), ExhaleHeap[o_1, f_2] }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, o_1, f_2) ==> Heap[o_1, f_2] == ExhaleHeap[o_1, f_2]
);
// Frame all predicate mask locations of predicates with direct permission
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsPredicateField(pm_f), ExhaleHeap[null, PredicateMaskField(pm_f)] }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsPredicateField(pm_f) ==> Heap[null, PredicateMaskField(pm_f)] == ExhaleHeap[null, PredicateMaskField(pm_f)]
);
// Frame all locations with known folded permissions
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsPredicateField(pm_f) }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsPredicateField(pm_f) ==> (forall o2: Ref, f_2: (Field A B) ::
{ ExhaleHeap[o2, f_2] }
Heap[null, PredicateMaskField(pm_f)][o2, f_2] ==> Heap[o2, f_2] == ExhaleHeap[o2, f_2]
)
);
// Frame all wand mask locations of wands with direct permission
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsWandField(pm_f), ExhaleHeap[null, WandMaskField(pm_f)] }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsWandField(pm_f) ==> Heap[null, WandMaskField(pm_f)] == ExhaleHeap[null, WandMaskField(pm_f)]
);
// Frame all locations in the footprint of magic wands
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsWandField(pm_f) }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsWandField(pm_f) ==> (forall o2: Ref, f_2: (Field A B) ::
{ ExhaleHeap[o2, f_2] }
Heap[null, WandMaskField(pm_f)][o2, f_2] ==> Heap[o2, f_2] == ExhaleHeap[o2, f_2]
)
);
// All previously-allocated references are still allocated
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, o_1: Ref ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), ExhaleHeap[o_1, $allocated] }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> Heap[o_1, $allocated] ==> ExhaleHeap[o_1, $allocated]
);
// Updated Heaps are Successor Heaps
axiom (forall Heap: HeapType, o: Ref, f_3: (Field A B), v: B ::
{ Heap[o, f_3:=v] }
succHeap(Heap, Heap[o, f_3:=v])
);
// IdenticalOnKnownLocations Heaps are Successor Heaps
axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType ::
{ IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) }
IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> succHeap(Heap, ExhaleHeap)
);
// Successor Heaps are Transitive Successor Heaps
axiom (forall Heap0: HeapType, Heap1: HeapType ::
{ succHeap(Heap0, Heap1) }
succHeap(Heap0, Heap1) ==> succHeapTrans(Heap0, Heap1)
);
// Transitivity of Transitive Successor Heaps
axiom (forall Heap0: HeapType, Heap1: HeapType, Heap2: HeapType ::
{ succHeapTrans(Heap0, Heap1), succHeap(Heap1, Heap2) }
succHeapTrans(Heap0, Heap1) && succHeap(Heap1, Heap2) ==> succHeapTrans(Heap0, Heap2)
);
// ==================================================
// Preamble of Permission module.
// ==================================================
type Perm = real;
type MaskType = [Ref, Field A B]Perm;
var Mask: MaskType;
const ZeroMask: MaskType;
axiom (forall o_2: Ref, f_4: (Field A B) ::
{ ZeroMask[o_2, f_4] }
ZeroMask[o_2, f_4] == NoPerm
);
type PMaskType = [Ref, Field A B]bool;
const ZeroPMask: PMaskType;
axiom (forall o_2: Ref, f_4: (Field A B) ::
{ ZeroPMask[o_2, f_4] }
!ZeroPMask[o_2, f_4]
);
function PredicateMaskField(f_5: (Field A FrameType)): Field A PMaskType;
function WandMaskField(f_5: (Field A FrameType)): Field A PMaskType;
const NoPerm: Perm;
axiom NoPerm == 0.000000000;
const FullPerm: Perm;
axiom FullPerm == 1.000000000;
function Perm(a: real, b: real): Perm;
function GoodMask(Mask: MaskType): bool;
axiom (forall Heap: HeapType, Mask: MaskType ::
{ state(Heap, Mask) }
state(Heap, Mask) ==> GoodMask(Mask)
);
axiom (forall Mask: MaskType, o_2: Ref, f_4: (Field A B) ::
{ GoodMask(Mask), Mask[o_2, f_4] }
GoodMask(Mask) ==> Mask[o_2, f_4] >= NoPerm && ((GoodMask(Mask) && !IsPredicateField(f_4)) && !IsWandField(f_4) ==> Mask[o_2, f_4] <= FullPerm)
);
function HasDirectPerm(Mask: MaskType, o_2: Ref, f_4: (Field A B)): bool;
axiom (forall Mask: MaskType, o_2: Ref, f_4: (Field A B) ::
{ HasDirectPerm(Mask, o_2, f_4) }
HasDirectPerm(Mask, o_2, f_4) <==> Mask[o_2, f_4] > NoPerm
);
function sumMask(ResultMask: MaskType, SummandMask1: MaskType, SummandMask2: MaskType): bool;
axiom (forall ResultMask: MaskType, SummandMask1: MaskType, SummandMask2: MaskType, o_2: Ref, f_4: (Field A B) ::
{ sumMask(ResultMask, SummandMask1, SummandMask2), ResultMask[o_2, f_4] } { sumMask(ResultMask, SummandMask1, SummandMask2), SummandMask1[o_2, f_4] } { sumMask(ResultMask, SummandMask1, SummandMask2), SummandMask2[o_2, f_4] }
sumMask(ResultMask, SummandMask1, SummandMask2) ==> ResultMask[o_2, f_4] == SummandMask1[o_2, f_4] + SummandMask2[o_2, f_4]
);
// ==================================================
// Function for trigger used in checks which are never triggered
// ==================================================
function neverTriggered1(__ind_4: int): bool;
function neverTriggered2(__ind_6: int): bool;
function neverTriggered3(__ind_9: int): bool;
function neverTriggered4(__ind_10: int): bool;
function neverTriggered5(__ind_11: int): bool;
function neverTriggered6(__ind_12: int): bool;
function neverTriggered7(__ind_13: int): bool;
function neverTriggered8(__ind_3: int): bool;
function neverTriggered9(j_1: int): bool;
function neverTriggered10(__ind_2: int): bool;
function neverTriggered11(__ind_3: int): bool;
function neverTriggered12(__ind_7: int): bool;
function neverTriggered13(__ind_8: int): bool;
function neverTriggered14(__ind_12: int): bool;
function neverTriggered15(__ind_13: int): bool;
function neverTriggered16(__ind_17: int): bool;
function neverTriggered17(__ind_18: int): bool;
function neverTriggered18(__ind_22: int): bool;
function neverTriggered19(__ind_23: int): bool;
function neverTriggered20(__ind_27: int): bool;
function neverTriggered21(__ind_28: int): bool;
function neverTriggered22(__ind_32: int): bool;
function neverTriggered23(__ind_33: int): bool;
function neverTriggered24(__ind_37: int): bool;
function neverTriggered25(__ind_38: int): bool;
function neverTriggered26(__ind_42: int): bool;
function neverTriggered27(__ind_43: int): bool;
function neverTriggered28(__ind_45: int): bool;
function neverTriggered29(__ind_46: int): bool;
// ==================================================
// Functions used as inverse of receiver expressions in quantified permissions during inhale and exhale
// ==================================================
function invRecv1(recv: Ref): int;
function invRecv2(recv: Ref): int;
function invRecv3(recv: Ref): int;
function invRecv4(recv: Ref): int;
function invRecv5(recv: Ref): int;
function invRecv6(recv: Ref): int;
function invRecv7(recv: Ref): int;
function invRecv8(recv: Ref): int;
function invRecv9(recv: Ref): int;
function invRecv10(recv: Ref): int;
function invRecv11(recv: Ref): int;
function invRecv12(recv: Ref): int;
function invRecv13(recv: Ref): int;
function invRecv14(recv: Ref): int;
function invRecv15(recv: Ref): int;
function invRecv16(recv: Ref): int;
function invRecv17(recv: Ref): int;
function invRecv18(recv: Ref): int;
function invRecv19(recv: Ref): int;
function invRecv20(recv: Ref): int;
function invRecv21(recv: Ref): int;
function invRecv22(recv: Ref): int;
function invRecv23(recv: Ref): int;
function invRecv24(recv: Ref): int;
function invRecv25(recv: Ref): int;
function invRecv26(recv: Ref): int;
function invRecv27(recv: Ref): int;
function invRecv28(recv: Ref): int;
function invRecv29(recv: Ref): int;
// ==================================================
// Functions used to represent the range of the projection of each QP instance onto its receiver expressions for quantified permissions during inhale and exhale
// ==================================================
function qpRange1(recv: Ref): bool;
function qpRange2(recv: Ref): bool;
function qpRange3(recv: Ref): bool;
function qpRange4(recv: Ref): bool;
function qpRange5(recv: Ref): bool;
function qpRange6(recv: Ref): bool;
function qpRange7(recv: Ref): bool;
function qpRange8(recv: Ref): bool;
function qpRange9(recv: Ref): bool;
function qpRange10(recv: Ref): bool;
function qpRange11(recv: Ref): bool;
function qpRange12(recv: Ref): bool;
function qpRange13(recv: Ref): bool;
function qpRange14(recv: Ref): bool;
function qpRange15(recv: Ref): bool;
function qpRange16(recv: Ref): bool;
function qpRange17(recv: Ref): bool;
function qpRange18(recv: Ref): bool;
function qpRange19(recv: Ref): bool;
function qpRange20(recv: Ref): bool;
function qpRange21(recv: Ref): bool;
function qpRange22(recv: Ref): bool;
function qpRange23(recv: Ref): bool;
function qpRange24(recv: Ref): bool;
function qpRange25(recv: Ref): bool;
function qpRange26(recv: Ref): bool;
function qpRange27(recv: Ref): bool;
function qpRange28(recv: Ref): bool;
function qpRange29(recv: Ref): bool;
// ==================================================
// Preamble of Function and predicate module.
// ==================================================
// Function heights (higher height means its body is available earlier):
// - height 1: __snap_Int_Int_Int_val_prime
// - height 0: __snap_Int_Int_Int_val
const AssumeFunctionsAbove: int;
// Declarations for function framing
type FrameType;
const EmptyFrame: FrameType;
function FrameFragment(t: T): FrameType;
function ConditionalFrame(p: Perm, f_6: FrameType): FrameType;
function dummyFunction(t: T): bool;
function CombineFrames(a_1: FrameType, b_1: FrameType): FrameType;
// ==================================================
// Definition of conditional frame fragments
// ==================================================
axiom (forall p: Perm, f_6: FrameType ::
{ ConditionalFrame(p, f_6) }
ConditionalFrame(p, f_6) == (if p > 0.000000000 then f_6 else EmptyFrame)
);
// Function for recording enclosure of one predicate instance in another
function InsidePredicate(p: (Field A FrameType), v_1: FrameType, q: (Field B FrameType), w: FrameType): bool;
// Transitivity of InsidePredicate
axiom (forall p: (Field A FrameType), v_1: FrameType, q: (Field B FrameType), w: FrameType, r: (Field C FrameType), u: FrameType ::
{ InsidePredicate(p, v_1, q, w), InsidePredicate(q, w, r, u) }
InsidePredicate(p, v_1, q, w) && InsidePredicate(q, w, r, u) ==> InsidePredicate(p, v_1, r, u)
);
// Knowledge that two identical instances of the same predicate cannot be inside each other
axiom (forall p: (Field A FrameType), v_1: FrameType, w: FrameType ::
{ InsidePredicate(p, v_1, p, w) }
!InsidePredicate(p, v_1, p, w)
);
// ==================================================
// Preamble of Set module.
// ==================================================
type Set T = [T]bool;
function Set#Card(Set T): int;
axiom (forall s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
function Set#Empty(): Set T;
axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
axiom (forall s: Set T :: { Set#Card(s) }
(Set#Card(s) == 0 <==> s == Set#Empty()) &&
(Set#Card(s) != 0 ==> (exists x: T :: s[x])));
function Set#Singleton(T): Set T;
axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
axiom (forall r: T :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1);
function Set#UnionOne(Set T, T): Set T;
axiom (forall a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
Set#UnionOne(a,x)[o] <==> o == x || a[o]);
axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) }
Set#UnionOne(a, x)[x]);
axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
a[y] ==> Set#UnionOne(a, x)[y]);
axiom (forall a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
axiom (forall a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
!a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
function Set#Union(Set T, Set T): Set T;
axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
Set#Union(a,b)[o] <==> a[o] || b[o]);
axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] }
a[y] ==> Set#Union(a, b)[y]);
axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), b[y] }
b[y] ==> Set#Union(a, b)[y]);
//axiom (forall a, b: Set T :: { Set#Union(a, b) }
// Set#Disjoint(a, b) ==>
// Set#Difference(Set#Union(a, b), a) == b &&
// Set#Difference(Set#Union(a, b), b) == a);
function Set#Intersection(Set T, Set T): Set T;
axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } {Set#Intersection(a,b), a[o]} {Set#Intersection(a,b), b[o]} // AS: added alternative triggers 20/06/19
Set#Intersection(a,b)[o] <==> a[o] && b[o]);
axiom (forall a, b: Set T :: { Set#Union(Set#Union(a, b), b) }
Set#Union(Set#Union(a, b), b) == Set#Union(a, b));
axiom (forall a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }
Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));
axiom (forall a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }
Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));
axiom (forall a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }
Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
axiom (forall a, b: Set T :: { Set#Card(Set#Union(a, b)) }{ Set#Card(Set#Intersection(a, b)) }
Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) == Set#Card(a) + Set#Card(b));
function Set#Difference(Set T, Set T): Set T;
axiom (forall a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] } { Set#Difference(a,b), a[o] }
Set#Difference(a,b)[o] <==> a[o] && !b[o]);
axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
b[y] ==> !Set#Difference(a, b)[y] );
axiom (forall a, b: Set T ::
{ Set#Card(Set#Difference(a, b)) }
Set#Card(Set#Difference(a, b)) + Set#Card(Set#Difference(b, a))
+ Set#Card(Set#Intersection(a, b))
== Set#Card(Set#Union(a, b)) &&
Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b)));
function Set#Subset(Set T, Set T): bool;
axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) }
Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
// axiom(forall a: Set T, b: Set T ::
// { Set#Subset(a,b), Set#Card(a), Set#Card(b) } // very restrictive trigger
// Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b));
function Set#Equal(Set T, Set T): bool;
axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) }
Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));
axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets
Set#Equal(a,b) ==> a == b);
//function Set#Disjoint(Set T, Set T): bool;
//axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) }
// Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
// ---------------------------------------------------------------
// -- Axiomatization of multisets --------------------------------
// ---------------------------------------------------------------
function Math#min(a: int, b: int): int;
axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);
axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);
axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);
function Math#clip(a: int): int;
axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);
axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);
type MultiSet T; // = [T]int;
function MultiSet#Select(ms: MultiSet T, x:T): int;
//function $IsGoodMultiSet(ms: MultiSet T): bool;
// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
//axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) }
// $IsGoodMultiSet(ms) <==>
// (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));
axiom (forall ms: MultiSet T, x: T :: {MultiSet#Select(ms,x)} MultiSet#Select(ms,x) >= 0); // NEW
function MultiSet#Card(MultiSet T): int;
axiom (forall s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
//axiom (forall s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
// 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
//
function MultiSet#Empty(): MultiSet T;
axiom (forall o: T :: { MultiSet#Select(MultiSet#Empty(),o) } MultiSet#Select(MultiSet#Empty(),o) == 0);
axiom (forall s: MultiSet T :: { MultiSet#Card(s) }
(MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) &&
(MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < MultiSet#Select(s,x))));
function MultiSet#Singleton(T): MultiSet T;
axiom (forall r: T, o: T :: { MultiSet#Select(MultiSet#Singleton(r),o) } (MultiSet#Select(MultiSet#Singleton(r),o) == 1 <==> r == o) &&
(MultiSet#Select(MultiSet#Singleton(r),o) == 0 <==> r != o));
axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Card(MultiSet#Singleton(r)) == 1 && MultiSet#Select(MultiSet#Singleton(r),r) == 1); // AS: added
axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); // AS: remove this?
function MultiSet#UnionOne(MultiSet T, T): MultiSet T;
// union-ing increases count by one for x, not for others
axiom (forall a: MultiSet T, x: T, o: T :: { MultiSet#Select(MultiSet#UnionOne(a,x),o) } { MultiSet#UnionOne(a, x), MultiSet#Select(a,o) } // AS: added back this trigger (used on a similar axiom before)
MultiSet#Select(MultiSet#UnionOne(a, x),o) == (if x==o then MultiSet#Select(a,o) + 1 else MultiSet#Select(a,o)));
// non-decreasing
axiom (forall a: MultiSet T, x: T :: { MultiSet#Card(MultiSet#UnionOne(a, x)) } {MultiSet#UnionOne(a, x), MultiSet#Card(a)} // AS: added alternative trigger
MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
// AS: added - concrete knowledge of element added
axiom (forall a: MultiSet T, x: T :: { MultiSet#UnionOne(a,x)}
MultiSet#Select(MultiSet#UnionOne(a, x),x) > 0 && MultiSet#Card(MultiSet#UnionOne(a, x)) > 0);
function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T;
// union-ing is the sum of the contents
axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Union(a,b),o) } {MultiSet#Union(a,b), MultiSet#Select(a,o), MultiSet#Select(b,o)}// AS: added triggers
MultiSet#Select(MultiSet#Union(a,b),o) == MultiSet#Select(a,o) + MultiSet#Select(b,o));
axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Card(MultiSet#Union(a,b)) } {MultiSet#Card(a), MultiSet#Union(a,b)} {MultiSet#Card(b), MultiSet#Union(a,b)}
MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b));
function MultiSet#Intersection(MultiSet T, MultiSet T): MultiSet T;
axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Intersection(a,b),o) }
MultiSet#Select(MultiSet#Intersection(a,b),o) == Math#min(MultiSet#Select(a,o), MultiSet#Select(b,o)));
// left and right pseudo-idempotence
axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }
MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));
axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }
MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));
// multiset difference, a - b. clip() makes it positive.
function MultiSet#Difference(MultiSet T, MultiSet T): MultiSet T;
axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Difference(a,b),o) }
MultiSet#Select(MultiSet#Difference(a,b),o) == Math#clip(MultiSet#Select(a,o) - MultiSet#Select(b,o)));
axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), MultiSet#Select(b,y), MultiSet#Select(a,y) }
MultiSet#Select(a,y) <= MultiSet#Select(b,y) ==> MultiSet#Select(MultiSet#Difference(a, b),y) == 0 );
axiom (forall a, b: MultiSet T ::
{ MultiSet#Card(MultiSet#Difference(a, b)) }
MultiSet#Card(MultiSet#Difference(a, b)) + MultiSet#Card(MultiSet#Difference(b, a))
+ 2 * MultiSet#Card(MultiSet#Intersection(a, b))
== MultiSet#Card(MultiSet#Union(a, b)) &&
MultiSet#Card(MultiSet#Difference(a, b)) == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b)));
// multiset subset means a must have at most as many of each element as b
function MultiSet#Subset(MultiSet T, MultiSet T): bool;
axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) }
MultiSet#Subset(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) <= MultiSet#Select(b,o)));
function MultiSet#Equal(MultiSet T, MultiSet T): bool;
axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
MultiSet#Equal(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) == MultiSet#Select(b,o)));
// extensionality axiom for multisets
axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
MultiSet#Equal(a,b) ==> a == b);
function MultiSet#Disjoint(MultiSet T, MultiSet T): bool;
axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }
MultiSet#Disjoint(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) == 0 || MultiSet#Select(b,o) == 0));
// ==================================================
// Preamble of Map module.
// ==================================================
type Map U V;
// A Map is defined by three functions, Map#Domain, Map#Elements, and #Map#Card.
function Map#Domain(Map U V) : Set U;
function Map#Elements(Map U V) : [U]V;
function Map#Card(Map U V) : int;
axiom (forall m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
// The set of Keys of a Map are available by Map#Domain, and the cardinality of that
// set is given by Map#Card.
/* added second trigger set */
axiom (forall m: Map U V :: { Set#Card(Map#Domain(m)) } { Map#Card(m) }
Set#Card(Map#Domain(m)) == Map#Card(m));
// The set of Values of a Map can be obtained by the function Map#Values, which is
// defined as follows. Remember, a Set is defined by membership (using Boogie's
// square brackets) and Map#Card, so we need to define what these mean for the Set
// returned by Map#Values.
function Map#Values(Map U V) : Set V;
/* split axiom into each direction */
axiom (forall m: Map U V, v: V :: { Map#Values(m)[v] }
Map#Values(m)[v] ==>
(exists u: U :: { Map#Domain(m)[u] } { Map#Elements(m)[u] }
Map#Domain(m)[u] &&
v == Map#Elements(m)[u]));
axiom (forall m: Map U V, u: U :: { Map#Elements(m)[u] } // { Map#Domain(m)[u] } // REMOVED this trigger due to a potential for matching loops
Map#Domain(m)[u]
==> Map#Values(m)[Map#Elements(m)[u]]);
// There's a potential for matching loops with the extra trigger if two maps have equal domains:
// v in range(m1); some k in dom(m1) = dom(m2) s.t. m1[k] = v; m2[k] in range(m2); some k' in dom(m2) s.t. m2[k'] = m2[k]
axiom (forall m: Map U V, u: U :: { Map#Domain(m)[u] } { Map#Elements(m)[u] }
Map#Domain(m)[u]
==> Set#Card(Map#Values(m)) > 0); // weaker property than above, with weaker triggers
// Here are the operations that produce Map values.
function Map#Empty(): Map U V;
axiom (forall u: U ::
{ Map#Domain(Map#Empty(): Map U V)[u] }
!Map#Domain(Map#Empty(): Map U V)[u]);
axiom (forall m: Map U V :: { Map#Card(m) }
(Map#Card(m) == 0 <==> m == Map#Empty()) &&
(Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])) &&
((forall x: U :: {Map#Domain(m)[x]} Map#Domain(m)[x] ==> Map#Card(m) != 0)));
//Build is used in displays, and for map updates
function Map#Build(Map U V, U, V): Map U V;
/* added second trigger set (cf. example3 test case, test3) */
axiom (forall m: Map U V, u: U, u': U, v: V ::
{ Map#Domain(Map#Build(m, u, v))[u'] } { Map#Domain(m)[u'],Map#Build(m, u, v) } { Map#Elements(Map#Build(m, u, v))[u'] }
(u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] &&
Map#Elements(Map#Build(m, u, v))[u'] == v) &&
(u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] &&
Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
/* added second trigger set (not sure of a test case needing it, though) */
axiom (forall m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }{ Map#Card(m),Map#Build(m, u, v) }
Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
/* added second trigger set (not sure of a test case needing it, though) */
axiom (forall m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }{ Map#Card(m),Map#Build(m, u, v) }
!Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
//equality for maps
// this axiom is only needed in one direction; the other is implied by the next axiom
function Map#Equal(Map U V, Map U V): bool;
axiom (forall m: Map U V, m': Map U V::
{ Map#Equal(m, m') }
(forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) &&
(forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]) ==> Map#Equal(m, m'));
// extensionality
axiom (forall m: Map U V, m': Map U V::
{ Map#Equal(m, m') }
Map#Equal(m, m') ==> m == m');
function Map#Disjoint(Map U V, Map U V): bool;
// split in both directions
axiom (forall m: Map U V, m': Map U V ::
{ Map#Disjoint(m, m') }
Map#Disjoint(m, m') ==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));
axiom (forall m: Map U V, m': Map U V ::
{ Map#Disjoint(m, m') }
!Map#Disjoint(m, m') ==> (exists o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} Map#Domain(m)[o] && Map#Domain(m')[o]));
// ==================================================
// Translation of domain Array
// ==================================================
// The type for domain Array
type ArrayDomainType;
// Translation of domain function loc
function loc(a_2: ArrayDomainType, i: int): Ref;
// Translation of domain function len
function len(a_2: ArrayDomainType): int;
// Translation of domain function first
function first(r_1: Ref): ArrayDomainType;
// Translation of domain function second
function second(r_1: Ref): int;
// Translation of domain axiom all_diff
axiom (forall a_3: ArrayDomainType, i_1: int ::
{ (loc(a_3, i_1): Ref) }
(first((loc(a_3, i_1): Ref)): ArrayDomainType) == a_3 && (second((loc(a_3, i_1): Ref)): int) == i_1
);
// Translation of domain axiom len_nonneg
axiom (forall a_3: ArrayDomainType ::
{ (len(a_3): int) }
(len(a_3): int) >= 0
);
// ==================================================
// Translation of domain Fold
// ==================================================
// The type for domain Fold
type FoldDomainType A V B;
// Translation of domain function hfold
function hfold(r_1: (ReceiverDomainType A), m: (MappingDomainType V B), op: (OperatorDomainType B)): FoldDomainType A V B;
// Translation of domain function hfoldApply
function hfoldApply(c: (FoldDomainType A V B), snap: (Map A B)): B;
// Translation of domain function hfoldApply1
function hfoldApply1(c: (FoldDomainType A V B), snap: (Map A B)): B;
// Translation of domain function getreceiver
function getreceiver(c: (FoldDomainType A V B)): ReceiverDomainType A;
// Translation of domain function getoperator
function getoperator(c: (FoldDomainType A V B)): OperatorDomainType B;
// Translation of domain function getmapping
function getmapping(c: (FoldDomainType A V B)): MappingDomainType V B;
// Translation of domain function dummy1
function dummy1(a_2: B): bool;
// Translation of domain function _triggerDeleteBlock
function _triggerDeleteBlock(applyC: B, block: (Set A)): bool;
// Translation of domain function _triggerDeleteKey1
function _triggerDeleteKey1(applyC: B, key: A): bool;
// Translation of domain function exhaleCompMap
function exhaleCompMap(c: (FoldDomainType A V B), m: (Map A B), fieldID: int): bool;
// Translation of domain function getSnapFieldID
function getSnapFieldID(m: (Map A B)): int;
// Translation of domain axiom applyComp1Eq
axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B) ::
{ (hfoldApply(__fold_c, __fold_snap): B) }
(hfoldApply(__fold_c, __fold_snap): B) == (hfoldApply1(__fold_c, __fold_snap): B)
);
// Translation of domain axiom _invAxFold
axiom (forall __fold_r: (ReceiverDomainType A), __fold_m: (MappingDomainType V B), __fold_o: (OperatorDomainType B) ::
{ (hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B) }
(getreceiver((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): ReceiverDomainType A) == __fold_r && ((getmapping((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): MappingDomainType V B) == __fold_m && (getoperator((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): OperatorDomainType B) == __fold_o)
);
// Translation of domain axiom _emptyFold
axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B) ::
{ (hfoldApply(__fold_c, __fold_snap): B) }
Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Empty(): Set A)) ==> Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Empty(): Set A)) && (hfoldApply(__fold_c, __fold_snap): B) == (opGetIden((getoperator(__fold_c): OperatorDomainType B)): B)
);
// Translation of domain axiom _singleton
axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B), __fold_elem: A ::
{ (hfoldApply(__fold_c, __fold_snap): B), (Set#Singleton(__fold_elem): Set A) }
Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Singleton(__fold_elem): Set A)) ==> Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Singleton(__fold_elem): Set A)) && (hfoldApply(__fold_c, __fold_snap): B) == Map#Elements(__fold_snap)[__fold_elem]
);
// Translation of domain axiom _dropOne1
axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap1: (Map A B), __fold_key: A ::
{ (_triggerDeleteKey1((hfoldApply(__fold_c, __fold_snap1): B), __fold_key): bool) }
(Map#Domain(__fold_snap1): Set A)[__fold_key] ==> (Map#Domain(__fold_snap1): Set A)[__fold_key] && (hfoldApply(__fold_c, __fold_snap1): B) == (opApply((getoperator(__fold_c): OperatorDomainType B), (hfoldApply1(__fold_c, (mapDelete(__fold_snap1, (Set#Singleton(__fold_key): Set A)): Map A B)): B), Map#Elements(__fold_snap1)[__fold_key]): B)
);
// Translation of domain axiom loseMany
axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap1: (Map A B), __fold_keys: (Set A) ::
{ (_triggerDeleteBlock((hfoldApply(__fold_c, __fold_snap1): B), __fold_keys): bool) }
Set#Subset(__fold_keys, (Map#Domain(__fold_snap1): Set A)) ==> Set#Subset(__fold_keys, (Map#Domain(__fold_snap1): Set A)) && (hfoldApply(__fold_c, __fold_snap1): B) == (opApply((getoperator(__fold_c): OperatorDomainType B), (hfoldApply1(__fold_c, (mapDelete(__fold_snap1, __fold_keys): Map A B)): B), (hfoldApply1(__fold_c, (mapSubmap(__fold_snap1, __fold_keys): Map A B)): B)): B)
);
// ==================================================
// Translation of domain Receiver
// ==================================================
// The type for domain Receiver
type ReceiverDomainType A;
// Translation of domain function recApply
function recApply(r_1: (ReceiverDomainType A), a_2: A): Ref;
// Translation of domain function recInv
function recInv(rec: (ReceiverDomainType A), ref: Ref): A;
// Translation of domain function filterReceiverGood
function filterReceiverGood(f_7: (Set A), r_1: (ReceiverDomainType A)): bool;
// Translation of domain function filterNotLost
function filterNotLost(f1: (Set A), r_1: (ReceiverDomainType A), lostR: (Set Ref)): Set A;
// Translation of domain axiom _inverse_receiver
axiom (forall __fold_a: A, __fold_f: (Set A), __fold_r: (ReceiverDomainType A) ::
{ (recApply(__fold_r, __fold_a): Ref), (filterReceiverGood(__fold_f, __fold_r): bool) } { (filterReceiverGood(__fold_f, __fold_r): bool), __fold_f[__fold_a] }
(filterReceiverGood(__fold_f, __fold_r): bool) && __fold_f[__fold_a] ==> (filterReceiverGood(__fold_f, __fold_r): bool) && (__fold_f[__fold_a] && (recInv(__fold_r, (recApply(__fold_r, __fold_a): Ref)): A) == __fold_a)
);
// Translation of domain axiom _inverse_receiver1
axiom (forall __fold_ref: Ref, __fold_f: (Set A), __fold_r: (ReceiverDomainType A) ::
{ (filterReceiverGood(__fold_f, __fold_r): bool), (recInv(__fold_r, __fold_ref): A) }
(filterReceiverGood(__fold_f, __fold_r): bool) && __fold_f[(recInv(__fold_r, __fold_ref): A)] ==> (filterReceiverGood(__fold_f, __fold_r): bool) && (__fold_f[(recInv(__fold_r, __fold_ref): A)] && (recApply(__fold_r, (recInv(__fold_r, __fold_ref): A)): Ref) == __fold_ref)
);
// Translation of domain axiom smallerF
axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) ::
{ Set#Subset(__fold_f2, __fold_f1), (filterReceiverGood(__fold_f1, __fold_r): bool) }
(filterReceiverGood(__fold_f1, __fold_r): bool) && Set#Subset(__fold_f2, __fold_f1) ==> (filterReceiverGood(__fold_f1, __fold_r): bool) && (Set#Subset(__fold_f2, __fold_f1) && (filterReceiverGood(__fold_f2, __fold_r): bool))
);
// Translation of domain axiom smallerFDelete
axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) ::
{ (filterReceiverGood(__fold_f1, __fold_r): bool), (Set#Difference(__fold_f1, __fold_f2): Set A) }
(filterReceiverGood(__fold_f1, __fold_r): bool) ==> (filterReceiverGood(__fold_f1, __fold_r): bool) && (filterReceiverGood((Set#Difference(__fold_f1, __fold_f2): Set A), __fold_r): bool)
);
// Translation of domain axiom unionF
axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) ::
{ (filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) }
(filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) ==> (filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) && ((filterReceiverGood(__fold_f1, __fold_r): bool) && (filterReceiverGood(__fold_f2, __fold_r): bool))
);
// Translation of domain axiom _filterNotLostAxiom
axiom (forall __fold_a: A, __fold_fs: (Set A), __fold_r: (ReceiverDomainType A), __fold_lostR: (Set Ref) ::
{ (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A)[__fold_a] }
(filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A)[__fold_a] == (__fold_fs[__fold_a] && !__fold_lostR[(recApply(__fold_r, __fold_a): Ref)])
);
// Translation of domain axiom _filterNotLostSubset
axiom (forall __fold_fs: (Set A), __fold_r: (ReceiverDomainType A), __fold_lostR: (Set Ref) ::
{ (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A) }
Set#Subset((filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A), __fold_fs)
);
// ==================================================
// Translation of domain Operator
// ==================================================
// The type for domain Operator
type OperatorDomainType B;
// Translation of domain function _noTrigOp
function _noTrigOp(out: B): bool;
// Translation of domain function opApply
function opApply(op: (OperatorDomainType B), val1: B, val2: B): B;
// Translation of domain function opGetIden
function opGetIden(op: (OperatorDomainType B)): B;
// ==================================================
// Translation of domain Mapping
// ==================================================
// The type for domain Mapping
type MappingDomainType V B;
// Translation of domain function mapApply
function mapApply(m: (MappingDomainType V B), _mInput: V): B;
// Translation of domain function mapIdentity
function mapIdentity(): MappingDomainType V V;
// Translation of anonymous domain axiom
axiom (forall __v: V ::
{ (mapApply((mapIdentity(): MappingDomainType V V), __v): V) }
(mapApply((mapIdentity(): MappingDomainType V V), __v): V) == __v
);
// ==================================================
// Translation of domain MapEdit
// ==================================================
// The type for domain MapEdit
type MapEditDomainType A B;
// Translation of domain function mapDelete
function mapDelete(m: (Map A B), e: (Set A)): Map A B;
// Translation of domain function mapSubmap
function mapSubmap(m: (Map A B), es: (Set A)): Map A B;
// Translation of domain function disjUnionEq
function disjUnionEq(s1: (Set A), s2: (Set A), s3: (Set A)): bool;
// Translation of domain axiom disjUnionEqDef
axiom (forall __fold_s1: (Set A), __fold_s2: (Set A), __fold_s3: (Set A) ::
{ (disjUnionEq(__fold_s1, __fold_s2, __fold_s3): bool) }
(disjUnionEq(__fold_s1, __fold_s2, __fold_s3): bool) == (Set#Equal((Set#Intersection(__fold_s1, __fold_s2): Set A), (Set#Empty(): Set A)) && Set#Equal((Set#Union(__fold_s1, __fold_s2): Set A), __fold_s3))
);
// ==================================================
// Translation of domain setFunc
// ==================================================
// The type for domain setFunc
type setFuncDomainType A;
// Translation of domain axiom setminusAssoc
axiom (forall __fold_s1: (Set A), __fold_s2: (Set A), __fold_s3: (Set A) ::
{ (Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s3): Set A) }
Set#Equal((Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s3): Set A), (Set#Difference((Set#Difference(__fold_s1, __fold_s3): Set A), __fold_s2): Set A))
);
// Translation of domain axiom setminusRepeated
axiom (forall __fold_s1: (Set A), __fold_s2: (Set A) ::
{ (Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s2): Set A) }
Set#Equal((Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s2): Set A), (Set#Difference(__fold_s1, __fold_s2): Set A))
);
// Translation of domain axiom _emptySubset
axiom (forall __fold_s1: (Set A), __fold_s2: (Set A) ::
{ Set#Subset(__fold_s2, __fold_s1) }
Set#Equal(__fold_s1, (Set#Empty(): Set A)) ==> Set#Subset(__fold_s2, __fold_s1) == Set#Equal(__fold_s2, (Set#Empty(): Set A))
);
// ==================================================
// Translation of domain ___arrayRec_Receiver_Domain
// ==================================================
// The type for domain ___arrayRec_Receiver_Domain
type ___arrayRec_Receiver_DomainDomainType;
// Translation of domain function arrayRec
function arrayRec(a_2: ArrayDomainType): ReceiverDomainType int;
// Translation of anonymous domain axiom
axiom (forall a_3: ArrayDomainType, i_1: int ::
{ (recApply((arrayRec(a_3): ReceiverDomainType int), i_1): Ref) } { (loc(a_3, i_1): Ref) }
(recApply((arrayRec(a_3): ReceiverDomainType int), i_1): Ref) == (loc(a_3, i_1): Ref)
);
// ==================================================
// Translation of domain ___allInt_Filter_Domain
// ==================================================
// The type for domain ___allInt_Filter_Domain
type ___allInt_Filter_DomainDomainType;
// Translation of domain function allInt
function allInt(start: int, end: int): Set int;
// Translation of anonymous domain axiom
axiom (forall start_1: int, end_1: int, i_1: int ::
{ (allInt(start_1, end_1): Set int)[i_1] }
(allInt(start_1, end_1): Set int)[i_1] == (i_1 >= start_1 && i_1 < end_1)
);
// ==================================================
// Translation of domain ___add_Operator_Domain
// ==================================================
// The type for domain ___add_Operator_Domain
type ___add_Operator_DomainDomainType;
// Translation of domain function add
function add(): OperatorDomainType int;
// Translation of anonymous domain axiom
axiom (forall a_3: int, b_2: int ::
{ (opApply((add(): OperatorDomainType int), a_3, b_2): int) }
(opApply((add(): OperatorDomainType int), a_3, b_2): int) == a_3 + b_2
);
// Translation of anonymous domain axiom
axiom (opGetIden((add(): OperatorDomainType int)): int) == 0;
// ==================================================
// Translation of all fields
// ==================================================
const unique val: Field NormalField int;
axiom !IsPredicateField(val);
axiom !IsWandField(val);
// ==================================================
// Translation of function __snap_Int_Int_Int_val
// ==================================================
// Uninterpreted function definitions
function __snap_Int_Int_Int_val(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
function __snap_Int_Int_Int_val'(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val(Heap, c_1, f_8) }
__snap_Int_Int_Int_val(Heap, c_1, f_8) == __snap_Int_Int_Int_val'(Heap, c_1, f_8) && dummyFunction(__snap_Int_Int_Int_val#triggerStateless(c_1, f_8))
);
axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
dummyFunction(__snap_Int_Int_Int_val#triggerStateless(c_1, f_8))
);
// Framing axioms
function __snap_Int_Int_Int_val#frame(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) ==> __snap_Int_Int_Int_val'(Heap, c_1, f_8) == __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)
);
// ==================================================
// Function used for framing of quantified permission (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) in function __snap_Int_Int_Int_val
// ==================================================
function __qpSkSnap_Int_Int_Int_val(int1: int, int2: int): int;
function __snap_Int_Int_Int_val#condqp1(Heap: HeapType, c_1_1: (FoldDomainType int int int), f_1_1: (Set int)): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8), succHeapTrans(Heap2Heap, Heap1Heap) }
((f_8[__qpSkSnap_Int_Int_Int_val(__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10 <==> f_8[__qpSkSnap_Int_Int_Int_val(__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10) && (f_8[__qpSkSnap_Int_Int_Int_val(__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10 ==> Heap2Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __qpSkSnap_Int_Int_Int_val(__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8))): Ref), val] == Heap1Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __qpSkSnap_Int_Int_Int_val(__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8))): Ref), val])) ==>
__snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8) == __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8)
);
// Postcondition axioms
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> Set#Equal(Map#Domain(__snap_Int_Int_Int_val'(Heap, c_1, f_8)), f_8)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (forall __ind_2: int ::
{ Map#Elements(__snap_Int_Int_Int_val'(Heap, c_1, f_8))[__ind_2] }
f_8[__ind_2] ==> Map#Elements(__snap_Int_Int_Int_val'(Heap, c_1, f_8))[__ind_2] == (mapApply((getmapping(c_1): MappingDomainType int int), Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_2): Ref), val]): int)
)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (forall __s: (Set int) ::
{ (mapDelete(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s): Map int int) }
!Set#Equal(__s, (Set#Empty(): Set int)) ==> Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, Set#Difference(f_8, __s)), (mapDelete(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s): Map int int))
)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (forall __s_1: (Set int) ::
{ (mapSubmap(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s_1): Map int int) }
Set#Subset(__s_1, f_8) && !Set#Equal(__s_1, f_8) ==> Set#Subset(__s_1, f_8) && (!Set#Equal(__s_1, f_8) && Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, __s_1), (mapSubmap(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s_1): Map int int)))
)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (forall __s1: (Set int), __s2: (Set int) ::
{ (disjUnionEq(__s1, __s2, f_8): bool) }
(disjUnionEq(__s1, __s2, f_8): bool) ==> (disjUnionEq(__s1, __s2, f_8): bool) && (hfoldApply1(c_1, __snap_Int_Int_Int_val'(Heap, c_1, f_8)): int) == (opApply((getoperator(c_1): OperatorDomainType int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s1)): int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s2)): int)): int)
)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (forall __s_2: (Set int) ::
{ (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, __s_2)), c_1, __s_2)): int) }
(dummy1(Set#Equal(__s_2, f_8)): bool)
)
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> Map#Equal(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __snap_Int_Int_Int_val_prime(Heap, c_1, f_8))
);
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ f_8[__ind1], f_8[__ind2] }
f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref)
) ==> (getSnapFieldID(__snap_Int_Int_Int_val'(Heap, c_1, f_8)): int) == 0
);
// Trigger function (controlling recursive postconditions)
function __snap_Int_Int_Int_val#trigger(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): bool;
// State-independent trigger function
function __snap_Int_Int_Int_val#triggerStateless(c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
// Check contract well-formedness and postcondition
procedure __snap_Int_Int_Int_val#definedness(c_1: (FoldDomainType int int int), f_8: (Set int)) returns (Result: (Map int int))
modifies Heap, Mask;
{
var QPMask: MaskType;
var __ind_1: int;
var __s_3: (Set int);
var ExhaleWellDef0Mask: MaskType;
var ExhaleWellDef0Heap: HeapType;
var ExhaleHeap: HeapType;
var __s_5: (Set int);
var __s1_1: (Set int);
var __s2_1: (Set int);
// -- Initializing the state
Mask := ZeroMask;
assume state(Heap, Mask);
assume AssumeFunctionsAbove == 0;
// -- Inhaling precondition (with checking)
// -- Do welldefinedness check of the exhale part.
if (*) {
// -- Check definedness of (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in f), (__ind2 in f) } (__ind1 in f) && ((__ind2 in f) && __ind1 != __ind2) ==> (recApply((getreceiver(c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(c): Receiver[Int]), __ind2): Ref))
if (!(filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1_2: int, __ind2_2: int ::
{ f_8[__ind1_2], f_8[__ind2_2] }
f_8[__ind1_2] && (f_8[__ind2_2] && __ind1_2 != __ind2_2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1_2): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2_2): Ref)
);
assume state(Heap, Mask);
// -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10))
if (*) {
assume false;
}
havoc QPMask;
assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@294.13--298.10) [506]"}
(forall __ind_4: int, __ind_4_1: int ::
(((__ind_4 != __ind_4_1 && f_8[__ind_4]) && f_8[__ind_4_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4_1): Ref)
);
// -- Define Inverse Function
assume (forall __ind_4: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] }
f_8[__ind_4] && NoPerm < 1 / 10 ==> qpRange1((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref)) && invRecv1((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref)) == __ind_4
);
assume (forall o_3: Ref ::
{ invRecv1(o_3) }
(f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv1(o_3)): Ref) == o_3
);
// Check that permission expression is non-negative for all fields
assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@294.13--298.10) [507]"}
(forall __ind_4: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] }
f_8[__ind_4] ==> 1 / 10 >= NoPerm
);
// -- Assume set of fields is nonNull
assume (forall __ind_4: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] }
f_8[__ind_4] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) != null
);
// -- Define permissions
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
((f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv1(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val])
);
assume (forall o_3: Ref, f_5: (Field A B) ::
{ Mask[o_3, f_5] } { QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
assume state(Heap, Mask);
assume state(Heap, Mask);
assume false;
}
// -- Normally inhale the inhale part.
assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool);
assume state(Heap, Mask);
// -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10))
if (*) {
assume false;
}
havoc QPMask;
assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@294.13--298.10) [508]"}
(forall __ind_6: int, __ind_6_1: int ::
(((__ind_6 != __ind_6_1 && f_8[__ind_6]) && f_8[__ind_6_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6_1): Ref)
);
// -- Define Inverse Function
assume (forall __ind_6: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] }
f_8[__ind_6] && NoPerm < 1 / 10 ==> qpRange2((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref)) && invRecv2((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref)) == __ind_6
);
assume (forall o_3: Ref ::
{ invRecv2(o_3) }
(f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv2(o_3)): Ref) == o_3
);
// Check that permission expression is non-negative for all fields
assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@294.13--298.10) [509]"}
(forall __ind_6: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] }
f_8[__ind_6] ==> 1 / 10 >= NoPerm
);
// -- Assume set of fields is nonNull
assume (forall __ind_6: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] }
f_8[__ind_6] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) != null
);
// -- Define permissions
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
((f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv2(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val])
);
assume (forall o_3: Ref, f_5: (Field A B) ::
{ Mask[o_3, f_5] } { QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Checking definedness of postcondition (no body)
assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool);
assume state(Heap, Mask);
assume Set#Equal(Map#Domain(Result), f_8);
assume state(Heap, Mask);
// -- Check definedness of (forall __ind: Int :: { result[__ind] } (__ind in f) ==> result[__ind] == (mapApply((getmapping(c): Mapping[Int, Int]), (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val): Int))
if (*) {
if (f_8[__ind_1]) {
assert {:msg " Contract might not be well-formed. Map result might not contain an entry at key __ind. (arrayTestChainIrrel3.vpr@301.12--306.30) [510]"}
Map#Domain(Result)[__ind_1];
assert {:msg " Contract might not be well-formed. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@301.12--306.30) [511]"}
HasDirectPerm(Mask, (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_1): Ref), val);
}
assume false;
}
assume (forall __ind_8: int ::
{ Map#Elements(Result)[__ind_8] }
f_8[__ind_8] ==> Map#Elements(Result)[__ind_8] == (mapApply((getmapping(c_1): MappingDomainType int int), Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_8): Ref), val]): int)
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Check definedness of (forall __s: Set[Int] :: { (mapDelete(result, __s): Map[Int,Int]) } __s != Set[Int]() ==> __snap_Int_Int_Int_val_prime(c, (f setminus __s)) == (mapDelete(result, __s): Map[Int,Int]))
if (*) {
if (!Set#Equal(__s_3, (Set#Empty(): Set int))) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood((f setminus __s), (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@310.7--310.56) [512]"}
(filterReceiverGood(Set#Difference(f_8, __s_3), (getreceiver(c_1): ReceiverDomainType int)): bool);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@310.7--310.56) [513]"}
(forall __ind_9: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] }
Set#Difference(f_8, __s_3)[__ind_9] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@310.7--310.56) [514]"}
(forall __ind_9: int, __ind_9_1: int ::
{ neverTriggered3(__ind_9), neverTriggered3(__ind_9_1) }
(((__ind_9 != __ind_9_1 && Set#Difference(f_8, __s_3)[__ind_9]) && Set#Difference(f_8, __s_3)[__ind_9_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@310.7--310.56) [515]"}
(forall __ind_9: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] }
Set#Difference(f_8, __s_3)[__ind_9] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref)
assume (forall __ind_9: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] }
Set#Difference(f_8, __s_3)[__ind_9] && NoPerm < 1 / 10 ==> qpRange3((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref)) && invRecv3((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref)) == __ind_9
);
assume (forall o_3: Ref ::
{ invRecv3(o_3) }
Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv3(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv3(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
assume false;
}
assume (forall __s_4: (Set int) ::
{ (mapDelete(Result, __s_4): Map int int) }
!Set#Equal(__s_4, (Set#Empty(): Set int)) ==> Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, Set#Difference(f_8, __s_4)), (mapDelete(Result, __s_4): Map int int))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Check definedness of (forall __s: Set[Int] :: { (mapSubmap(result, __s): Map[Int,Int]) } (__s subset f) && __s != f ==> (__s subset f) && (__s != f && __snap_Int_Int_Int_val_prime(c, __s) == (mapSubmap(result, __s): Map[Int,Int])))
if (*) {
if (Set#Subset(__s_5, f_8) && !Set#Equal(__s_5, f_8)) {
if (Set#Subset(__s_5, f_8)) {
if (!Set#Equal(__s_5, f_8)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@317.7--317.43) [516]"}
(filterReceiverGood(__s_5, (getreceiver(c_1): ReceiverDomainType int)): bool);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@317.7--317.43) [517]"}
(forall __ind_10: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] }
__s_5[__ind_10] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@317.7--317.43) [518]"}
(forall __ind_10: int, __ind_10_1: int ::
{ neverTriggered4(__ind_10), neverTriggered4(__ind_10_1) }
(((__ind_10 != __ind_10_1 && __s_5[__ind_10]) && __s_5[__ind_10_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@317.7--317.43) [519]"}
(forall __ind_10: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] }
__s_5[__ind_10] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref)
assume (forall __ind_10: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] }
__s_5[__ind_10] && NoPerm < 1 / 10 ==> qpRange4((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref)) && invRecv4((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref)) == __ind_10
);
assume (forall o_3: Ref ::
{ invRecv4(o_3) }
__s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv4(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv4(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __s_6: (Set int) ::
{ (mapSubmap(Result, __s_6): Map int int) }
Set#Subset(__s_6, f_8) && !Set#Equal(__s_6, f_8) ==> Set#Subset(__s_6, f_8) && (!Set#Equal(__s_6, f_8) && Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, __s_6), (mapSubmap(Result, __s_6): Map int int)))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Check definedness of (forall __s1: Set[Int], __s2: Set[Int] :: { (disjUnionEq(__s1, __s2, f): Bool) } (disjUnionEq(__s1, __s2, f): Bool) ==> (disjUnionEq(__s1, __s2, f): Bool) && (hfoldApply1(c, result): Int) == (opApply((getoperator(c): Operator[Int]), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s1)): Int), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s2)): Int)): Int))
if (*) {
if ((disjUnionEq(__s1_1, __s2_1, f_8): bool)) {
if ((disjUnionEq(__s1_1, __s2_1, f_8): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s1, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@324.65--325.12) [520]"}
(filterReceiverGood(__s1_1, (getreceiver(c_1): ReceiverDomainType int)): bool);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@324.65--325.12) [521]"}
(forall __ind_11: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] }
__s1_1[__ind_11] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@324.65--325.12) [522]"}
(forall __ind_11: int, __ind_11_1: int ::
{ neverTriggered5(__ind_11), neverTriggered5(__ind_11_1) }
(((__ind_11 != __ind_11_1 && __s1_1[__ind_11]) && __s1_1[__ind_11_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@324.65--325.12) [523]"}
(forall __ind_11: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] }
__s1_1[__ind_11] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref)
assume (forall __ind_11: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] }
__s1_1[__ind_11] && NoPerm < 1 / 10 ==> qpRange5((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref)) && invRecv5((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref)) == __ind_11
);
assume (forall o_3: Ref ::
{ invRecv5(o_3) }
__s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv5(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv5(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s2, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@325.37--325.74) [524]"}
(filterReceiverGood(__s2_1, (getreceiver(c_1): ReceiverDomainType int)): bool);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@325.37--325.74) [525]"}
(forall __ind_12: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] }
__s2_1[__ind_12] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@325.37--325.74) [526]"}
(forall __ind_12: int, __ind_12_1: int ::
{ neverTriggered6(__ind_12), neverTriggered6(__ind_12_1) }
(((__ind_12 != __ind_12_1 && __s2_1[__ind_12]) && __s2_1[__ind_12_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@325.37--325.74) [527]"}
(forall __ind_12: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] }
__s2_1[__ind_12] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref)
assume (forall __ind_12: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] }
__s2_1[__ind_12] && NoPerm < 1 / 10 ==> qpRange6((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref)) && invRecv6((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref)) == __ind_12
);
assume (forall o_3: Ref ::
{ invRecv6(o_3) }
__s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv6(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv6(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
assume false;
}
assume (forall __s1_2: (Set int), __s2_2: (Set int) ::
{ (disjUnionEq(__s1_2, __s2_2, f_8): bool) }
(disjUnionEq(__s1_2, __s2_2, f_8): bool) ==> (disjUnionEq(__s1_2, __s2_2, f_8): bool) && (hfoldApply1(c_1, Result): int) == (opApply((getoperator(c_1): OperatorDomainType int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s1_2)): int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s2_2)): int)): int)
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Check definedness of (forall __s: Set[Int] :: { (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s)): Int) } (dummy1(__s == f): Bool))
if (*) {
assume false;
}
assume (forall __s_8: (Set int) ::
{ (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, __s_8)), c_1, __s_8)): int) }
(dummy1(Set#Equal(__s_8, f_8)): bool)
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Check definedness of result == __snap_Int_Int_Int_val_prime(c, f)
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@329.21--329.55) [528]"}
(filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@329.21--329.55) [529]"}
(forall __ind_13: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] }
f_8[__ind_13] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@329.21--329.55) [530]"}
(forall __ind_13: int, __ind_13_1: int ::
{ neverTriggered7(__ind_13), neverTriggered7(__ind_13_1) }
(((__ind_13 != __ind_13_1 && f_8[__ind_13]) && f_8[__ind_13_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@329.21--329.55) [531]"}
(forall __ind_13: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] }
f_8[__ind_13] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref)
assume (forall __ind_13: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] }
f_8[__ind_13] && NoPerm < 1 / 10 ==> qpRange7((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref)) && invRecv7((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref)) == __ind_13
);
assume (forall o_3: Ref ::
{ invRecv7(o_3) }
f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv7(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv7(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
assume Map#Equal(Result, __snap_Int_Int_Int_val_prime(Heap, c_1, f_8));
assume state(Heap, Mask);
assume (getSnapFieldID(Result): int) == 0;
assume state(Heap, Mask);
}
// ==================================================
// Translation of function __snap_Int_Int_Int_val_prime
// ==================================================
// Uninterpreted function definitions
function __snap_Int_Int_Int_val_prime(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
function __snap_Int_Int_Int_val_prime'(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val_prime(Heap, c_1, f_8) }
__snap_Int_Int_Int_val_prime(Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) && dummyFunction(__snap_Int_Int_Int_val_prime#triggerStateless(c_1, f_8))
);
axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) }
dummyFunction(__snap_Int_Int_Int_val_prime#triggerStateless(c_1, f_8))
);
// Framing axioms
function __snap_Int_Int_Int_val_prime#frame(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) }
state(Heap, Mask) ==> __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, f_8)), c_1, f_8)
);
// ==================================================
// Function used for framing of quantified permission (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) in function __snap_Int_Int_Int_val_prime
// ==================================================
function __qpSkSnap_Int_Int_Int_val_prime(int1: int, int2: int): int;
function __snap_Int_Int_Int_val_prime#condqp2(Heap: HeapType, c_2_1: (FoldDomainType int int int), f_2_1: (Set int)): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ __snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8), succHeapTrans(Heap2Heap, Heap1Heap) }
((f_8[__qpSkSnap_Int_Int_Int_val_prime(__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10 <==> f_8[__qpSkSnap_Int_Int_Int_val_prime(__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10) && (f_8[__qpSkSnap_Int_Int_Int_val_prime(__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8))] && NoPerm < 1 / 10 ==> Heap2Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __qpSkSnap_Int_Int_Int_val_prime(__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8))): Ref), val] == Heap1Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __qpSkSnap_Int_Int_Int_val_prime(__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8))): Ref), val])) ==>
__snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8)
);
// Postcondition axioms
axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) ::
{ state(Heap, Mask), __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) }
state(Heap, Mask) && (AssumeFunctionsAbove < 1 || __snap_Int_Int_Int_val_prime#trigger(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool)
);
// Trigger function (controlling recursive postconditions)
function __snap_Int_Int_Int_val_prime#trigger(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): bool;
// State-independent trigger function
function __snap_Int_Int_Int_val_prime#triggerStateless(c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int;
// Check contract well-formedness and postcondition
procedure __snap_Int_Int_Int_val_prime#definedness(c_1: (FoldDomainType int int int), f_8: (Set int)) returns (Result: (Map int int))
modifies Heap, Mask;
{
var QPMask: MaskType;
// -- Initializing the state
Mask := ZeroMask;
assume state(Heap, Mask);
assume AssumeFunctionsAbove == 1;
// -- Inhaling precondition (with checking)
assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool);
assume state(Heap, Mask);
// -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10))
if (*) {
assume false;
}
havoc QPMask;
assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@335.13--339.10) [532]"}
(forall __ind_3: int, __ind_3_1: int ::
(((__ind_3 != __ind_3_1 && f_8[__ind_3]) && f_8[__ind_3_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3_1): Ref)
);
// -- Define Inverse Function
assume (forall __ind_3: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] }
f_8[__ind_3] && NoPerm < 1 / 10 ==> qpRange8((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref)) && invRecv8((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref)) == __ind_3
);
assume (forall o_3: Ref ::
{ invRecv8(o_3) }
(f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv8(o_3)): Ref) == o_3
);
// Check that permission expression is non-negative for all fields
assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@335.13--339.10) [533]"}
(forall __ind_3: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] }
f_8[__ind_3] ==> 1 / 10 >= NoPerm
);
// -- Assume set of fields is nonNull
assume (forall __ind_3: int ::
{ (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] }
f_8[__ind_3] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) != null
);
// -- Define permissions
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
((f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv8(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val])
);
assume (forall o_3: Ref, f_5: (Field A B) ::
{ Mask[o_3, f_5] } { QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Checking definedness of postcondition (no body)
assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool);
assume state(Heap, Mask);
}
// ==================================================
// Translation of method operator_add_welldef_check
// ==================================================
procedure operator_add_welldef_check() returns ()
modifies Heap, Mask;
{
var oldMask: MaskType;
var oldHeap: HeapType;
var ExhaleWellDef0Mask: MaskType;
var ExhaleWellDef0Heap: HeapType;
var _i1_1: int;
var _i2_1: int;
var _i1_4: int;
var _i2_4: int;
var _i3_1: int;
var _i1_7: int;
// -- Initializing the state
Mask := ZeroMask;
assume state(Heap, Mask);
assume AssumeFunctionsAbove == -1;
// -- Initializing of old state
// -- Initializing the old state
oldMask := Mask;
oldHeap := Heap;
// -- Translating statement: assert (forall _i1: Int, _i2: Int ::
// { (_noTrigOp((opApply(add(), _i1, _i2): Int)): Bool) }
// (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int)) -- arrayTestChainIrrel3.vpr@345.3--348.56
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
// -- Check definedness of (forall _i1: Int, _i2: Int :: { (_noTrigOp((opApply(add(), _i1, _i2): Int)): Bool) } (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int))
if (*) {
assume false;
}
if (*) {
assert {:msg " Assert might fail. Assertion (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int) might not hold. (arrayTestChainIrrel3.vpr@345.11--348.55) [534]"}
(opApply((add(): OperatorDomainType int), _i1_1, _i2_1): int) == (opApply((add(): OperatorDomainType int), _i2_1, _i1_1): int);
assume false;
}
assume (forall _i1_2_1: int, _i2_2_1: int ::
{ (_noTrigOp((opApply((add(): OperatorDomainType int), _i1_2_1, _i2_2_1): int)): bool) }
(opApply((add(): OperatorDomainType int), _i1_2_1, _i2_2_1): int) == (opApply((add(): OperatorDomainType int), _i2_2_1, _i1_2_1): int)
);
assume state(Heap, Mask);
// -- Translating statement: assert (forall _i1: Int, _i2: Int, _i3: Int ::
// { (_noTrigOp((opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int)): Bool) }
// (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) ==
// (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int)) -- arrayTestChainIrrel3.vpr@349.3--355.30
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
// -- Check definedness of (forall _i1: Int, _i2: Int, _i3: Int :: { (_noTrigOp((opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int)): Bool) } (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) == (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int))
if (*) {
assume false;
}
if (*) {
assert {:msg " Assert might fail. Assertion (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) == (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int) might not hold. (arrayTestChainIrrel3.vpr@349.11--355.29) [535]"}
(opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_4, _i2_4): int), _i3_1): int) == (opApply((add(): OperatorDomainType int), _i1_4, (opApply((add(): OperatorDomainType int), _i2_4, _i3_1): int)): int);
assume false;
}
assume (forall _i1_5_1: int, _i2_5_1: int, _i3_2_1: int ::
{ (_noTrigOp((opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_5_1, _i2_5_1): int), _i3_2_1): int)): bool) }
(opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_5_1, _i2_5_1): int), _i3_2_1): int) == (opApply((add(): OperatorDomainType int), _i1_5_1, (opApply((add(): OperatorDomainType int), _i2_5_1, _i3_2_1): int)): int)
);
assume state(Heap, Mask);
// -- Translating statement: assert (forall _i1: Int ::
// { (_noTrigOp((opApply(add(), _i1, (opGetIden(add()): Int)): Int)): Bool) }
// (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1) -- arrayTestChainIrrel3.vpr@356.3--359.11
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
// -- Check definedness of (forall _i1: Int :: { (_noTrigOp((opApply(add(), _i1, (opGetIden(add()): Int)): Int)): Bool) } (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1)
if (*) {
assume false;
}
if (*) {
assert {:msg " Assert might fail. Assertion (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1 might not hold. (arrayTestChainIrrel3.vpr@356.11--359.10) [536]"}
(opApply((add(): OperatorDomainType int), _i1_7, (opGetIden((add(): OperatorDomainType int)): int)): int) == _i1_7;
assume false;
}
assume (forall _i1_8_1: int ::
{ (_noTrigOp((opApply((add(): OperatorDomainType int), _i1_8_1, (opGetIden((add(): OperatorDomainType int)): int)): int)): bool) }
(opApply((add(): OperatorDomainType int), _i1_8_1, (opGetIden((add(): OperatorDomainType int)): int)): int) == _i1_8_1
);
assume state(Heap, Mask);
}
// ==================================================
// Translation of method test1
// ==================================================
procedure test1(a_3: ArrayDomainType) returns ()
modifies Heap, Mask;
{
var _compLabell6_lblGuard: bool;
var _compLabell7_lblGuard: bool;
var _compLabell8_lblGuard: bool;
var _compLabell9_lblGuard: bool;
var _compLabell0_lblGuard: bool;
var _compLabell1_lblGuard: bool;
var _compLabell2_lblGuard: bool;
var _compLabell3_lblGuard: bool;
var _compLabell4_lblGuard: bool;
var _compLabell5_lblGuard: bool;
var QPMask: MaskType;
var oldMask: MaskType;
var oldHeap: HeapType;
var Label_compLabell0Mask: MaskType;
var Label_compLabell0Heap: HeapType;
var js: (Set int);
var vis: (Set int);
var j1: int;
var j2: int;
var j3: int;
var i1: int;
var i2: int;
var i3: int;
var i4: int;
var i5: int;
var i6: int;
var Label_compLabell1Mask: MaskType;
var Label_compLabell1Heap: HeapType;
var __f: (Set int);
var __c: (FoldDomainType int int int);
var ExhaleWellDef0Mask: MaskType;
var ExhaleWellDef0Heap: HeapType;
var ExhaleHeap: HeapType;
var Label_compLabell2Mask: MaskType;
var Label_compLabell2Heap: HeapType;
var __f_2: (Set int);
var __c_2: (FoldDomainType int int int);
var Label_compLabell3Mask: MaskType;
var Label_compLabell3Heap: HeapType;
var __f_4: (Set int);
var __c_4: (FoldDomainType int int int);
var Label_compLabell4Mask: MaskType;
var Label_compLabell4Heap: HeapType;
var __f_6: (Set int);
var __c_6: (FoldDomainType int int int);
var Label_compLabell5Mask: MaskType;
var Label_compLabell5Heap: HeapType;
var __f_8: (Set int);
var __c_8: (FoldDomainType int int int);
var Label_compLabell6Mask: MaskType;
var Label_compLabell6Heap: HeapType;
var __f_10: (Set int);
var __c_10: (FoldDomainType int int int);
var Label_compLabell7Mask: MaskType;
var Label_compLabell7Heap: HeapType;
var __f_12: (Set int);
var __c_12: (FoldDomainType int int int);
var Label_compLabell8Mask: MaskType;
var Label_compLabell8Heap: HeapType;
var __f_14: (Set int);
var __c_14: (FoldDomainType int int int);
var Label_compLabell9Mask: MaskType;
var Label_compLabell9Heap: HeapType;
var __f_16: (Set int);
var __c_16: (FoldDomainType int int int);
var ExhaleWellDef1Mask: MaskType;
var ExhaleWellDef1Heap: HeapType;
// -- Initializing the state
Mask := ZeroMask;
assume state(Heap, Mask);
assume AssumeFunctionsAbove == -1;
_compLabell6_lblGuard := false;
_compLabell7_lblGuard := false;
_compLabell8_lblGuard := false;
_compLabell9_lblGuard := false;
_compLabell0_lblGuard := false;
_compLabell1_lblGuard := false;
_compLabell2_lblGuard := false;
_compLabell3_lblGuard := false;
_compLabell4_lblGuard := false;
_compLabell5_lblGuard := false;
// -- Checked inhaling of precondition
// -- Check definedness of (forall j: Int :: { loc(a, j) } 0 <= j && j < len(a) ==> acc(loc(a, j).val, write))
if (*) {
assume false;
}
havoc QPMask;
assert {:msg " Contract might not be well-formed. Quantified resource loc(a, j).val might not be injective. (arrayTestChainIrrel3.vpr@363.13--365.57) [537]"}
(forall j_1: int, j_1_1: int ::
(((j_1 != j_1_1 && (0 <= j_1 && j_1 < (len(a_3): int))) && (0 <= j_1_1 && j_1_1 < (len(a_3): int))) && NoPerm < FullPerm) && NoPerm < FullPerm ==> (loc(a_3, j_1): Ref) != (loc(a_3, j_1_1): Ref)
);
// -- Define Inverse Function
assume (forall j_1: int ::
{ (loc(a_3, j_1): Ref) } { (loc(a_3, j_1): Ref) }
(0 <= j_1 && j_1 < (len(a_3): int)) && NoPerm < FullPerm ==> qpRange9((loc(a_3, j_1): Ref)) && invRecv9((loc(a_3, j_1): Ref)) == j_1
);
assume (forall o_3: Ref ::
{ invRecv9(o_3) }
((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3) ==> (loc(a_3, invRecv9(o_3)): Ref) == o_3
);
// -- Assume set of fields is nonNull
assume (forall j_1: int ::
{ (loc(a_3, j_1): Ref) } { (loc(a_3, j_1): Ref) }
0 <= j_1 && j_1 < (len(a_3): int) ==> (loc(a_3, j_1): Ref) != null
);
// -- Define permissions
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3) ==> (NoPerm < FullPerm ==> (loc(a_3, invRecv9(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + FullPerm) && (!(((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val])
);
assume (forall o_3: Ref, f_5: (Field A B) ::
{ Mask[o_3, f_5] } { QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
assume state(Heap, Mask);
assume state(Heap, Mask);
assume (len(a_3): int) > 10;
assume state(Heap, Mask);
// -- Initializing of old state
// -- Initializing the old state
oldMask := Mask;
oldHeap := Heap;
// -- Translating statement: label _compLabell0 -- arrayTestChainIrrel3.vpr@379.3--379.21
_compLabell0:
Label_compLabell0Mask := Mask;
Label_compLabell0Heap := Heap;
_compLabell0_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (js subset allInt(0, len(a))) -- arrayTestChainIrrel3.vpr@380.3--380.39
assume Set#Subset(js, (allInt(0, (len(a_3): int)): Set int));
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (is subset allInt(0, len(a))) -- arrayTestChainIrrel3.vpr@381.3--381.39
assume Set#Subset(vis, (allInt(0, (len(a_3): int)): Set int));
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (j1 in js) -- arrayTestChainIrrel3.vpr@382.3--382.20
assume js[j1];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (j2 in js) -- arrayTestChainIrrel3.vpr@383.3--383.20
assume js[j2];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (j3 in js) -- arrayTestChainIrrel3.vpr@384.3--384.20
assume js[j3];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i1 in is) -- arrayTestChainIrrel3.vpr@385.3--385.20
assume vis[i1];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i2 in is) -- arrayTestChainIrrel3.vpr@386.3--386.20
assume vis[i2];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i3 in is) -- arrayTestChainIrrel3.vpr@387.3--387.20
assume vis[i3];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i4 in is) -- arrayTestChainIrrel3.vpr@388.3--388.20
assume vis[i4];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i5 in is) -- arrayTestChainIrrel3.vpr@389.3--389.20
assume vis[i5];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (i6 in is) -- arrayTestChainIrrel3.vpr@390.3--390.20
assume vis[i6];
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i1).val := loc(a, i1).val + 1 -- arrayTestChainIrrel3.vpr@391.3--391.39
// -- Check definedness of loc(a, i1).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i1).val (arrayTestChainIrrel3.vpr@391.3--391.39) [538]"}
HasDirectPerm(Mask, (loc(a_3, i1): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i1).val (arrayTestChainIrrel3.vpr@391.3--391.39) [539]"}
FullPerm == Mask[(loc(a_3, i1): Ref), val];
Heap := Heap[(loc(a_3, i1): Ref), val:=Heap[(loc(a_3, i1): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell1 -- arrayTestChainIrrel3.vpr@392.3--392.21
_compLabell1:
Label_compLabell1Mask := Mask;
Label_compLabell1Heap := Heap;
_compLabell1_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@393.3--406.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) && (forall __ind_1_1: int ::
{ __f[__ind_1_1] }
__f[__ind_1_1] ==> NoPerm < Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_1_1): Ref), val]
)) {
if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@403.45--403.77) [540]"}
(filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int ::
{ __f[__ind1], __f[__ind2] }
__f[__ind1] && (__f[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind2): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@403.45--403.77) [541]"}
(forall __ind_2: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] }
__f[__ind_2] && dummyFunction(Heap[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@403.45--403.77) [542]"}
(forall __ind_2: int, __ind_2_1: int ::
{ neverTriggered10(__ind_2), neverTriggered10(__ind_2_1) }
(((__ind_2 != __ind_2_1 && __f[__ind_2]) && __f[__ind_2_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@403.45--403.77) [543]"}
(forall __ind_2: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] }
__f[__ind_2] ==> Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_2: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] }
__f[__ind_2] && NoPerm < 1 / 10 ==> qpRange10((recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref)) && invRecv10((recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref)) == __ind_2
);
assume (forall o_3: Ref ::
{ invRecv10(o_3) }
__f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv10(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv10(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(Heap, __c, __f)): int), (recInv((getreceiver(__c): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell0 required to evaluate old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@393.11--406.90) [544]"}
_compLabell0_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell0Mask;
ExhaleWellDef0Heap := Label_compLabell0Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@405.62--406.11) [545]"}
(filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) || (forall __ind1_1: int, __ind2_1: int ::
{ __f[__ind1_1], __f[__ind2_1] }
__f[__ind1_1] && (__f[__ind2_1] && __ind1_1 != __ind2_1) ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind1_1): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind2_1): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@405.62--406.11) [546]"}
(forall __ind_3: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] }
__f[__ind_3] && dummyFunction(Label_compLabell0Heap[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@405.62--406.11) [547]"}
(forall __ind_3: int, __ind_3_1: int ::
{ neverTriggered11(__ind_3), neverTriggered11(__ind_3_1) }
(((__ind_3 != __ind_3_1 && __f[__ind_3]) && __f[__ind_3_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@405.62--406.11) [548]"}
(forall __ind_3: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] }
__f[__ind_3] ==> Label_compLabell0Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_3: int ::
{ (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] }
__f[__ind_3] && NoPerm < 1 / 10 ==> qpRange11((recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref)) && invRecv11((recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref)) == __ind_3
);
assume (forall o_3: Ref ::
{ invRecv11(o_3) }
__f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv11(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv11(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell0Mask[o_3, val] - 1 / 10) && (!(__f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3))) ==> QPMask[o_3, val] == Label_compLabell0Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell0Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell0Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell0Heap, ExhaleHeap, Label_compLabell0Mask);
Label_compLabell0Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_1: (FoldDomainType int int int), __f_1: (Set int) ::
{ (hfoldApply(__c_1, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell0Heap, __c_1, __f_1)), __c_1, __f_1)): int) } { (hfoldApply(__c_1, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_1, __f_1)), __c_1, __f_1)): int) }
(filterReceiverGood(__f_1, (getreceiver(__c_1): ReceiverDomainType int)): bool) && (forall __ind_4: int ::
{ __f_1[__ind_4] }
__f_1[__ind_4] ==> NoPerm < Mask[(recApply((getreceiver(__c_1): ReceiverDomainType int), __ind_4): Ref), val]
) ==> (filterReceiverGood(__f_1, (getreceiver(__c_1): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_1, __snap_Int_Int_Int_val(Heap, __c_1, __f_1)): int), (recInv((getreceiver(__c_1): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_1, __snap_Int_Int_Int_val(Label_compLabell0Heap, __c_1, __f_1)): int), (recInv((getreceiver(__c_1): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, j1).val := loc(a, j1).val + 1 -- arrayTestChainIrrel3.vpr@407.3--407.39
// -- Check definedness of loc(a, j1).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j1).val (arrayTestChainIrrel3.vpr@407.3--407.39) [549]"}
HasDirectPerm(Mask, (loc(a_3, j1): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j1).val (arrayTestChainIrrel3.vpr@407.3--407.39) [550]"}
FullPerm == Mask[(loc(a_3, j1): Ref), val];
Heap := Heap[(loc(a_3, j1): Ref), val:=Heap[(loc(a_3, j1): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell2 -- arrayTestChainIrrel3.vpr@408.3--408.21
_compLabell2:
Label_compLabell2Mask := Mask;
Label_compLabell2Heap := Heap;
_compLabell2_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@409.3--422.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) && (forall __ind_6: int ::
{ __f_2[__ind_6] }
__f_2[__ind_6] ==> NoPerm < Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_6): Ref), val]
)) {
if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@419.45--419.77) [551]"}
(filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) || (forall __ind1_2: int, __ind2_2: int ::
{ __f_2[__ind1_2], __f_2[__ind2_2] }
__f_2[__ind1_2] && (__f_2[__ind2_2] && __ind1_2 != __ind2_2) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind1_2): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind2_2): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@419.45--419.77) [552]"}
(forall __ind_7: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] }
__f_2[__ind_7] && dummyFunction(Heap[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@419.45--419.77) [553]"}
(forall __ind_7: int, __ind_7_1: int ::
{ neverTriggered12(__ind_7), neverTriggered12(__ind_7_1) }
(((__ind_7 != __ind_7_1 && __f_2[__ind_7]) && __f_2[__ind_7_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@419.45--419.77) [554]"}
(forall __ind_7: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] }
__f_2[__ind_7] ==> Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_7: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] }
__f_2[__ind_7] && NoPerm < 1 / 10 ==> qpRange12((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref)) && invRecv12((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref)) == __ind_7
);
assume (forall o_3: Ref ::
{ invRecv12(o_3) }
__f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv12(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv12(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_2, __snap_Int_Int_Int_val(Heap, __c_2, __f_2)): int), (recInv((getreceiver(__c_2): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell1 required to evaluate old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@409.11--422.90) [555]"}
_compLabell1_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell1Mask;
ExhaleWellDef0Heap := Label_compLabell1Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@421.62--422.11) [556]"}
(filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) || (forall __ind1_3: int, __ind2_3: int ::
{ __f_2[__ind1_3], __f_2[__ind2_3] }
__f_2[__ind1_3] && (__f_2[__ind2_3] && __ind1_3 != __ind2_3) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind1_3): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind2_3): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@421.62--422.11) [557]"}
(forall __ind_8: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] }
__f_2[__ind_8] && dummyFunction(Label_compLabell1Heap[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@421.62--422.11) [558]"}
(forall __ind_8: int, __ind_8_1: int ::
{ neverTriggered13(__ind_8), neverTriggered13(__ind_8_1) }
(((__ind_8 != __ind_8_1 && __f_2[__ind_8]) && __f_2[__ind_8_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@421.62--422.11) [559]"}
(forall __ind_8: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] }
__f_2[__ind_8] ==> Label_compLabell1Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_8: int ::
{ (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] }
__f_2[__ind_8] && NoPerm < 1 / 10 ==> qpRange13((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref)) && invRecv13((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref)) == __ind_8
);
assume (forall o_3: Ref ::
{ invRecv13(o_3) }
__f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv13(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv13(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell1Mask[o_3, val] - 1 / 10) && (!(__f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3))) ==> QPMask[o_3, val] == Label_compLabell1Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell1Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell1Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell1Heap, ExhaleHeap, Label_compLabell1Mask);
Label_compLabell1Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_3: (FoldDomainType int int int), __f_3: (Set int) ::
{ (hfoldApply(__c_3, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell1Heap, __c_3, __f_3)), __c_3, __f_3)): int) } { (hfoldApply(__c_3, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_3, __f_3)), __c_3, __f_3)): int) }
(filterReceiverGood(__f_3, (getreceiver(__c_3): ReceiverDomainType int)): bool) && (forall __ind_9: int ::
{ __f_3[__ind_9] }
__f_3[__ind_9] ==> NoPerm < Mask[(recApply((getreceiver(__c_3): ReceiverDomainType int), __ind_9): Ref), val]
) ==> (filterReceiverGood(__f_3, (getreceiver(__c_3): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_3, __snap_Int_Int_Int_val(Heap, __c_3, __f_3)): int), (recInv((getreceiver(__c_3): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_3, __snap_Int_Int_Int_val(Label_compLabell1Heap, __c_3, __f_3)): int), (recInv((getreceiver(__c_3): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i2).val := loc(a, i2).val + 1 -- arrayTestChainIrrel3.vpr@423.3--423.39
// -- Check definedness of loc(a, i2).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i2).val (arrayTestChainIrrel3.vpr@423.3--423.39) [560]"}
HasDirectPerm(Mask, (loc(a_3, i2): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i2).val (arrayTestChainIrrel3.vpr@423.3--423.39) [561]"}
FullPerm == Mask[(loc(a_3, i2): Ref), val];
Heap := Heap[(loc(a_3, i2): Ref), val:=Heap[(loc(a_3, i2): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell3 -- arrayTestChainIrrel3.vpr@424.3--424.21
_compLabell3:
Label_compLabell3Mask := Mask;
Label_compLabell3Heap := Heap;
_compLabell3_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@425.3--438.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) && (forall __ind_11: int ::
{ __f_4[__ind_11] }
__f_4[__ind_11] ==> NoPerm < Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_11): Ref), val]
)) {
if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@435.45--435.77) [562]"}
(filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) || (forall __ind1_4: int, __ind2_4: int ::
{ __f_4[__ind1_4], __f_4[__ind2_4] }
__f_4[__ind1_4] && (__f_4[__ind2_4] && __ind1_4 != __ind2_4) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind1_4): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind2_4): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@435.45--435.77) [563]"}
(forall __ind_12: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] }
__f_4[__ind_12] && dummyFunction(Heap[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@435.45--435.77) [564]"}
(forall __ind_12: int, __ind_12_1: int ::
{ neverTriggered14(__ind_12), neverTriggered14(__ind_12_1) }
(((__ind_12 != __ind_12_1 && __f_4[__ind_12]) && __f_4[__ind_12_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@435.45--435.77) [565]"}
(forall __ind_12: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] }
__f_4[__ind_12] ==> Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_12: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] }
__f_4[__ind_12] && NoPerm < 1 / 10 ==> qpRange14((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref)) && invRecv14((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref)) == __ind_12
);
assume (forall o_3: Ref ::
{ invRecv14(o_3) }
__f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv14(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv14(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_4, __snap_Int_Int_Int_val(Heap, __c_4, __f_4)): int), (recInv((getreceiver(__c_4): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell2 required to evaluate old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@425.11--438.90) [566]"}
_compLabell2_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell2Mask;
ExhaleWellDef0Heap := Label_compLabell2Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@437.62--438.11) [567]"}
(filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) || (forall __ind1_5: int, __ind2_5: int ::
{ __f_4[__ind1_5], __f_4[__ind2_5] }
__f_4[__ind1_5] && (__f_4[__ind2_5] && __ind1_5 != __ind2_5) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind1_5): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind2_5): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@437.62--438.11) [568]"}
(forall __ind_13: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] }
__f_4[__ind_13] && dummyFunction(Label_compLabell2Heap[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@437.62--438.11) [569]"}
(forall __ind_13: int, __ind_13_1: int ::
{ neverTriggered15(__ind_13), neverTriggered15(__ind_13_1) }
(((__ind_13 != __ind_13_1 && __f_4[__ind_13]) && __f_4[__ind_13_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@437.62--438.11) [570]"}
(forall __ind_13: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] }
__f_4[__ind_13] ==> Label_compLabell2Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_13: int ::
{ (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] }
__f_4[__ind_13] && NoPerm < 1 / 10 ==> qpRange15((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref)) && invRecv15((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref)) == __ind_13
);
assume (forall o_3: Ref ::
{ invRecv15(o_3) }
__f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv15(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv15(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell2Mask[o_3, val] - 1 / 10) && (!(__f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3))) ==> QPMask[o_3, val] == Label_compLabell2Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell2Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell2Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell2Heap, ExhaleHeap, Label_compLabell2Mask);
Label_compLabell2Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_5: (FoldDomainType int int int), __f_5: (Set int) ::
{ (hfoldApply(__c_5, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell2Heap, __c_5, __f_5)), __c_5, __f_5)): int) } { (hfoldApply(__c_5, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_5, __f_5)), __c_5, __f_5)): int) }
(filterReceiverGood(__f_5, (getreceiver(__c_5): ReceiverDomainType int)): bool) && (forall __ind_14: int ::
{ __f_5[__ind_14] }
__f_5[__ind_14] ==> NoPerm < Mask[(recApply((getreceiver(__c_5): ReceiverDomainType int), __ind_14): Ref), val]
) ==> (filterReceiverGood(__f_5, (getreceiver(__c_5): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_5, __snap_Int_Int_Int_val(Heap, __c_5, __f_5)): int), (recInv((getreceiver(__c_5): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_5, __snap_Int_Int_Int_val(Label_compLabell2Heap, __c_5, __f_5)): int), (recInv((getreceiver(__c_5): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i3).val := loc(a, i3).val + 1 -- arrayTestChainIrrel3.vpr@439.3--439.39
// -- Check definedness of loc(a, i3).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i3).val (arrayTestChainIrrel3.vpr@439.3--439.39) [571]"}
HasDirectPerm(Mask, (loc(a_3, i3): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i3).val (arrayTestChainIrrel3.vpr@439.3--439.39) [572]"}
FullPerm == Mask[(loc(a_3, i3): Ref), val];
Heap := Heap[(loc(a_3, i3): Ref), val:=Heap[(loc(a_3, i3): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell4 -- arrayTestChainIrrel3.vpr@440.3--440.21
_compLabell4:
Label_compLabell4Mask := Mask;
Label_compLabell4Heap := Heap;
_compLabell4_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@441.3--454.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) && (forall __ind_16: int ::
{ __f_6[__ind_16] }
__f_6[__ind_16] ==> NoPerm < Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_16): Ref), val]
)) {
if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@451.45--451.77) [573]"}
(filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) || (forall __ind1_6: int, __ind2_6: int ::
{ __f_6[__ind1_6], __f_6[__ind2_6] }
__f_6[__ind1_6] && (__f_6[__ind2_6] && __ind1_6 != __ind2_6) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind1_6): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind2_6): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@451.45--451.77) [574]"}
(forall __ind_17: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] }
__f_6[__ind_17] && dummyFunction(Heap[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@451.45--451.77) [575]"}
(forall __ind_17: int, __ind_17_1: int ::
{ neverTriggered16(__ind_17), neverTriggered16(__ind_17_1) }
(((__ind_17 != __ind_17_1 && __f_6[__ind_17]) && __f_6[__ind_17_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@451.45--451.77) [576]"}
(forall __ind_17: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] }
__f_6[__ind_17] ==> Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_17: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] }
__f_6[__ind_17] && NoPerm < 1 / 10 ==> qpRange16((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref)) && invRecv16((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref)) == __ind_17
);
assume (forall o_3: Ref ::
{ invRecv16(o_3) }
__f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv16(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv16(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_6, __snap_Int_Int_Int_val(Heap, __c_6, __f_6)): int), (recInv((getreceiver(__c_6): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell3 required to evaluate old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@441.11--454.90) [577]"}
_compLabell3_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell3Mask;
ExhaleWellDef0Heap := Label_compLabell3Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@453.62--454.11) [578]"}
(filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) || (forall __ind1_7: int, __ind2_7: int ::
{ __f_6[__ind1_7], __f_6[__ind2_7] }
__f_6[__ind1_7] && (__f_6[__ind2_7] && __ind1_7 != __ind2_7) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind1_7): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind2_7): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@453.62--454.11) [579]"}
(forall __ind_18: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] }
__f_6[__ind_18] && dummyFunction(Label_compLabell3Heap[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@453.62--454.11) [580]"}
(forall __ind_18: int, __ind_18_1: int ::
{ neverTriggered17(__ind_18), neverTriggered17(__ind_18_1) }
(((__ind_18 != __ind_18_1 && __f_6[__ind_18]) && __f_6[__ind_18_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@453.62--454.11) [581]"}
(forall __ind_18: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] }
__f_6[__ind_18] ==> Label_compLabell3Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_18: int ::
{ (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] }
__f_6[__ind_18] && NoPerm < 1 / 10 ==> qpRange17((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref)) && invRecv17((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref)) == __ind_18
);
assume (forall o_3: Ref ::
{ invRecv17(o_3) }
__f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv17(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv17(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell3Mask[o_3, val] - 1 / 10) && (!(__f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3))) ==> QPMask[o_3, val] == Label_compLabell3Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell3Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell3Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell3Heap, ExhaleHeap, Label_compLabell3Mask);
Label_compLabell3Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_7: (FoldDomainType int int int), __f_7: (Set int) ::
{ (hfoldApply(__c_7, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell3Heap, __c_7, __f_7)), __c_7, __f_7)): int) } { (hfoldApply(__c_7, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_7, __f_7)), __c_7, __f_7)): int) }
(filterReceiverGood(__f_7, (getreceiver(__c_7): ReceiverDomainType int)): bool) && (forall __ind_19: int ::
{ __f_7[__ind_19] }
__f_7[__ind_19] ==> NoPerm < Mask[(recApply((getreceiver(__c_7): ReceiverDomainType int), __ind_19): Ref), val]
) ==> (filterReceiverGood(__f_7, (getreceiver(__c_7): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_7, __snap_Int_Int_Int_val(Heap, __c_7, __f_7)): int), (recInv((getreceiver(__c_7): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_7, __snap_Int_Int_Int_val(Label_compLabell3Heap, __c_7, __f_7)): int), (recInv((getreceiver(__c_7): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, j2).val := loc(a, j2).val + 1 -- arrayTestChainIrrel3.vpr@455.3--455.39
// -- Check definedness of loc(a, j2).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j2).val (arrayTestChainIrrel3.vpr@455.3--455.39) [582]"}
HasDirectPerm(Mask, (loc(a_3, j2): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j2).val (arrayTestChainIrrel3.vpr@455.3--455.39) [583]"}
FullPerm == Mask[(loc(a_3, j2): Ref), val];
Heap := Heap[(loc(a_3, j2): Ref), val:=Heap[(loc(a_3, j2): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell5 -- arrayTestChainIrrel3.vpr@456.3--456.21
_compLabell5:
Label_compLabell5Mask := Mask;
Label_compLabell5Heap := Heap;
_compLabell5_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@457.3--470.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) && (forall __ind_21: int ::
{ __f_8[__ind_21] }
__f_8[__ind_21] ==> NoPerm < Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_21): Ref), val]
)) {
if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@467.45--467.77) [584]"}
(filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) || (forall __ind1_8: int, __ind2_8: int ::
{ __f_8[__ind1_8], __f_8[__ind2_8] }
__f_8[__ind1_8] && (__f_8[__ind2_8] && __ind1_8 != __ind2_8) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind1_8): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind2_8): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@467.45--467.77) [585]"}
(forall __ind_22: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] }
__f_8[__ind_22] && dummyFunction(Heap[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@467.45--467.77) [586]"}
(forall __ind_22: int, __ind_22_1: int ::
{ neverTriggered18(__ind_22), neverTriggered18(__ind_22_1) }
(((__ind_22 != __ind_22_1 && __f_8[__ind_22]) && __f_8[__ind_22_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@467.45--467.77) [587]"}
(forall __ind_22: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] }
__f_8[__ind_22] ==> Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_22: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] }
__f_8[__ind_22] && NoPerm < 1 / 10 ==> qpRange18((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref)) && invRecv18((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref)) == __ind_22
);
assume (forall o_3: Ref ::
{ invRecv18(o_3) }
__f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv18(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv18(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_8, __snap_Int_Int_Int_val(Heap, __c_8, __f_8)): int), (recInv((getreceiver(__c_8): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell4 required to evaluate old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@457.11--470.90) [588]"}
_compLabell4_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell4Mask;
ExhaleWellDef0Heap := Label_compLabell4Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@469.62--470.11) [589]"}
(filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) || (forall __ind1_9: int, __ind2_9: int ::
{ __f_8[__ind1_9], __f_8[__ind2_9] }
__f_8[__ind1_9] && (__f_8[__ind2_9] && __ind1_9 != __ind2_9) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind1_9): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind2_9): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@469.62--470.11) [590]"}
(forall __ind_23: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] }
__f_8[__ind_23] && dummyFunction(Label_compLabell4Heap[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@469.62--470.11) [591]"}
(forall __ind_23: int, __ind_23_1: int ::
{ neverTriggered19(__ind_23), neverTriggered19(__ind_23_1) }
(((__ind_23 != __ind_23_1 && __f_8[__ind_23]) && __f_8[__ind_23_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@469.62--470.11) [592]"}
(forall __ind_23: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] }
__f_8[__ind_23] ==> Label_compLabell4Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_23: int ::
{ (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] }
__f_8[__ind_23] && NoPerm < 1 / 10 ==> qpRange19((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref)) && invRecv19((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref)) == __ind_23
);
assume (forall o_3: Ref ::
{ invRecv19(o_3) }
__f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv19(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv19(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell4Mask[o_3, val] - 1 / 10) && (!(__f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3))) ==> QPMask[o_3, val] == Label_compLabell4Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell4Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell4Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell4Heap, ExhaleHeap, Label_compLabell4Mask);
Label_compLabell4Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_9: (FoldDomainType int int int), __f_9: (Set int) ::
{ (hfoldApply(__c_9, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell4Heap, __c_9, __f_9)), __c_9, __f_9)): int) } { (hfoldApply(__c_9, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_9, __f_9)), __c_9, __f_9)): int) }
(filterReceiverGood(__f_9, (getreceiver(__c_9): ReceiverDomainType int)): bool) && (forall __ind_24: int ::
{ __f_9[__ind_24] }
__f_9[__ind_24] ==> NoPerm < Mask[(recApply((getreceiver(__c_9): ReceiverDomainType int), __ind_24): Ref), val]
) ==> (filterReceiverGood(__f_9, (getreceiver(__c_9): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_9, __snap_Int_Int_Int_val(Heap, __c_9, __f_9)): int), (recInv((getreceiver(__c_9): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_9, __snap_Int_Int_Int_val(Label_compLabell4Heap, __c_9, __f_9)): int), (recInv((getreceiver(__c_9): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i4).val := loc(a, i4).val + 1 -- arrayTestChainIrrel3.vpr@471.3--471.39
// -- Check definedness of loc(a, i4).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i4).val (arrayTestChainIrrel3.vpr@471.3--471.39) [593]"}
HasDirectPerm(Mask, (loc(a_3, i4): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i4).val (arrayTestChainIrrel3.vpr@471.3--471.39) [594]"}
FullPerm == Mask[(loc(a_3, i4): Ref), val];
Heap := Heap[(loc(a_3, i4): Ref), val:=Heap[(loc(a_3, i4): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell6 -- arrayTestChainIrrel3.vpr@472.3--472.21
_compLabell6:
Label_compLabell6Mask := Mask;
Label_compLabell6Heap := Heap;
_compLabell6_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@473.3--486.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) && (forall __ind_26: int ::
{ __f_10[__ind_26] }
__f_10[__ind_26] ==> NoPerm < Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_26): Ref), val]
)) {
if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@483.45--483.77) [595]"}
(filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) || (forall __ind1_10: int, __ind2_10: int ::
{ __f_10[__ind1_10], __f_10[__ind2_10] }
__f_10[__ind1_10] && (__f_10[__ind2_10] && __ind1_10 != __ind2_10) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind1_10): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind2_10): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@483.45--483.77) [596]"}
(forall __ind_27: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] }
__f_10[__ind_27] && dummyFunction(Heap[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@483.45--483.77) [597]"}
(forall __ind_27: int, __ind_27_1: int ::
{ neverTriggered20(__ind_27), neverTriggered20(__ind_27_1) }
(((__ind_27 != __ind_27_1 && __f_10[__ind_27]) && __f_10[__ind_27_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@483.45--483.77) [598]"}
(forall __ind_27: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] }
__f_10[__ind_27] ==> Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_27: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] }
__f_10[__ind_27] && NoPerm < 1 / 10 ==> qpRange20((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref)) && invRecv20((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref)) == __ind_27
);
assume (forall o_3: Ref ::
{ invRecv20(o_3) }
__f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv20(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv20(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_10, __snap_Int_Int_Int_val(Heap, __c_10, __f_10)): int), (recInv((getreceiver(__c_10): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell5 required to evaluate old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@473.11--486.90) [599]"}
_compLabell5_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell5Mask;
ExhaleWellDef0Heap := Label_compLabell5Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@485.62--486.11) [600]"}
(filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) || (forall __ind1_11: int, __ind2_11: int ::
{ __f_10[__ind1_11], __f_10[__ind2_11] }
__f_10[__ind1_11] && (__f_10[__ind2_11] && __ind1_11 != __ind2_11) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind1_11): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind2_11): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@485.62--486.11) [601]"}
(forall __ind_28: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] }
__f_10[__ind_28] && dummyFunction(Label_compLabell5Heap[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@485.62--486.11) [602]"}
(forall __ind_28: int, __ind_28_1: int ::
{ neverTriggered21(__ind_28), neverTriggered21(__ind_28_1) }
(((__ind_28 != __ind_28_1 && __f_10[__ind_28]) && __f_10[__ind_28_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@485.62--486.11) [603]"}
(forall __ind_28: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] }
__f_10[__ind_28] ==> Label_compLabell5Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_28: int ::
{ (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] }
__f_10[__ind_28] && NoPerm < 1 / 10 ==> qpRange21((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref)) && invRecv21((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref)) == __ind_28
);
assume (forall o_3: Ref ::
{ invRecv21(o_3) }
__f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv21(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv21(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell5Mask[o_3, val] - 1 / 10) && (!(__f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3))) ==> QPMask[o_3, val] == Label_compLabell5Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell5Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell5Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell5Heap, ExhaleHeap, Label_compLabell5Mask);
Label_compLabell5Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_11: (FoldDomainType int int int), __f_11: (Set int) ::
{ (hfoldApply(__c_11, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell5Heap, __c_11, __f_11)), __c_11, __f_11)): int) } { (hfoldApply(__c_11, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_11, __f_11)), __c_11, __f_11)): int) }
(filterReceiverGood(__f_11, (getreceiver(__c_11): ReceiverDomainType int)): bool) && (forall __ind_29: int ::
{ __f_11[__ind_29] }
__f_11[__ind_29] ==> NoPerm < Mask[(recApply((getreceiver(__c_11): ReceiverDomainType int), __ind_29): Ref), val]
) ==> (filterReceiverGood(__f_11, (getreceiver(__c_11): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_11, __snap_Int_Int_Int_val(Heap, __c_11, __f_11)): int), (recInv((getreceiver(__c_11): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_11, __snap_Int_Int_Int_val(Label_compLabell5Heap, __c_11, __f_11)): int), (recInv((getreceiver(__c_11): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i5).val := loc(a, i5).val + 1 -- arrayTestChainIrrel3.vpr@487.3--487.39
// -- Check definedness of loc(a, i5).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i5).val (arrayTestChainIrrel3.vpr@487.3--487.39) [604]"}
HasDirectPerm(Mask, (loc(a_3, i5): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i5).val (arrayTestChainIrrel3.vpr@487.3--487.39) [605]"}
FullPerm == Mask[(loc(a_3, i5): Ref), val];
Heap := Heap[(loc(a_3, i5): Ref), val:=Heap[(loc(a_3, i5): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell7 -- arrayTestChainIrrel3.vpr@488.3--488.21
_compLabell7:
Label_compLabell7Mask := Mask;
Label_compLabell7Heap := Heap;
_compLabell7_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@489.3--502.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) && (forall __ind_31: int ::
{ __f_12[__ind_31] }
__f_12[__ind_31] ==> NoPerm < Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_31): Ref), val]
)) {
if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@499.45--499.77) [606]"}
(filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) || (forall __ind1_12: int, __ind2_12: int ::
{ __f_12[__ind1_12], __f_12[__ind2_12] }
__f_12[__ind1_12] && (__f_12[__ind2_12] && __ind1_12 != __ind2_12) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind1_12): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind2_12): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@499.45--499.77) [607]"}
(forall __ind_32: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] }
__f_12[__ind_32] && dummyFunction(Heap[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@499.45--499.77) [608]"}
(forall __ind_32: int, __ind_32_1: int ::
{ neverTriggered22(__ind_32), neverTriggered22(__ind_32_1) }
(((__ind_32 != __ind_32_1 && __f_12[__ind_32]) && __f_12[__ind_32_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@499.45--499.77) [609]"}
(forall __ind_32: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] }
__f_12[__ind_32] ==> Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_32: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] }
__f_12[__ind_32] && NoPerm < 1 / 10 ==> qpRange22((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref)) && invRecv22((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref)) == __ind_32
);
assume (forall o_3: Ref ::
{ invRecv22(o_3) }
__f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv22(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv22(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_12, __snap_Int_Int_Int_val(Heap, __c_12, __f_12)): int), (recInv((getreceiver(__c_12): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell6 required to evaluate old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@489.11--502.90) [610]"}
_compLabell6_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell6Mask;
ExhaleWellDef0Heap := Label_compLabell6Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@501.62--502.11) [611]"}
(filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) || (forall __ind1_13: int, __ind2_13: int ::
{ __f_12[__ind1_13], __f_12[__ind2_13] }
__f_12[__ind1_13] && (__f_12[__ind2_13] && __ind1_13 != __ind2_13) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind1_13): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind2_13): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@501.62--502.11) [612]"}
(forall __ind_33: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] }
__f_12[__ind_33] && dummyFunction(Label_compLabell6Heap[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@501.62--502.11) [613]"}
(forall __ind_33: int, __ind_33_1: int ::
{ neverTriggered23(__ind_33), neverTriggered23(__ind_33_1) }
(((__ind_33 != __ind_33_1 && __f_12[__ind_33]) && __f_12[__ind_33_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@501.62--502.11) [614]"}
(forall __ind_33: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] }
__f_12[__ind_33] ==> Label_compLabell6Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_33: int ::
{ (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] }
__f_12[__ind_33] && NoPerm < 1 / 10 ==> qpRange23((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref)) && invRecv23((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref)) == __ind_33
);
assume (forall o_3: Ref ::
{ invRecv23(o_3) }
__f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv23(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv23(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell6Mask[o_3, val] - 1 / 10) && (!(__f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3))) ==> QPMask[o_3, val] == Label_compLabell6Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell6Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell6Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell6Heap, ExhaleHeap, Label_compLabell6Mask);
Label_compLabell6Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_13: (FoldDomainType int int int), __f_13: (Set int) ::
{ (hfoldApply(__c_13, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell6Heap, __c_13, __f_13)), __c_13, __f_13)): int) } { (hfoldApply(__c_13, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_13, __f_13)), __c_13, __f_13)): int) }
(filterReceiverGood(__f_13, (getreceiver(__c_13): ReceiverDomainType int)): bool) && (forall __ind_34: int ::
{ __f_13[__ind_34] }
__f_13[__ind_34] ==> NoPerm < Mask[(recApply((getreceiver(__c_13): ReceiverDomainType int), __ind_34): Ref), val]
) ==> (filterReceiverGood(__f_13, (getreceiver(__c_13): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_13, __snap_Int_Int_Int_val(Heap, __c_13, __f_13)): int), (recInv((getreceiver(__c_13): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_13, __snap_Int_Int_Int_val(Label_compLabell6Heap, __c_13, __f_13)): int), (recInv((getreceiver(__c_13): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, j3).val := loc(a, j3).val + 1 -- arrayTestChainIrrel3.vpr@503.3--503.39
// -- Check definedness of loc(a, j3).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j3).val (arrayTestChainIrrel3.vpr@503.3--503.39) [615]"}
HasDirectPerm(Mask, (loc(a_3, j3): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j3).val (arrayTestChainIrrel3.vpr@503.3--503.39) [616]"}
FullPerm == Mask[(loc(a_3, j3): Ref), val];
Heap := Heap[(loc(a_3, j3): Ref), val:=Heap[(loc(a_3, j3): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell8 -- arrayTestChainIrrel3.vpr@504.3--504.21
_compLabell8:
Label_compLabell8Mask := Mask;
Label_compLabell8Heap := Heap;
_compLabell8_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@505.3--518.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) && (forall __ind_36: int ::
{ __f_14[__ind_36] }
__f_14[__ind_36] ==> NoPerm < Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_36): Ref), val]
)) {
if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@515.45--515.77) [617]"}
(filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) || (forall __ind1_14: int, __ind2_14: int ::
{ __f_14[__ind1_14], __f_14[__ind2_14] }
__f_14[__ind1_14] && (__f_14[__ind2_14] && __ind1_14 != __ind2_14) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind1_14): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind2_14): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@515.45--515.77) [618]"}
(forall __ind_37: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] }
__f_14[__ind_37] && dummyFunction(Heap[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@515.45--515.77) [619]"}
(forall __ind_37: int, __ind_37_1: int ::
{ neverTriggered24(__ind_37), neverTriggered24(__ind_37_1) }
(((__ind_37 != __ind_37_1 && __f_14[__ind_37]) && __f_14[__ind_37_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@515.45--515.77) [620]"}
(forall __ind_37: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] }
__f_14[__ind_37] ==> Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_37: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] }
__f_14[__ind_37] && NoPerm < 1 / 10 ==> qpRange24((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref)) && invRecv24((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref)) == __ind_37
);
assume (forall o_3: Ref ::
{ invRecv24(o_3) }
__f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv24(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv24(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_14, __snap_Int_Int_Int_val(Heap, __c_14, __f_14)): int), (recInv((getreceiver(__c_14): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell7 required to evaluate old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@505.11--518.90) [621]"}
_compLabell7_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell7Mask;
ExhaleWellDef0Heap := Label_compLabell7Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@517.62--518.11) [622]"}
(filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) || (forall __ind1_15: int, __ind2_15: int ::
{ __f_14[__ind1_15], __f_14[__ind2_15] }
__f_14[__ind1_15] && (__f_14[__ind2_15] && __ind1_15 != __ind2_15) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind1_15): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind2_15): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@517.62--518.11) [623]"}
(forall __ind_38: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] }
__f_14[__ind_38] && dummyFunction(Label_compLabell7Heap[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@517.62--518.11) [624]"}
(forall __ind_38: int, __ind_38_1: int ::
{ neverTriggered25(__ind_38), neverTriggered25(__ind_38_1) }
(((__ind_38 != __ind_38_1 && __f_14[__ind_38]) && __f_14[__ind_38_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@517.62--518.11) [625]"}
(forall __ind_38: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] }
__f_14[__ind_38] ==> Label_compLabell7Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_38: int ::
{ (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] }
__f_14[__ind_38] && NoPerm < 1 / 10 ==> qpRange25((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref)) && invRecv25((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref)) == __ind_38
);
assume (forall o_3: Ref ::
{ invRecv25(o_3) }
__f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv25(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv25(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell7Mask[o_3, val] - 1 / 10) && (!(__f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3))) ==> QPMask[o_3, val] == Label_compLabell7Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell7Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell7Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell7Heap, ExhaleHeap, Label_compLabell7Mask);
Label_compLabell7Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_15: (FoldDomainType int int int), __f_15: (Set int) ::
{ (hfoldApply(__c_15, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell7Heap, __c_15, __f_15)), __c_15, __f_15)): int) } { (hfoldApply(__c_15, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_15, __f_15)), __c_15, __f_15)): int) }
(filterReceiverGood(__f_15, (getreceiver(__c_15): ReceiverDomainType int)): bool) && (forall __ind_39: int ::
{ __f_15[__ind_39] }
__f_15[__ind_39] ==> NoPerm < Mask[(recApply((getreceiver(__c_15): ReceiverDomainType int), __ind_39): Ref), val]
) ==> (filterReceiverGood(__f_15, (getreceiver(__c_15): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_15, __snap_Int_Int_Int_val(Heap, __c_15, __f_15)): int), (recInv((getreceiver(__c_15): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_15, __snap_Int_Int_Int_val(Label_compLabell7Heap, __c_15, __f_15)): int), (recInv((getreceiver(__c_15): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: loc(a, i6).val := loc(a, i6).val + 1 -- arrayTestChainIrrel3.vpr@519.3--519.39
// -- Check definedness of loc(a, i6).val + 1
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i6).val (arrayTestChainIrrel3.vpr@519.3--519.39) [626]"}
HasDirectPerm(Mask, (loc(a_3, i6): Ref), val);
assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i6).val (arrayTestChainIrrel3.vpr@519.3--519.39) [627]"}
FullPerm == Mask[(loc(a_3, i6): Ref), val];
Heap := Heap[(loc(a_3, i6): Ref), val:=Heap[(loc(a_3, i6): Ref), val] + 1];
assume state(Heap, Mask);
// -- Translating statement: label _compLabell9 -- arrayTestChainIrrel3.vpr@520.3--520.21
_compLabell9:
Label_compLabell9Mask := Mask;
Label_compLabell9Heap := Heap;
_compLabell9_lblGuard := true;
assume state(Heap, Mask);
// -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] ::
// { old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) }
// { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) }
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// (forall __ind: Int ::
// { (__ind in __f) }
// (__ind in __f) ==>
// perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) >
// none) ==>
// (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) &&
// ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int),
// (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool) &&
// (_triggerDeleteKey1(old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c,
// __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@521.3--534.91
assume state(Heap, Mask);
// -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool)))
if (*) {
if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool)) {
if (*) {
assume false;
}
}
if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) && (forall __ind_41: int ::
{ __f_16[__ind_41] }
__f_16[__ind_41] ==> NoPerm < Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_41): Ref), val]
)) {
if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool)) {
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@531.45--531.77) [628]"}
(filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) || (forall __ind1_16: int, __ind2_16: int ::
{ __f_16[__ind1_16], __f_16[__ind2_16] }
__f_16[__ind1_16] && (__f_16[__ind2_16] && __ind1_16 != __ind2_16) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind1_16): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind2_16): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@531.45--531.77) [629]"}
(forall __ind_42: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] }
__f_16[__ind_42] && dummyFunction(Heap[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@531.45--531.77) [630]"}
(forall __ind_42: int, __ind_42_1: int ::
{ neverTriggered26(__ind_42), neverTriggered26(__ind_42_1) }
(((__ind_42 != __ind_42_1 && __f_16[__ind_42]) && __f_16[__ind_42_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@531.45--531.77) [631]"}
(forall __ind_42: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] }
__f_16[__ind_42] ==> Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_42: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] }
__f_16[__ind_42] && NoPerm < 1 / 10 ==> qpRange26((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref)) && invRecv26((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref)) == __ind_42
);
assume (forall o_3: Ref ::
{ invRecv26(o_3) }
__f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv26(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv26(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask);
Heap := ExhaleHeap;
// Stop execution
assume false;
}
if ((_triggerDeleteKey1((hfoldApply(__c_16, __snap_Int_Int_Int_val(Heap, __c_16, __f_16)): int), (recInv((getreceiver(__c_16): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool)) {
assert {:msg " Inhale might fail. Did not reach labelled state _compLabell8 required to evaluate old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@521.11--534.90) [632]"}
_compLabell8_lblGuard;
if (*) {
// Exhale precondition of function application
ExhaleWellDef0Mask := Label_compLabell8Mask;
ExhaleWellDef0Heap := Label_compLabell8Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@533.62--534.11) [633]"}
(filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) || (forall __ind1_17: int, __ind2_17: int ::
{ __f_16[__ind1_17], __f_16[__ind2_17] }
__f_16[__ind1_17] && (__f_16[__ind2_17] && __ind1_17 != __ind2_17) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind1_17): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind2_17): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@533.62--534.11) [634]"}
(forall __ind_43: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] }
__f_16[__ind_43] && dummyFunction(Label_compLabell8Heap[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@533.62--534.11) [635]"}
(forall __ind_43: int, __ind_43_1: int ::
{ neverTriggered27(__ind_43), neverTriggered27(__ind_43_1) }
(((__ind_43 != __ind_43_1 && __f_16[__ind_43]) && __f_16[__ind_43_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@533.62--534.11) [636]"}
(forall __ind_43: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] }
__f_16[__ind_43] ==> Label_compLabell8Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref)
assume (forall __ind_43: int ::
{ (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] }
__f_16[__ind_43] && NoPerm < 1 / 10 ==> qpRange27((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref)) && invRecv27((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref)) == __ind_43
);
assume (forall o_3: Ref ::
{ invRecv27(o_3) }
__f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv27(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(__f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv27(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell8Mask[o_3, val] - 1 / 10) && (!(__f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3))) ==> QPMask[o_3, val] == Label_compLabell8Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> Label_compLabell8Mask[o_3, f_5] == QPMask[o_3, f_5]
);
Label_compLabell8Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(Label_compLabell8Heap, ExhaleHeap, Label_compLabell8Mask);
Label_compLabell8Heap := ExhaleHeap;
// Stop execution
assume false;
}
}
}
}
assume false;
}
assume (forall __c_17: (FoldDomainType int int int), __f_17: (Set int) ::
{ (hfoldApply(__c_17, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell8Heap, __c_17, __f_17)), __c_17, __f_17)): int) } { (hfoldApply(__c_17, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_17, __f_17)), __c_17, __f_17)): int) }
(filterReceiverGood(__f_17, (getreceiver(__c_17): ReceiverDomainType int)): bool) && (forall __ind_44: int ::
{ __f_17[__ind_44] }
__f_17[__ind_44] ==> NoPerm < Mask[(recApply((getreceiver(__c_17): ReceiverDomainType int), __ind_44): Ref), val]
) ==> (filterReceiverGood(__f_17, (getreceiver(__c_17): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_17, __snap_Int_Int_Int_val(Heap, __c_17, __f_17)): int), (recInv((getreceiver(__c_17): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_17, __snap_Int_Int_Int_val(Label_compLabell8Heap, __c_17, __f_17)): int), (recInv((getreceiver(__c_17): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool))
);
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: inhale (js intersection is) == Set[Int]() -- arrayTestChainIrrel3.vpr@535.3--535.44
assume Set#Equal(Set#Intersection(js, vis), (Set#Empty(): Set int));
assume state(Heap, Mask);
assume state(Heap, Mask);
// -- Translating statement: assert (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]),
// __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]),
// add()): Fold[Int, Int, Int]), js)): Int) ==
// old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]),
// __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]),
// add()): Fold[Int, Int, Int]), js)): Int)) +
// 3 -- arrayTestChainIrrel3.vpr@536.3--542.6
ExhaleWellDef0Mask := Mask;
ExhaleWellDef0Heap := Heap;
// -- Check definedness of (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int) == old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int)) + 3
if (*) {
// Exhale precondition of function application
ExhaleWellDef1Mask := ExhaleWellDef0Mask;
ExhaleWellDef1Heap := ExhaleWellDef0Heap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(js, (getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in js), (__ind2 in js) } (__ind1 in js) && ((__ind2 in js) && __ind1 != __ind2) ==> (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@537.35--538.74) [637]"}
(filterReceiverGood(js, (getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int)): bool) || (forall __ind1_18: int, __ind2_18: int ::
{ js[__ind1_18], js[__ind2_18] }
js[__ind1_18] && (js[__ind2_18] && __ind1_18 != __ind2_18) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind1_18): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind2_18): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@537.35--538.74) [638]"}
(forall __ind_45: int ::
{ js[__ind_45] }
js[__ind_45] && dummyFunction(ExhaleWellDef0Heap[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@537.35--538.74) [639]"}
(forall __ind_45: int, __ind_45_1: int ::
{ neverTriggered28(__ind_45), neverTriggered28(__ind_45_1) }
(((__ind_45 != __ind_45_1 && js[__ind_45]) && js[__ind_45_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@537.35--538.74) [640]"}
(forall __ind_45: int ::
{ js[__ind_45] }
js[__ind_45] ==> ExhaleWellDef0Mask[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref)
assume (forall __ind_45: int ::
{ js[__ind_45] }
js[__ind_45] && NoPerm < 1 / 10 ==> qpRange28((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref)) && invRecv28((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref)) == __ind_45
);
assume (forall o_3: Ref ::
{ invRecv28(o_3) }
js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv28(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv28(o_3)): Ref) == o_3 && QPMask[o_3, val] == ExhaleWellDef0Mask[o_3, val] - 1 / 10) && (!(js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3))) ==> QPMask[o_3, val] == ExhaleWellDef0Mask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> ExhaleWellDef0Mask[o_3, f_5] == QPMask[o_3, f_5]
);
ExhaleWellDef0Mask := QPMask;
// Finish exhale
havoc ExhaleHeap;
assume IdenticalOnKnownLocations(ExhaleWellDef0Heap, ExhaleHeap, ExhaleWellDef0Mask);
ExhaleWellDef0Heap := ExhaleHeap;
// Stop execution
assume false;
}
if (*) {
// Exhale precondition of function application
ExhaleWellDef1Mask := oldMask;
ExhaleWellDef1Heap := oldHeap;
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(js, (getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in js), (__ind2 in js) } (__ind1 in js) && ((__ind2 in js) && __ind1 != __ind2) ==> (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@540.35--541.74) [641]"}
(filterReceiverGood(js, (getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int)): bool) || (forall __ind1_19: int, __ind2_19: int ::
{ js[__ind1_19], js[__ind2_19] }
js[__ind1_19] && (js[__ind2_19] && __ind1_19 != __ind2_19) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind1_19): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind2_19): Ref)
);
havoc QPMask;
// -- check that the permission amount is positive
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@540.35--541.74) [642]"}
(forall __ind_46: int ::
{ js[__ind_46] }
js[__ind_46] && dummyFunction(oldHeap[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref), val]) ==> 1 / 10 >= NoPerm
);
// -- check if receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) is injective
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@540.35--541.74) [643]"}
(forall __ind_46: int, __ind_46_1: int ::
{ neverTriggered29(__ind_46), neverTriggered29(__ind_46_1) }
(((__ind_46 != __ind_46_1 && js[__ind_46]) && js[__ind_46_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46_1): Ref)
);
// -- check if sufficient permission is held
assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@540.35--541.74) [644]"}
(forall __ind_46: int ::
{ js[__ind_46] }
js[__ind_46] ==> oldMask[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref), val] >= 1 / 10
);
// -- assumptions for inverse of receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref)
assume (forall __ind_46: int ::
{ js[__ind_46] }
js[__ind_46] && NoPerm < 1 / 10 ==> qpRange29((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref)) && invRecv29((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref)) == __ind_46
);
assume (forall o_3: Ref ::
{ invRecv29(o_3) }
js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv29(o_3)): Ref) == o_3
);
// -- assume permission updates for field val
assume (forall o_3: Ref ::
{ QPMask[o_3, val] }
(js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv29(o_3)): Ref) == o_3 && QPMask[o_3, val] == oldMask[o_3, val]) && (!(js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3))) ==> QPMask[o_3, val] == oldMask[o_3, val])
);
// -- assume permission updates for independent locations
assume (forall o_3: Ref, f_5: (Field A B) ::
{ QPMask[o_3, f_5] }
f_5 != val ==> oldMask[o_3, f_5] == QPMask[o_3, f_5]
);
oldMask := QPMask;
// Finish exhale
// Stop execution
assume false;
}
assert {:msg " Assert might fail. Assertion (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int) == old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int)) + 3 might not hold. (arrayTestChainIrrel3.vpr@536.10--542.6) [645]"}
(hfoldApply((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), __snap_Int_Int_Int_val(Heap, (hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), js)): int) == (hfoldApply((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), __snap_Int_Int_Int_val(oldHeap, (hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), js)): int) + 3;
assume state(Heap, Mask);
}