// 
// Translation of Viper program.
// 
// Date:         2022-09-09 14:22:30
// Tool:         carbon 1.0
// Arguments: :  --z3Exe /home/bobe/Workbench/Tools/vercors_ast/bin/../src/main/universal/deps/unix/z3/bin/z3 --print temp.boogie /home/bobe/PhD/students/Andrej Pistek (2022-06)/Ford-FulkersonAlgorithm/1.0-Lukas-tinker-2-minimized-array-4.vpr
// Dependencies:
//   Boogie , located at /home/bobe/Workbench/Tools/vercors_ast/bin/../src/main/universal/deps/unix/boogie/Boogie.
//   Z3 4.8.6 - 64 bit, located at /home/bobe/Workbench/Tools/vercors_ast/bin/../src/main/universal/deps/unix/z3/bin/z3.
// 

// ==================================================
// Preamble of State module.
// ==================================================

function  state(Heap: HeapType, Mask: MaskType): bool;

// ==================================================
// Preamble of Heap module.
// ==================================================

type Ref;
var Heap: HeapType;
const null: Ref;
type Field A B;
type NormalField;
type HeapType = <A, B> [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<A, B>(f_1: (Field A B)): bool;
function  IsWandField<A, B>(f_1: (Field A B)): bool;
function  getPredicateId<A, B>(f_1: (Field A B)): int;
// Frame all locations with direct permissions
axiom (forall <A, B> 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 <C> 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 <C> 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 <A, B> 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 <C> 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 <C> 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 <A, B> 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 <A, B> 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 = <A, B> [Ref, Field A B]Perm;
var Mask: MaskType;
const ZeroMask: MaskType;
axiom (forall <A, B> o_2: Ref, f_4: (Field A B) ::
  { ZeroMask[o_2, f_4] }
  ZeroMask[o_2, f_4] == NoPerm
);
type PMaskType = <A, B> [Ref, Field A B]bool;
const ZeroPMask: PMaskType;
axiom (forall <A, B> o_2: Ref, f_4: (Field A B) ::
  { ZeroPMask[o_2, f_4] }
  !ZeroPMask[o_2, f_4]
);
function  PredicateMaskField<A>(f_5: (Field A FrameType)): Field A PMaskType;
function  WandMaskField<A>(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 <A, B> 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<A, B>(Mask: MaskType, o_2: Ref, f_4: (Field A B)): bool;
axiom (forall <A, B> 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 <A, B> 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(i1_3: int): bool;
function  neverTriggered2(i1_1: int): bool;
function  neverTriggered3(i1_2: int): bool;
function  neverTriggered4(i1_3: int): bool;
function  neverTriggered5(i1_1: int): bool;
function  neverTriggered6(i1_2: 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;
// ==================================================
// 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;

// ==================================================
// Preamble of Function and predicate module.
// ==================================================

// Function heights (higher height means its body is available earlier):
// - height 1: aloc
// - height 0: matrixValues
const AssumeFunctionsAbove: int;
// Declarations for function framing
type FrameType;
const EmptyFrame: FrameType;
function  FrameFragment<T>(t: T): FrameType;
function  ConditionalFrame(p: Perm, f_6: FrameType): FrameType;
function  dummyFunction<T>(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<A, B>(p: (Field A FrameType), v_1: FrameType, q: (Field B FrameType), w: FrameType): bool;
// Transitivity of InsidePredicate
axiom (forall <A, B, C> 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 <A> p: (Field A FrameType), v_1: FrameType, w: FrameType ::
  { InsidePredicate(p, v_1, p, w) }
  !InsidePredicate(p, v_1, p, w)
);

// ==================================================
// Preamble of Sequence module.
// ==================================================

 // diff 0 implemented (no difference)
 // diff 1 implemented (fixes test5 in sequences.sil)
 // diff 2 implemented (fixes m01 and m03 in quantifiedpermissions/issues/issue_0064)
 // diff 3 implemented (no difference)
 // diff 4 implemented (no difference)
 // diff 5 implemented (fixes colourings0 in sequence-incompletenesses test case)
 // diff 6 implemented (no difference)
 // diff 7 implemented
 // diff 8 implemented (allows for contains triggering, without destroying performance of e.g. functions/linkedlists test case)
 // diff 11 implemented
 // diff 13 implemented, for now (may reduce completeness, but there's a known matching loop when the first drop amount is 0); another option would be to add !=0 as an explicit condition
 // diff 14 implemented: eliminate index over take/drop for trivial cases (to avoid matching loops when e.g. s[i..] == s is known)
 // diff 16 implemented: remove general cases of equality-learning between take/drop/append subsequences; only allow when take/drop are at top level (this affects linkedlists test case)
// START BASICS
type Seq T;

function Seq#Length<T>(Seq T): int;
axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

function Seq#Empty<T>(): Seq T;
axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

function Seq#Singleton<T>(T): Seq T;
//axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);// (diff 2 (old))
axiom (forall<T> t: T :: { Seq#Singleton(t) } Seq#Length(Seq#Singleton(t)) == 1);// (diff 2: changed trigger)

function Seq#Append<T>(Seq T, Seq T): Seq T;
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
s0 != Seq#Empty() && s1 != Seq#Empty() ==> //diff 11: consider removing constraints
  Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));

//axiom (forall<T> s: Seq T :: { Seq#Append(Seq#Empty(),s) } Seq#Append(Seq#Empty(),s) == s); // (diff 11: switched to double-quantified version)
//axiom (forall<T> s: Seq T :: { Seq#Append(s,Seq#Empty()) } Seq#Append(s,Seq#Empty()) == s); // (diff 11: switched to double-quantified version)
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Append(s0,s1) } (s0 == Seq#Empty() ==> Seq#Append(s0,s1) == s1) && (s1 == Seq#Empty() ==> Seq#Append(s0,s1) == s0)); // diff 11: switched to double-quantified version

function Seq#Index<T>(Seq T, int): T;
//axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t); // (diff 2 (old))
axiom (forall<T> t: T :: { Seq#Singleton(t) } Seq#Index(Seq#Singleton(t), 0) == t); // (diff 2: changed trigger)

// END BASICS

// START INDEX-APPEND-UPDATE

// extra addition function used to force equalities into the e-graph
function Seq#Add(int, int) : int;
axiom (forall i: int, j: int :: {Seq#Add(i,j)} Seq#Add(i,j) == i + j);
function Seq#Sub(int, int) : int;
axiom (forall i: int, j: int :: {Seq#Sub(i,j)} Seq#Sub(i,j) == i - j);

// (diff 3 (old))
//axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } // {:weight 25} // AS: dropped weight
//  s0 != Seq#Empty() && s1 != Seq#Empty() ==>
//  ((n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
//  (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0)))));

// (diff 3: split axiom, added constraints, replace arithmetic) // diff 11: consider removing constraints
axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } { Seq#Index(s0, n), Seq#Append(s0,s1) } // AS: added alternative trigger
  (s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= n && n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)));
axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } // term below breaks loops
  s0 != Seq#Empty() && s1 != Seq#Empty() && Seq#Length(s0) <= n && n < Seq#Length(Seq#Append(s0,s1)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s0)),Seq#Length(s0)) == n && Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, Seq#Sub(n,Seq#Length(s0))));
// AS: added "reverse triggering" versions of the axioms
axiom (forall<T> s0: Seq T, s1: Seq T, m: int :: { Seq#Index(s1, m), Seq#Append(s0,s1)}  // m == n-|s0|, n == m + |s0|
  s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m));

function Seq#Update<T>(Seq T, int, T): Seq T;
axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } {Seq#Length(s),Seq#Update(s,i,v)} // (diff 4: added trigger)
  0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) } { Seq#Index(s,n), Seq#Update(s,i,v) }  // (diff 4: added trigger)
  0 <= n && n < Seq#Length(s) ==>
    (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&
    (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));

// END INDEX-APPEND-UPDATE

// START TAKE/DROP

function Seq#Take<T>(s: Seq T, howMany: int): Seq T;
// AS: added triggers
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } { Seq#Take(s,n), Seq#Length(s)} // (diff 7: add trigger)
  (0 <= n ==>
    (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
    (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)))
    &&
   (n < 0 ==> Seq#Length(Seq#Take(s,n)) == 0)); // (diff 7: added case for n < 0)

// ** AS: 2nd of 3 axioms which get instantiated very often in certain problems involving take/drop/append
axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {Seq#Index(s,j), Seq#Take(s,n)} // (diff 0: (was already done)) : add trigger // {:weight 25} // AS: dropped weight
  0 <= j && j < n && j < Seq#Length(s) ==>
    Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } {Seq#Length(s), Seq#Drop(s,n)} // (diff 5: added trigger, exchange arithmetic)
  (0 <= n ==>
    (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
    (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0))
    &&
  (n < 0 ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s)) // (diff 7: added cases for n < 0)
    );

// ** AS: 3rd of 3 axioms which get instantiated very often in certain problems involving take/drop/append
// diff 5 (old)
//axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } // {:weight 25} // AS: dropped weight
//  0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
//    Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
//
// diff already added // diff -1: try removing this axiom and checking effect
//axiom (forall<T> s: Seq T, n: int, k: int :: { Seq#Drop(s,n), Seq#Index(s,k) } // AS: alternative triggering for above axiom
//  0 <= n && n <= k && k < Seq#Length(s) ==>
//    Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k));

// diff 5: split axiom, added triggering case, exhanged arithmetic

axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } // {:weight 25} // AS: dropped weight
  0 < n && 0 <= j && j < Seq#Length(s)-n ==> // diff 14: change 0 <= n to 0 < n
   Seq#Sub(Seq#Add(j,n),n) == j && Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, Seq#Add(j,n)));

axiom (forall<T> s: Seq T, n: int, i: int :: { Seq#Drop(s,n), Seq#Index(s,i) }
  0 < n && n <= i && i < Seq#Length(s) ==> // diff 14: change 0 <= n to 0 < n
  Seq#Add(Seq#Sub(i,n),n) == i && Seq#Index(Seq#Drop(s,n), Seq#Sub(i,n)) == Seq#Index(s, i)); // i = j + n, j = i - n

// (diff 6a: add axioms for the 0 > n case)
//axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } // {:weight 25} // AS: dropped weight
//  n <= 0 && 0 <= j && j < Seq#Length(s) ==> // diff 14: change n < 0 to n <= 0
//    Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j));

// (diff 6a: add axioms for the 0 > n case)
//axiom (forall<T> s: Seq T, n: int, i: int :: { Seq#Drop(s,n), Seq#Index(s,i) }
//  n <= 0 && 0 <= i && i < Seq#Length(s) ==> // diff 14: change n < 0 to n <= 0
//  Seq#Index(Seq#Drop(s,n), i) == Seq#Index(s, i)); // i = j + n, j = i - n

// ** AS: We dropped the weak trigger on this axiom. One option is to strengthen the triggers:
//axiom (forall<T> s, t: Seq T ::
// // { Seq#Append(s, t) }
//  {Seq#Take(Seq#Append(s, t), Seq#Length(s))}{Seq#Drop(Seq#Append(s, t), Seq#Length(s))}
//  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
//  Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

// ** AS: another option is to split the axiom (for some reason, this seems in some cases to perform slightly less well (but this could be random):
//axiom (forall<T> s, t: Seq T ::
// { Seq#Take(Seq#Append(s, t), Seq#Length(s)) }
//  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s);

//axiom (forall<T> s, t: Seq T ::
// { Seq#Drop(Seq#Append(s, t), Seq#Length(s)) }
//  Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

// (diff 6b: remove these?)
/* Removed: at present, Carbon doesn't generate Seq#Update (but desugars via take/drop/append)
// Commutability of Take and Drop with Update.
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
        { Seq#Take(Seq#Update(s, i, v), n) }
//        0 <= i && i < n && n < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
        0 <= i && i < n && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
        { Seq#Take(Seq#Update(s, i, v), n) }
        n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
        { Seq#Drop(Seq#Update(s, i, v), n) }
//        0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
        0 <= i && n <=i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
        { Seq#Drop(Seq#Update(s, i, v), n) }
//        0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
        0 <= i && i < n && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
*/

axiom (forall<T> s: Seq T, t: Seq T, n:int ::
  { Seq#Take(Seq#Append(s,t),n) } //{Seq#Append(s,t), Seq#Take(s,n)} // diff 16: temporarily dropped general case of these
  0 < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Append(s,t),n) == Seq#Take(s,n));

axiom (forall<T> s: Seq T, t: Seq T, n:int ::
  { Seq#Take(Seq#Append(s,t),n) }
  n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Take(Seq#Append(s,t),n) == Seq#Append(s,Seq#Take(t,Seq#Sub(n,Seq#Length(s)))));

// diff 16: temporarily dropped general case of these
//axiom (forall<T> s: Seq T, t: Seq T, m:int ::
//  { Seq#Append(s,Seq#Take(t,m)) } //{Seq#Append(s,t), Seq#Take(t,m)} // diff 16: temporarily dropped general case of these // reverse triggering version of above: m = n - |s|, n = m + |s|
//  m > 0 ==> Seq#Sub(Seq#Add(m,Seq#Length(s)),Seq#Length(s)) == m && Seq#Take(Seq#Append(s,t),Seq#Add(m,Seq#Length(s))) == Seq#Append(s,Seq#Take(t,m)));

axiom (forall<T> s: Seq T, t: Seq T, n:int ::
  { Seq#Drop(Seq#Append(s,t),n) } //{Seq#Append(s,t), Seq#Drop(s,n)} // diff 16: temporarily dropped general case of these
  0<n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Append(s,t),n) == Seq#Append(Seq#Drop(s,n),t));

axiom (forall<T> s: Seq T, t: Seq T, n:int ::
  { Seq#Drop(Seq#Append(s,t),n) }
 n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s))));

// diff 16: temporarily dropped general case of these
//axiom (forall<T> s: Seq T, t: Seq T, m:int ::
//  { Seq#Append(s,t),Seq#Drop(t,m) } // reverse triggering version of above: m = n - |s|, n = m + |s|
//  m > 0 ==> Seq#Sub(Seq#Add(m,Seq#Length(s)),Seq#Length(s)) == m && Seq#Drop(Seq#Append(s,t),Seq#Add(m,Seq#Length(s))) == Seq#Drop(t,m));

// Additional axioms about common things
axiom (forall<T> s: Seq T, n: int :: { Seq#Drop(s, n) } // ** NEW
        n <= 0 ==> Seq#Drop(s, n) == s); // (diff 1: try changing n==0 to n<=0 (should be ok))
axiom (forall<T> s: Seq T, n: int :: { Seq#Take(s, n) } // ** NEW
        n <= 0 ==> Seq#Take(s, n) == Seq#Empty());  // (diff 1: try changing n==0 to n<=0 (should be ok))
// diff 13: remove this?
//axiom (forall<T> s: Seq T, m, n: int :: { Seq#Drop(Seq#Drop(s, m), n) } // ** NEW - AS: could have bad triggering behaviour?
//        0 <= m && 0 <= n && m+n <= Seq#Length(s) ==>
//        Seq#Sub(Seq#Add(m,n),n) == m && Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, Seq#Add(m,n)));

// END TAKE/DROP

// START CONTAINS
// diff 8: skolemisation (old)
function Seq#Contains<T>(Seq T, T): bool;
function Seq#ContainsTrigger<T>(Seq T, T): bool; // usages of Contains inside quantifier triggers are replaced with this
function Seq#Skolem<T>(Seq T, T) : int; // skolem function for Seq#Contains // (diff 8: added)
axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
  Seq#Contains(s,x) ==>
    (0 <= Seq#Skolem(s,x) && Seq#Skolem(s,x) < Seq#Length(s) && Seq#Index(s,Seq#Skolem(s,x)) == x)); // (diff 8: skolem function)
axiom (forall<T> s: Seq T, x: T, i:int :: { Seq#Contains(s,x), Seq#Index(s,i) } // only trigger if interested in the Contains term
    (0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x ==> Seq#Contains(s,x)));
axiom (forall<T> s: Seq T, i:int :: { Seq#Index(s,i) }
  (0 <= i && i < Seq#Length(s) ==> Seq#ContainsTrigger(s,Seq#Index(s,i))));
// ** AS: made one change here - changed type of x from ref to T
/*axiom (forall<T> x: T ::
  { Seq#Contains(Seq#Empty(), x) }
  !Seq#Contains(Seq#Empty(), x));
axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
  { Seq#Contains(Seq#Append(s0, s1), x) }
  Seq#Contains(Seq#Append(s0, s1), x) <==>
    Seq#Contains(s0, x) || Seq#Contains(s1, x));

axiom (forall<T> s: Seq T, n: int, x: T ::
  { Seq#Contains(Seq#Take(s, n), x) }
  Seq#Contains(Seq#Take(s, n), x) <==>
    (exists i: int :: { Seq#Index(s, i) }
      0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
axiom (forall<T> s: Seq T, n: int, x: T ::
  { Seq#Contains(Seq#Drop(s, n), x) }
  Seq#Contains(Seq#Drop(s, n), x) <==>
    (exists i: int :: { Seq#Index(s, i) }
      0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
*/
// diff 8: skolemisation (new)
/*
function Seq#Skolem<T>(Seq T, T) : int; // skolem function for Seq#Contains
function Seq#SkolemContainsDrop<T>(Seq T, int, T) : int; // skolem function for Seq#Contains over drop
function Seq#SkolemContainsTake<T>(Seq T, int, T) : int; // skolem function for Seq#Contains over take

function Seq#Contains<T>(Seq T, T): bool;
axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
  Seq#Contains(s,x) ==> s != Seq#Empty() && Seq#Length(s) > 0 && 0 <= Seq#Skolem(s,x) &&
    Seq#Skolem(s,x) < Seq#Length(s) && Seq#Index(s,Seq#Skolem(s,x)) == x);

// AS: note: this is an unusual axiom, but is basically the original
// Consider writing a version without the (precise) first trigger? Also see later versions
axiom (forall<T> s: Seq T, x: T, i:int :: { Seq#Contains(s,x), Seq#Index(s,i) }
  0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x ==> Seq#Contains(s,x));

// ** AS: made one change here - changed type of x from ref to T
axiom (forall<T> x: T ::
  { Seq#Contains(Seq#Empty(), x) }
  !Seq#Contains(Seq#Empty(), x));

// AS: Consider dropping this axiom?
axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
  { Seq#Contains(Seq#Append(s0, s1), x) } { Seq#Contains(s0,x), Seq#Append(s0,s1)} { Seq#Contains(s1,x), Seq#Append(s0,s1)} // AS: added triggers
  Seq#Contains(Seq#Append(s0, s1), x) <==>
    Seq#Contains(s0, x) || Seq#Contains(s1, x));

// AS: split axioms
axiom (forall<T> s: Seq T, n: int, x: T ::
  { Seq#Contains(Seq#Take(s, n), x) }
  Seq#Contains(Seq#Take(s, n), x) ==>
    (Seq#Take(s, n) != Seq#Empty() && Seq#Length(Seq#Take(s, n)) > 0 &&
     0 <= Seq#SkolemContainsTake(s, n, x) && Seq#SkolemContainsTake(s, n, x) < n &&
      Seq#SkolemContainsTake(s, n, x) < Seq#Length(s) &&
      Seq#Index(s, Seq#SkolemContainsTake(s, n, x)) == x));

axiom (forall<T> s: Seq T, n: int, x: T, i:int ::
  { Seq#Contains(Seq#Take(s, n), x), Seq#Index(s, i) }
    0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x ==>
     Seq#Contains(Seq#Take(s, n), x));

// AS: split axioms
axiom (forall<T> s: Seq T, n: int, x: T ::
  { Seq#Contains(Seq#Drop(s, n), x) }
  Seq#Contains(Seq#Drop(s, n), x) ==>
    ( 0 <= Seq#SkolemContainsDrop(s, n, x) && n <= Seq#SkolemContainsDrop(s, n, x) &&
      Seq#SkolemContainsDrop(s, n, x) < Seq#Length(s) &&
      Seq#Index(s, Seq#SkolemContainsDrop(s, n, x)) == x));

axiom (forall<T> s: Seq T, n: int, x: T, i:int ::
  { Seq#Contains(Seq#Drop(s, n), x), Seq#Index(s, i) }
  0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x ==>
  Seq#Contains(Seq#Drop(s, n), x));
*/

// END CONTAINS

// START EQUALS

// diff 9 : skolemise equals (old)
function Seq#Equal<T>(Seq T, Seq T): bool;
/*axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
  Seq#Equal(s0,s1) <==>
    Seq#Length(s0) == Seq#Length(s1) &&
    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences
  Seq#Equal(a,b) ==> a == b);
*/
// diff 9: skolemise equals (new)
// AS: split axiom
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
  Seq#Equal(s0,s1) ==>
    Seq#Length(s0) == Seq#Length(s1) &&
    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));

function Seq#SkolemDiff<T>(Seq T, Seq T) : int; // skolem function for Seq#Equals

axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
  (s0==s1 && Seq#Equal(s0,s1)) || (s0!=s1 && !Seq#Equal(s0,s1) && Seq#Length(s0) != Seq#Length(s1)) ||
        (s0 != s1 && !Seq#Equal(s0,s1) && Seq#Length(s0) == Seq#Length(s1) && Seq#SkolemDiff(s0,s1) == Seq#SkolemDiff(s1,s0) && 0 <= Seq#SkolemDiff(s0,s1) && Seq#SkolemDiff(s0,s1) < Seq#Length(s0) &&
         Seq#Index(s0,Seq#SkolemDiff(s0,s1)) != Seq#Index(s1,Seq#SkolemDiff(s0,s1))));

axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) }  // extensionality axiom for sequences
  Seq#Equal(a,b) ==> a == b);


// END EQUALS


// START EXTRAS

// extra stuff not in current Dafny Prelude

// diff 10: variant of trigger (maybe drop these?)
// old:
axiom (forall<T> x, y: T ::
  { Seq#Contains(Seq#Singleton(x),y) }
    Seq#Contains(Seq#Singleton(x),y) <==> x==y);
// new:
/*axiom (forall<T> x, y: T ::
  { Seq#Contains(Seq#Singleton(x),y) }
    Seq#Contains(Seq#Singleton(x),y) ==> x==y);

axiom (forall<T> x: T ::
  { Seq#Singleton(x) }
    Seq#Contains(Seq#Singleton(x),x));
*/

function Seq#Range(min: int, max: int) returns (Seq int);
axiom (forall min: int, max: int :: { Seq#Length(Seq#Range(min, max)) } (min < max ==> Seq#Length(Seq#Range(min, max)) == max-min) && (max <= min ==> Seq#Length(Seq#Range(min, max)) == 0));
axiom (forall min: int, max: int, j: int :: { Seq#Index(Seq#Range(min, max), j) } 0<=j && j<max-min ==> Seq#Index(Seq#Range(min, max), j) == min + j);

axiom (forall min: int, max: int, v: int :: {Seq#Contains(Seq#Range(min, max),v)}
  (Seq#Contains(Seq#Range(min, max),v) <==> min <= v && v < max));

// END EXTRAS


// ==================================================
// Translation of domain array
// ==================================================

// The type for domain array
type arrayDomainType;

// Translation of domain function array_loc
function  array_loc(a_2: arrayDomainType, i: int): Ref;

// Translation of domain function alen
function  alen(a1: arrayDomainType): int;

// Translation of domain function loc_inv_1
function  loc_inv_1(loc: Ref): arrayDomainType;

// Translation of domain function loc_inv_2
function  loc_inv_2(loc1: Ref): int;

// Translation of anonymous domain axiom
axiom (forall a2: arrayDomainType ::
  
  (forall i1: int ::
    { (array_loc(a2, i1): Ref) }
    (loc_inv_1((array_loc(a2, i1): Ref)): arrayDomainType) == a2 && (loc_inv_2((array_loc(a2, i1): Ref)): int) == i1
  )
);

// Translation of anonymous domain axiom
axiom (forall a2: arrayDomainType ::
  { (alen(a2): int) }
  (alen(a2): int) >= 0
);

// ==================================================
// Translation of all fields
// ==================================================

const unique oa: Field NormalField arrayDomainType;
axiom !IsPredicateField(oa);
axiom !IsWandField(oa);
const unique vint: Field NormalField int;
axiom !IsPredicateField(vint);
axiom !IsWandField(vint);

// ==================================================
// Translation of function aloc
// ==================================================

// Uninterpreted function definitions
function  aloc(Heap: HeapType, a2: arrayDomainType, i1: int): Ref;
function  aloc'(Heap: HeapType, a2: arrayDomainType, i1: int): Ref;
axiom (forall Heap: HeapType, a2: arrayDomainType, i1: int ::
  { aloc(Heap, a2, i1) }
  aloc(Heap, a2, i1) == aloc'(Heap, a2, i1) && dummyFunction(aloc#triggerStateless(a2, i1))
);
axiom (forall Heap: HeapType, a2: arrayDomainType, i1: int ::
  { aloc'(Heap, a2, i1) }
  dummyFunction(aloc#triggerStateless(a2, i1))
);

// Definitional axiom
axiom (forall Heap: HeapType, Mask: MaskType, a2: arrayDomainType, i1: int ::
  { state(Heap, Mask), aloc(Heap, a2, i1) }
  state(Heap, Mask) && AssumeFunctionsAbove < 1 ==> 0 <= i1 && i1 < (alen(a2): int) ==> aloc(Heap, a2, i1) == (array_loc(a2, i1): Ref)
);

// Framing axioms
function  aloc#frame(frame: FrameType, a2: arrayDomainType, i1: int): Ref;
axiom (forall Heap: HeapType, Mask: MaskType, a2: arrayDomainType, i1: int ::
  { state(Heap, Mask), aloc'(Heap, a2, i1) }
  state(Heap, Mask) ==> aloc'(Heap, a2, i1) == aloc#frame(EmptyFrame, a2, i1)
);

// Postcondition axioms
axiom (forall Heap: HeapType, Mask: MaskType, a2: arrayDomainType, i1: int ::
  { state(Heap, Mask), aloc'(Heap, a2, i1) }
  state(Heap, Mask) && (AssumeFunctionsAbove < 1 || aloc#trigger(EmptyFrame, a2, i1)) ==> 0 <= i1 && i1 < (alen(a2): int) ==> (loc_inv_1(aloc'(Heap, a2, i1)): arrayDomainType) == a2
);
axiom (forall Heap: HeapType, Mask: MaskType, a2: arrayDomainType, i1: int ::
  { state(Heap, Mask), aloc'(Heap, a2, i1) }
  state(Heap, Mask) && (AssumeFunctionsAbove < 1 || aloc#trigger(EmptyFrame, a2, i1)) ==> 0 <= i1 && i1 < (alen(a2): int) ==> (loc_inv_2(aloc'(Heap, a2, i1)): int) == i1
);

// Trigger function (controlling recursive postconditions)
function  aloc#trigger(frame: FrameType, a2: arrayDomainType, i1: int): bool;

// State-independent trigger function
function  aloc#triggerStateless(a2: arrayDomainType, i1: int): Ref;

// Check contract well-formedness and postcondition
procedure aloc#definedness(a2: arrayDomainType, i1: int) returns (Result: Ref)
  modifies Heap, Mask;
{
  
  // -- Initializing the state
    Mask := ZeroMask;
    assume state(Heap, Mask);
    assume AssumeFunctionsAbove == 1;
  
  // -- Initializing the old state
    assume Heap == old(Heap);
    assume Mask == old(Mask);
  
  // -- Inhaling precondition (with checking)
    assume 0 <= i1;
    assume state(Heap, Mask);
    assume i1 < (alen(a2): int);
    assume state(Heap, Mask);
  
  // -- Translate function body
    Result := (array_loc(a2, i1): Ref);
  
  // -- Exhaling postcondition (with checking)
    assert {:msg "  Postcondition of aloc might not hold. Assertion loc_inv_1(result) == a2 might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@31.11--31.34) [127]"}
      (loc_inv_1(Result): arrayDomainType) == a2;
    assert {:msg "  Postcondition of aloc might not hold. Assertion loc_inv_2(result) == i1 might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@32.11--32.34) [128]"}
      (loc_inv_2(Result): int) == i1;
}

// ==================================================
// Translation of function matrixValues
// ==================================================

// Uninterpreted function definitions
function  matrixValues(Heap: HeapType, a2: arrayDomainType, V: int): Seq (Seq int);
function  matrixValues'(Heap: HeapType, a2: arrayDomainType, V: int): Seq (Seq int);
axiom (forall Heap: HeapType, a2: arrayDomainType, V: int ::
  { matrixValues(Heap, a2, V) }
  matrixValues(Heap, a2, V) == matrixValues'(Heap, a2, V) && dummyFunction(matrixValues#triggerStateless(a2, V))
);
axiom (forall Heap: HeapType, a2: arrayDomainType, V: int ::
  { matrixValues'(Heap, a2, V) }
  dummyFunction(matrixValues#triggerStateless(a2, V))
);

// Framing axioms
function  matrixValues#frame(frame: FrameType, a2: arrayDomainType, V: int): Seq (Seq int);
axiom (forall Heap: HeapType, Mask: MaskType, a2: arrayDomainType, V: int ::
  { state(Heap, Mask), matrixValues'(Heap, a2, V) }
  state(Heap, Mask) ==> matrixValues'(Heap, a2, V) == matrixValues#frame(FrameFragment(matrixValues#condqp1(Heap, a2, V)), a2, V)
);
// ==================================================
// Function used for framing of quantified permission (forall i1: Int :: { aloc(a2, i1).oa } 0 <= i1 && i1 < V ==> acc(aloc(a2, i1).oa, 1 / 2)) in function matrixValues
// ==================================================

function  matrixValues#condqp1(Heap: HeapType, a2_1_1: arrayDomainType, V_1_1: int): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, a2: arrayDomainType, V: int ::
  { matrixValues#condqp1(Heap2Heap, a2, V), matrixValues#condqp1(Heap1Heap, a2, V), succHeapTrans(Heap2Heap, Heap1Heap) }
  (forall i1: int ::
    
    ((0 <= i1 && i1 < V) && NoPerm < 1 / 2 <==> (0 <= i1 && i1 < V) && NoPerm < 1 / 2) && ((0 <= i1 && i1 < V) && NoPerm < 1 / 2 ==> Heap2Heap[aloc(Heap2Heap, a2, i1), oa] == Heap1Heap[aloc(Heap1Heap, a2, i1), oa])
  ) ==> matrixValues#condqp1(Heap2Heap, a2, V) == matrixValues#condqp1(Heap1Heap, a2, V)
);

// Trigger function (controlling recursive postconditions)
function  matrixValues#trigger(frame: FrameType, a2: arrayDomainType, V: int): bool;

// State-independent trigger function
function  matrixValues#triggerStateless(a2: arrayDomainType, V: int): Seq (Seq int);

// Check contract well-formedness and postcondition
procedure matrixValues#definedness(a2: arrayDomainType, V: int) returns (Result: (Seq (Seq int)))
  modifies Heap, Mask;
{
  var i1_4: int;
  var QPMask: MaskType;
  
  // -- Initializing the state
    Mask := ZeroMask;
    assume state(Heap, Mask);
    assume AssumeFunctionsAbove == 0;
  
  // -- Initializing the old state
    assume Heap == old(Heap);
    assume Mask == old(Mask);
  
  // -- Inhaling precondition (with checking)
    assume (alen(a2): int) == V;
    assume state(Heap, Mask);
    
    // -- Check definedness of (forall i1: Int :: { aloc(a2, i1).oa } 0 <= i1 && i1 < V ==> acc(aloc(a2, i1).oa, 1 / 2))
      if (*) {
        if (0 <= i1_4 && i1_4 < V) {
          if (*) {
            // Exhale precondition of function application
            assert {:msg "  Precondition of function aloc might not hold. Assertion 0 <= i1 might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@39.75--39.87) [129]"}
              0 <= i1_4;
            assert {:msg "  Precondition of function aloc might not hold. Assertion i1 < alen(a2) might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@39.75--39.87) [130]"}
              i1_4 < (alen(a2): int);
            // Stop execution
            assume false;
          }
        }
        assume false;
      }
      assume state(Heap, Mask);
    assume state(Heap, Mask);
    havoc QPMask;
    assert {:msg "  Contract might not be well-formed. Quantified resource aloc(a2, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@39.13--39.96) [131]"}
      (forall i1_3: int, i1_3_1: int ::
      
      (((i1_3 != i1_3_1 && (0 <= i1_3 && i1_3 < V)) && (0 <= i1_3_1 && i1_3_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, a2, i1_3) != aloc(Heap, a2, i1_3_1)
    );
    
    // -- Define Inverse Function
      assume (forall i1_3: int ::
        { aloc(Heap, a2, i1_3) } { Heap[aloc(Heap, a2, i1_3), oa] }
        (0 <= i1_3 && i1_3 < V) && NoPerm < 1 / 2 ==> qpRange1(aloc(Heap, a2, i1_3)) && invRecv1(aloc(Heap, a2, i1_3)) == i1_3
      );
      assume (forall o_3: Ref ::
        { invRecv1(o_3) }
        ((0 <= invRecv1(o_3) && invRecv1(o_3) < V) && NoPerm < 1 / 2) && qpRange1(o_3) ==> aloc(Heap, a2, invRecv1(o_3)) == o_3
      );
    // Check that permission expression is non-negative for all fields
    assert {:msg "  Contract might not be well-formed. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@39.13--39.96) [132]"}
      (forall i1_3: int ::
      { aloc(Heap, a2, i1_3) } { Heap[aloc(Heap, a2, i1_3), oa] }
      0 <= i1_3 && i1_3 < V ==> 1 / 2 >= NoPerm
    );
    
    // -- Assume set of fields is nonNull
      assume (forall i1_3: int ::
        { aloc(Heap, a2, i1_3) } { Heap[aloc(Heap, a2, i1_3), oa] }
        (0 <= i1_3 && i1_3 < V) && 1 / 2 > NoPerm ==> aloc(Heap, a2, i1_3) != null
      );
    
    // -- Define permissions
      assume (forall o_3: Ref ::
        { QPMask[o_3, oa] }
        (((0 <= invRecv1(o_3) && invRecv1(o_3) < V) && NoPerm < 1 / 2) && qpRange1(o_3) ==> (NoPerm < 1 / 2 ==> aloc(Heap, a2, invRecv1(o_3)) == o_3) && QPMask[o_3, oa] == Mask[o_3, oa] + 1 / 2) && (!(((0 <= invRecv1(o_3) && invRecv1(o_3) < V) && NoPerm < 1 / 2) && qpRange1(o_3)) ==> QPMask[o_3, oa] == Mask[o_3, oa])
      );
      assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
        { Mask[o_3, f_5] } { QPMask[o_3, f_5] }
        f_5 != oa ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
      );
    Mask := QPMask;
    assume state(Heap, Mask);
    assume state(Heap, Mask);
}

// ==================================================
// Translation of method maxFlowInline
// ==================================================

procedure maxFlowInline(tid: int, G: arrayDomainType, V: int) returns (exc: Ref, res: int)
  modifies Heap, Mask;
{
  var i1_5: int;
  var QPMask: MaskType;
  var ExhaleHeap: HeapType;
  
  // -- Initializing the state
    Mask := ZeroMask;
    assume state(Heap, Mask);
    assume AssumeFunctionsAbove == -1;
  
  // -- Checked inhaling of precondition
    assume (alen(G): int) == V;
    assume state(Heap, Mask);
    
    // -- Check definedness of (forall i1: Int :: { aloc(G, i1).oa } 0 <= i1 && i1 < V ==> acc(aloc(G, i1).oa, 1 / 2))
      if (*) {
        if (0 <= i1_5 && i1_5 < V) {
          if (*) {
            // Exhale precondition of function application
            assert {:msg "  Precondition of function aloc might not hold. Assertion 0 <= i1 might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@43.74--43.85) [133]"}
              0 <= i1_5;
            assert {:msg "  Precondition of function aloc might not hold. Assertion i1 < alen(G) might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@43.74--43.85) [134]"}
              i1_5 < (alen(G): int);
            // Stop execution
            assume false;
          }
        }
        assume false;
      }
      assume state(Heap, Mask);
    assume state(Heap, Mask);
    havoc QPMask;
    assert {:msg "  Contract might not be well-formed. Quantified resource aloc(G, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@43.13--43.94) [135]"}
      (forall i1_1: int, i1_1_1: int ::
      
      (((i1_1 != i1_1_1 && (0 <= i1_1 && i1_1 < V)) && (0 <= i1_1_1 && i1_1_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, G, i1_1) != aloc(Heap, G, i1_1_1)
    );
    
    // -- Define Inverse Function
      assume (forall i1_1: int ::
        { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
        (0 <= i1_1 && i1_1 < V) && NoPerm < 1 / 2 ==> qpRange2(aloc(Heap, G, i1_1)) && invRecv2(aloc(Heap, G, i1_1)) == i1_1
      );
      assume (forall o_3: Ref ::
        { invRecv2(o_3) }
        ((0 <= invRecv2(o_3) && invRecv2(o_3) < V) && NoPerm < 1 / 2) && qpRange2(o_3) ==> aloc(Heap, G, invRecv2(o_3)) == o_3
      );
    // Check that permission expression is non-negative for all fields
    assert {:msg "  Contract might not be well-formed. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@43.13--43.94) [136]"}
      (forall i1_1: int ::
      { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
      0 <= i1_1 && i1_1 < V ==> 1 / 2 >= NoPerm
    );
    
    // -- Assume set of fields is nonNull
      assume (forall i1_1: int ::
        { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
        (0 <= i1_1 && i1_1 < V) && 1 / 2 > NoPerm ==> aloc(Heap, G, i1_1) != null
      );
    
    // -- Define permissions
      assume (forall o_3: Ref ::
        { QPMask[o_3, oa] }
        (((0 <= invRecv2(o_3) && invRecv2(o_3) < V) && NoPerm < 1 / 2) && qpRange2(o_3) ==> (NoPerm < 1 / 2 ==> aloc(Heap, G, invRecv2(o_3)) == o_3) && QPMask[o_3, oa] == Mask[o_3, oa] + 1 / 2) && (!(((0 <= invRecv2(o_3) && invRecv2(o_3) < V) && NoPerm < 1 / 2) && qpRange2(o_3)) ==> QPMask[o_3, oa] == Mask[o_3, oa])
      );
      assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
        { Mask[o_3, f_5] } { QPMask[o_3, f_5] }
        f_5 != oa ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
      );
    Mask := QPMask;
    assume state(Heap, Mask);
    assume state(Heap, Mask);
    
    // -- Check definedness of matrixValues(G, V) == matrixValues(G, V)
      if (*) {
        // Exhale precondition of function application
        assert {:msg "  Precondition of function matrixValues might not hold. Assertion alen(G) == V might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.12--44.30) [137]"}
          (alen(G): int) == V;
        havoc QPMask;
        
        // -- check that the permission amount is positive
          assert {:msg "  Precondition of function matrixValues might not hold. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.12--44.30) [138]"}
            (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            (0 <= i1_2 && i1_2 < V) && dummyFunction(Heap[aloc(Heap, G, i1_2), oa]) ==> 1 / 2 >= NoPerm
          );
        
        // -- check if receiver aloc(G, i1) is injective
          assert {:msg "  Precondition of function matrixValues might not hold. Quantified resource aloc(G, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.12--44.30) [139]"}
            (forall i1_2: int, i1_2_1: int ::
            { neverTriggered3(i1_2), neverTriggered3(i1_2_1) }
            (((i1_2 != i1_2_1 && (0 <= i1_2 && i1_2 < V)) && (0 <= i1_2_1 && i1_2_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, G, i1_2) != aloc(Heap, G, i1_2_1)
          );
        
        // -- check if sufficient permission is held
          assert {:msg "  Precondition of function matrixValues might not hold. There might be insufficient permission to access aloc(G, i1).oa (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.12--44.30) [140]"}
            (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            0 <= i1_2 && i1_2 < V ==> Mask[aloc(Heap, G, i1_2), oa] >= 1 / 2
          );
        
        // -- assumptions for inverse of receiver aloc(G, i1)
          assume (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            (0 <= i1_2 && i1_2 < V) && NoPerm < 1 / 2 ==> qpRange3(aloc(Heap, G, i1_2)) && invRecv3(aloc(Heap, G, i1_2)) == i1_2
          );
          assume (forall o_3: Ref ::
            { invRecv3(o_3) }
            (0 <= invRecv3(o_3) && invRecv3(o_3) < V) && (NoPerm < 1 / 2 && qpRange3(o_3)) ==> aloc(Heap, G, invRecv3(o_3)) == o_3
          );
        
        // -- assume permission updates for field oa
          assume (forall o_3: Ref ::
            { QPMask[o_3, oa] }
            ((0 <= invRecv3(o_3) && invRecv3(o_3) < V) && (NoPerm < 1 / 2 && qpRange3(o_3)) ==> aloc(Heap, G, invRecv3(o_3)) == o_3 && QPMask[o_3, oa] == Mask[o_3, oa] - 1 / 2) && (!((0 <= invRecv3(o_3) && invRecv3(o_3) < V) && (NoPerm < 1 / 2 && qpRange3(o_3))) ==> QPMask[o_3, oa] == Mask[o_3, oa])
          );
        
        // -- assume permission updates for independent locations
          assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
            { QPMask[o_3, f_5] }
            f_5 != oa ==> 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
        assert {:msg "  Precondition of function matrixValues might not hold. Assertion alen(G) == V might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.34--44.52) [141]"}
          (alen(G): int) == V;
        havoc QPMask;
        
        // -- check that the permission amount is positive
          assert {:msg "  Precondition of function matrixValues might not hold. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.34--44.52) [142]"}
            (forall i1_3: int ::
            { aloc(Heap, G, i1_3) } { Heap[aloc(Heap, G, i1_3), oa] }
            (0 <= i1_3 && i1_3 < V) && dummyFunction(Heap[aloc(Heap, G, i1_3), oa]) ==> 1 / 2 >= NoPerm
          );
        
        // -- check if receiver aloc(G, i1) is injective
          assert {:msg "  Precondition of function matrixValues might not hold. Quantified resource aloc(G, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.34--44.52) [143]"}
            (forall i1_3: int, i1_3_1: int ::
            { neverTriggered4(i1_3), neverTriggered4(i1_3_1) }
            (((i1_3 != i1_3_1 && (0 <= i1_3 && i1_3 < V)) && (0 <= i1_3_1 && i1_3_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, G, i1_3) != aloc(Heap, G, i1_3_1)
          );
        
        // -- check if sufficient permission is held
          assert {:msg "  Precondition of function matrixValues might not hold. There might be insufficient permission to access aloc(G, i1).oa (1.0-Lukas-tinker-2-minimized-array-4.vpr@44.34--44.52) [144]"}
            (forall i1_3: int ::
            { aloc(Heap, G, i1_3) } { Heap[aloc(Heap, G, i1_3), oa] }
            0 <= i1_3 && i1_3 < V ==> Mask[aloc(Heap, G, i1_3), oa] >= 1 / 2
          );
        
        // -- assumptions for inverse of receiver aloc(G, i1)
          assume (forall i1_3: int ::
            { aloc(Heap, G, i1_3) } { Heap[aloc(Heap, G, i1_3), oa] }
            (0 <= i1_3 && i1_3 < V) && NoPerm < 1 / 2 ==> qpRange4(aloc(Heap, G, i1_3)) && invRecv4(aloc(Heap, G, i1_3)) == i1_3
          );
          assume (forall o_3: Ref ::
            { invRecv4(o_3) }
            (0 <= invRecv4(o_3) && invRecv4(o_3) < V) && (NoPerm < 1 / 2 && qpRange4(o_3)) ==> aloc(Heap, G, invRecv4(o_3)) == o_3
          );
        
        // -- assume permission updates for field oa
          assume (forall o_3: Ref ::
            { QPMask[o_3, oa] }
            ((0 <= invRecv4(o_3) && invRecv4(o_3) < V) && (NoPerm < 1 / 2 && qpRange4(o_3)) ==> aloc(Heap, G, invRecv4(o_3)) == o_3 && QPMask[o_3, oa] == Mask[o_3, oa] - 1 / 2) && (!((0 <= invRecv4(o_3) && invRecv4(o_3) < V) && (NoPerm < 1 / 2 && qpRange4(o_3))) ==> QPMask[o_3, oa] == Mask[o_3, oa])
          );
        
        // -- assume permission updates for independent locations
          assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
            { QPMask[o_3, f_5] }
            f_5 != oa ==> 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 state(Heap, Mask);
    assume state(Heap, Mask);
    assume Seq#Equal(matrixValues(Heap, G, V), matrixValues(Heap, G, V));
    assume state(Heap, Mask);
  
  // -- Initializing of old state
    
    // -- Initializing the old state
      assume Heap == old(Heap);
      assume Mask == old(Mask);
  
  // -- Translating statement: inhale false -- <no position>
    assume false;
    assume state(Heap, Mask);
    assume state(Heap, Mask);
}

// ==================================================
// Translation of method maxFlowLet
// ==================================================

procedure maxFlowLet(tid: int, G: arrayDomainType, V: int, mv: (Seq (Seq int))) returns (exc: Ref, res: int)
  modifies Heap, Mask;
{
  var i1_6: int;
  var QPMask: MaskType;
  var ExhaleHeap: HeapType;
  
  // -- Initializing the state
    Mask := ZeroMask;
    assume state(Heap, Mask);
    assume AssumeFunctionsAbove == -1;
  
  // -- Checked inhaling of precondition
    assume (alen(G): int) == V;
    assume state(Heap, Mask);
    
    // -- Check definedness of (forall i1: Int :: { aloc(G, i1).oa } 0 <= i1 && i1 < V ==> acc(aloc(G, i1).oa, 1 / 2))
      if (*) {
        if (0 <= i1_6 && i1_6 < V) {
          if (*) {
            // Exhale precondition of function application
            assert {:msg "  Precondition of function aloc might not hold. Assertion 0 <= i1 might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@48.74--48.85) [145]"}
              0 <= i1_6;
            assert {:msg "  Precondition of function aloc might not hold. Assertion i1 < alen(G) might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@48.74--48.85) [146]"}
              i1_6 < (alen(G): int);
            // Stop execution
            assume false;
          }
        }
        assume false;
      }
      assume state(Heap, Mask);
    assume state(Heap, Mask);
    havoc QPMask;
    assert {:msg "  Contract might not be well-formed. Quantified resource aloc(G, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@48.13--48.94) [147]"}
      (forall i1_1: int, i1_1_1: int ::
      
      (((i1_1 != i1_1_1 && (0 <= i1_1 && i1_1 < V)) && (0 <= i1_1_1 && i1_1_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, G, i1_1) != aloc(Heap, G, i1_1_1)
    );
    
    // -- Define Inverse Function
      assume (forall i1_1: int ::
        { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
        (0 <= i1_1 && i1_1 < V) && NoPerm < 1 / 2 ==> qpRange5(aloc(Heap, G, i1_1)) && invRecv5(aloc(Heap, G, i1_1)) == i1_1
      );
      assume (forall o_3: Ref ::
        { invRecv5(o_3) }
        ((0 <= invRecv5(o_3) && invRecv5(o_3) < V) && NoPerm < 1 / 2) && qpRange5(o_3) ==> aloc(Heap, G, invRecv5(o_3)) == o_3
      );
    // Check that permission expression is non-negative for all fields
    assert {:msg "  Contract might not be well-formed. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@48.13--48.94) [148]"}
      (forall i1_1: int ::
      { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
      0 <= i1_1 && i1_1 < V ==> 1 / 2 >= NoPerm
    );
    
    // -- Assume set of fields is nonNull
      assume (forall i1_1: int ::
        { aloc(Heap, G, i1_1) } { Heap[aloc(Heap, G, i1_1), oa] }
        (0 <= i1_1 && i1_1 < V) && 1 / 2 > NoPerm ==> aloc(Heap, G, i1_1) != null
      );
    
    // -- Define permissions
      assume (forall o_3: Ref ::
        { QPMask[o_3, oa] }
        (((0 <= invRecv5(o_3) && invRecv5(o_3) < V) && NoPerm < 1 / 2) && qpRange5(o_3) ==> (NoPerm < 1 / 2 ==> aloc(Heap, G, invRecv5(o_3)) == o_3) && QPMask[o_3, oa] == Mask[o_3, oa] + 1 / 2) && (!(((0 <= invRecv5(o_3) && invRecv5(o_3) < V) && NoPerm < 1 / 2) && qpRange5(o_3)) ==> QPMask[o_3, oa] == Mask[o_3, oa])
      );
      assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
        { Mask[o_3, f_5] } { QPMask[o_3, f_5] }
        f_5 != oa ==> Mask[o_3, f_5] == QPMask[o_3, f_5]
      );
    Mask := QPMask;
    assume state(Heap, Mask);
    assume state(Heap, Mask);
    
    // -- Check definedness of mv == matrixValues(G, V)
      if (*) {
        // Exhale precondition of function application
        assert {:msg "  Precondition of function matrixValues might not hold. Assertion alen(G) == V might not hold. (1.0-Lukas-tinker-2-minimized-array-4.vpr@49.18--49.36) [149]"}
          (alen(G): int) == V;
        havoc QPMask;
        
        // -- check that the permission amount is positive
          assert {:msg "  Precondition of function matrixValues might not hold. Fraction 1 / 2 might be negative. (1.0-Lukas-tinker-2-minimized-array-4.vpr@49.18--49.36) [150]"}
            (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            (0 <= i1_2 && i1_2 < V) && dummyFunction(Heap[aloc(Heap, G, i1_2), oa]) ==> 1 / 2 >= NoPerm
          );
        
        // -- check if receiver aloc(G, i1) is injective
          assert {:msg "  Precondition of function matrixValues might not hold. Quantified resource aloc(G, i1).oa might not be injective. (1.0-Lukas-tinker-2-minimized-array-4.vpr@49.18--49.36) [151]"}
            (forall i1_2: int, i1_2_1: int ::
            { neverTriggered6(i1_2), neverTriggered6(i1_2_1) }
            (((i1_2 != i1_2_1 && (0 <= i1_2 && i1_2 < V)) && (0 <= i1_2_1 && i1_2_1 < V)) && NoPerm < 1 / 2) && NoPerm < 1 / 2 ==> aloc(Heap, G, i1_2) != aloc(Heap, G, i1_2_1)
          );
        
        // -- check if sufficient permission is held
          assert {:msg "  Precondition of function matrixValues might not hold. There might be insufficient permission to access aloc(G, i1).oa (1.0-Lukas-tinker-2-minimized-array-4.vpr@49.18--49.36) [152]"}
            (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            0 <= i1_2 && i1_2 < V ==> Mask[aloc(Heap, G, i1_2), oa] >= 1 / 2
          );
        
        // -- assumptions for inverse of receiver aloc(G, i1)
          assume (forall i1_2: int ::
            { aloc(Heap, G, i1_2) } { Heap[aloc(Heap, G, i1_2), oa] }
            (0 <= i1_2 && i1_2 < V) && NoPerm < 1 / 2 ==> qpRange6(aloc(Heap, G, i1_2)) && invRecv6(aloc(Heap, G, i1_2)) == i1_2
          );
          assume (forall o_3: Ref ::
            { invRecv6(o_3) }
            (0 <= invRecv6(o_3) && invRecv6(o_3) < V) && (NoPerm < 1 / 2 && qpRange6(o_3)) ==> aloc(Heap, G, invRecv6(o_3)) == o_3
          );
        
        // -- assume permission updates for field oa
          assume (forall o_3: Ref ::
            { QPMask[o_3, oa] }
            ((0 <= invRecv6(o_3) && invRecv6(o_3) < V) && (NoPerm < 1 / 2 && qpRange6(o_3)) ==> aloc(Heap, G, invRecv6(o_3)) == o_3 && QPMask[o_3, oa] == Mask[o_3, oa] - 1 / 2) && (!((0 <= invRecv6(o_3) && invRecv6(o_3) < V) && (NoPerm < 1 / 2 && qpRange6(o_3))) ==> QPMask[o_3, oa] == Mask[o_3, oa])
          );
        
        // -- assume permission updates for independent locations
          assume (forall <A, B> o_3: Ref, f_5: (Field A B) ::
            { QPMask[o_3, f_5] }
            f_5 != oa ==> 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 state(Heap, Mask);
    assume state(Heap, Mask);
    assume Seq#Equal(mv, matrixValues(Heap, G, V));
    assume state(Heap, Mask);
    assume Seq#Equal(mv, mv);
    assume state(Heap, Mask);
  
  // -- Initializing of old state
    
    // -- Initializing the old state
      assume Heap == old(Heap);
      assume Mask == old(Mask);
  
  // -- Translating statement: inhale false -- <no position>
    assume false;
    assume state(Heap, Mask);
    assume state(Heap, Mask);
}