Fix test failure. Print the resulting boogie code to a file instead

of console.

2 files changed, 1 insertions, 1771 deletions

diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy
index 5f3cde69..97c9e389 100644
--- a/Test/dafny4/Bug136.dfy
+++ b/Test/dafny4/Bug136.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:- "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 method test()

diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect
index 8b9d32a8..069e7767 100644
--- a/Test/dafny4/Bug136.dfy.expect
+++ b/Test/dafny4/Bug136.dfy.expect
@@ -1,1772 +1,2 @@
-// Dafny program verifier version 1.9.6.21116, Copyright (c) 2003-2015, Microsoft.

-// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /compile:0 /print:- c:\dafny\Test\dafny4\Bug136.dfy

-

-const $$Language$Dafny: bool;

-

-axiom $$Language$Dafny;

-

-type Ty;

-

-const unique TBool: Ty;

-

-const unique TChar: Ty;

-

-const unique TInt: Ty;

-

-const unique TNat: Ty;

-

-const unique TReal: Ty;

-

-function TSet(Ty) : Ty;

-

-function TISet(Ty) : Ty;

-

-function TMultiSet(Ty) : Ty;

-

-function TSeq(Ty) : Ty;

-

-function TMap(Ty, Ty) : Ty;

-

-function TIMap(Ty, Ty) : Ty;

-

-function Inv0_TSet(Ty) : Ty;

-

-axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);

-

-function Inv0_TISet(Ty) : Ty;

-

-axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);

-

-function Inv0_TSeq(Ty) : Ty;

-

-axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);

-

-function Inv0_TMultiSet(Ty) : Ty;

-

-axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);

-

-function Inv0_TMap(Ty) : Ty;

-

-function Inv1_TMap(Ty) : Ty;

-

-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv0_TMap(TMap(t, u)) == t);

-

-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv1_TMap(TMap(t, u)) == u);

-

-function Inv0_TIMap(Ty) : Ty;

-

-function Inv1_TIMap(Ty) : Ty;

-

-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv0_TIMap(TIMap(t, u)) == t);

-

-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv1_TIMap(TIMap(t, u)) == u);

-

-type TyTag;

-

-function Tag(Ty) : TyTag;

-

-const unique TagBool: TyTag;

-

-const unique TagChar: TyTag;

-

-const unique TagInt: TyTag;

-

-const unique TagNat: TyTag;

-

-const unique TagReal: TyTag;

-

-const unique TagSet: TyTag;

-

-const unique TagISet: TyTag;

-

-const unique TagMultiSet: TyTag;

-

-const unique TagSeq: TyTag;

-

-const unique TagMap: TyTag;

-

-const unique TagIMap: TyTag;

-

-const unique TagClass: TyTag;

-

-axiom Tag(TBool) == TagBool;

-

-axiom Tag(TChar) == TagChar;

-

-axiom Tag(TInt) == TagInt;

-

-axiom Tag(TNat) == TagNat;

-

-axiom Tag(TReal) == TagReal;

-

-axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet);

-

-axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet);

-

-axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);

-

-axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);

-

-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Tag(TMap(t, u)) == TagMap);

-

-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Tag(TIMap(t, u)) == TagIMap);

-

-function {:identity} LitInt(x: int) : int;

-

-axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x);

-

-axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)));

-

-function {:identity} LitReal(x: real) : real;

-

-axiom (forall x: real :: {:identity} { LitReal(x): real } LitReal(x): real == x);

-

-axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)));

-

-function {:identity} Lit<T>(x: T) : T;

-

-axiom (forall<T> x: T :: {:identity} { Lit(x): T } Lit(x): T == x);

-

-axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)));

-

-type char;

-

-function char#FromInt(int) : char;

-

-function char#ToInt(char) : int;

-

-axiom (forall ch: char :: { char#ToInt(ch) } char#FromInt(char#ToInt(ch)) == ch);

-

-axiom (forall n: int :: 

-  { char#FromInt(n) } 

-  0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);

-

-type ref;

-

-const null: ref;

-

-const unique NoTraitAtAll: ClassName;

-

-function TraitParent(ClassName) : ClassName;

-

-type Box;

-

-const $ArbitraryBoxValue: Box;

-

-function $Box<T>(T) : Box;

-

-function $Unbox<T>(Box) : T;

-

-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

-

-axiom (forall bx: Box :: 

-  { $IsBox(bx, TInt) } 

-  $IsBox(bx, TInt) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TInt));

-

-axiom (forall bx: Box :: 

-  { $IsBox(bx, TNat) } 

-  $IsBox(bx, TNat) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TNat));

-

-axiom (forall bx: Box :: 

-  { $IsBox(bx, TReal) } 

-  $IsBox(bx, TReal)

-     ==> $Box($Unbox(bx): real) == bx && $Is($Unbox(bx): real, TReal));

-

-axiom (forall bx: Box :: 

-  { $IsBox(bx, TBool) } 

-  $IsBox(bx, TBool)

-     ==> $Box($Unbox(bx): bool) == bx && $Is($Unbox(bx): bool, TBool));

-

-axiom (forall bx: Box :: 

-  { $IsBox(bx, TChar) } 

-  $IsBox(bx, TChar)

-     ==> $Box($Unbox(bx): char) == bx && $Is($Unbox(bx): char, TChar));

-

-axiom (forall bx: Box, t: Ty :: 

-  { $IsBox(bx, TSet(t)) } 

-  $IsBox(bx, TSet(t))

-     ==> $Box($Unbox(bx): Set Box) == bx && $Is($Unbox(bx): Set Box, TSet(t)));

-

-axiom (forall bx: Box, t: Ty :: 

-  { $IsBox(bx, TISet(t)) } 

-  $IsBox(bx, TISet(t))

-     ==> $Box($Unbox(bx): ISet Box) == bx && $Is($Unbox(bx): ISet Box, TISet(t)));

-

-axiom (forall bx: Box, t: Ty :: 

-  { $IsBox(bx, TMultiSet(t)) } 

-  $IsBox(bx, TMultiSet(t))

-     ==> $Box($Unbox(bx): MultiSet Box) == bx

-       && $Is($Unbox(bx): MultiSet Box, TMultiSet(t)));

-

-axiom (forall bx: Box, t: Ty :: 

-  { $IsBox(bx, TSeq(t)) } 

-  $IsBox(bx, TSeq(t))

-     ==> $Box($Unbox(bx): Seq Box) == bx && $Is($Unbox(bx): Seq Box, TSeq(t)));

-

-axiom (forall bx: Box, s: Ty, t: Ty :: 

-  { $IsBox(bx, TMap(s, t)) } 

-  $IsBox(bx, TMap(s, t))

-     ==> $Box($Unbox(bx): Map Box Box) == bx && $Is($Unbox(bx): Map Box Box, TMap(s, t)));

-

-axiom (forall bx: Box, s: Ty, t: Ty :: 

-  { $IsBox(bx, TIMap(s, t)) } 

-  $IsBox(bx, TIMap(s, t))

-     ==> $Box($Unbox(bx): IMap Box Box) == bx

-       && $Is($Unbox(bx): IMap Box Box, TIMap(s, t)));

-

-axiom (forall<T> v: T, t: Ty :: 

-  { $IsBox($Box(v), t) } 

-  $IsBox($Box(v), t) <==> $Is(v, t));

-

-axiom (forall<T> v: T, t: Ty, h: Heap :: 

-  { $IsAllocBox($Box(v), t, h) } 

-  $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h));

-

-function $Is<T>(T, Ty) : bool;

-

-function $IsAlloc<T>(T, Ty, Heap) : bool;

-

-function $IsBox<T>(T, Ty) : bool;

-

-function $IsAllocBox<T>(T, Ty, Heap) : bool;

-

-axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt));

-

-axiom (forall v: int :: { $Is(v, TNat) } $Is(v, TNat) <==> v >= 0);

-

-axiom (forall v: real :: { $Is(v, TReal) } $Is(v, TReal));

-

-axiom (forall v: bool :: { $Is(v, TBool) } $Is(v, TBool));

-

-axiom (forall v: char :: { $Is(v, TChar) } $Is(v, TChar));

-

-axiom (forall h: Heap, v: int :: { $IsAlloc(v, TInt, h) } $IsAlloc(v, TInt, h));

-

-axiom (forall h: Heap, v: int :: { $IsAlloc(v, TNat, h) } $IsAlloc(v, TNat, h));

-

-axiom (forall h: Heap, v: real :: { $IsAlloc(v, TReal, h) } $IsAlloc(v, TReal, h));

-

-axiom (forall h: Heap, v: bool :: { $IsAlloc(v, TBool, h) } $IsAlloc(v, TBool, h));

-

-axiom (forall h: Heap, v: char :: { $IsAlloc(v, TChar, h) } $IsAlloc(v, TChar, h));

-

-axiom (forall v: Set Box, t0: Ty :: 

-  { $Is(v, TSet(t0)) } 

-  $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));

-

-axiom (forall v: ISet Box, t0: Ty :: 

-  { $Is(v, TISet(t0)) } 

-  $Is(v, TISet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));

-

-axiom (forall v: MultiSet Box, t0: Ty :: 

-  { $Is(v, TMultiSet(t0)) } 

-  $Is(v, TMultiSet(t0))

-     <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsBox(bx, t0)));

-

-axiom (forall v: MultiSet Box, t0: Ty :: 

-  { $Is(v, TMultiSet(t0)) } 

-  $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));

-

-axiom (forall v: Seq Box, t0: Ty :: 

-  { $Is(v, TSeq(t0)) } 

-  $Is(v, TSeq(t0))

-     <==> (forall i: int :: 

-      { Seq#Index(v, i) } 

-      0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));

-

-axiom (forall v: Set Box, t0: Ty, h: Heap :: 

-  { $IsAlloc(v, TSet(t0), h) } 

-  $IsAlloc(v, TSet(t0), h)

-     <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));

-

-axiom (forall v: ISet Box, t0: Ty, h: Heap :: 

-  { $IsAlloc(v, TISet(t0), h) } 

-  $IsAlloc(v, TISet(t0), h)

-     <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));

-

-axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: 

-  { $IsAlloc(v, TMultiSet(t0), h) } 

-  $IsAlloc(v, TMultiSet(t0), h)

-     <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsAllocBox(bx, t0, h)));

-

-axiom (forall v: Seq Box, t0: Ty, h: Heap :: 

-  { $IsAlloc(v, TSeq(t0), h) } 

-  $IsAlloc(v, TSeq(t0), h)

-     <==> (forall i: int :: 

-      { Seq#Index(v, i) } 

-      0 <= i && i < Seq#Length(v) ==> $IsAllocBox(Seq#Index(v, i), t0, h)));

-

-axiom (forall v: Map Box Box, t0: Ty, t1: Ty :: 

-  { $Is(v, TMap(t0, t1)) } 

-  $Is(v, TMap(t0, t1))

-     <==> (forall bx: Box :: 

-      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } 

-      Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0)));

-

-axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap :: 

-  { $IsAlloc(v, TMap(t0, t1), h) } 

-  $IsAlloc(v, TMap(t0, t1), h)

-     <==> (forall bx: Box :: 

-      { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } 

-      Map#Domain(v)[bx]

-         ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));

-

-axiom (forall v: IMap Box Box, t0: Ty, t1: Ty :: 

-  { $Is(v, TIMap(t0, t1)) } 

-  $Is(v, TIMap(t0, t1))

-     <==> (forall bx: Box :: 

-      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } 

-      IMap#Domain(v)[bx] ==> $IsBox(IMap#Elements(v)[bx], t1) && $IsBox(bx, t0)));

-

-axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap :: 

-  { $IsAlloc(v, TIMap(t0, t1), h) } 

-  $IsAlloc(v, TIMap(t0, t1), h)

-     <==> (forall bx: Box :: 

-      { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } 

-      IMap#Domain(v)[bx]

-         ==> $IsAllocBox(IMap#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));

-

-type ClassName;

-

-const unique class._System.int: ClassName;

-

-const unique class._System.bool: ClassName;

-

-const unique class._System.set: ClassName;

-

-const unique class._System.seq: ClassName;

-

-const unique class._System.multiset: ClassName;

-

-function Tclass._System.object() : Ty;

-

-function dtype(ref) : Ty;

-

-function TypeTuple(a: ClassName, b: ClassName) : ClassName;

-

-function TypeTupleCar(ClassName) : ClassName;

-

-function TypeTupleCdr(ClassName) : ClassName;

-

-axiom (forall a: ClassName, b: ClassName :: 

-  { TypeTuple(a, b) } 

-  TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);

-

-type HandleType;

-

-function SetRef_to_SetBox(s: [ref]bool) : Set Box;

-

-axiom (forall s: [ref]bool, bx: Box :: 

-  { SetRef_to_SetBox(s)[bx] } 

-  SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);

-

-axiom (forall s: [ref]bool :: 

-  { SetRef_to_SetBox(s) } 

-  $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));

-

-type DatatypeType;

-

-type DtCtorId;

-

-function DatatypeCtorId(DatatypeType) : DtCtorId;

-

-function DtRank(DatatypeType) : int;

-

-function BoxRank(Box) : int;

-

-axiom (forall d: DatatypeType :: { BoxRank($Box(d)) } BoxRank($Box(d)) == DtRank(d));

-

-const $ModuleContextHeight: int;

-

-const $FunctionContextHeight: int;

-

-type LayerType;

-

-const $LZ: LayerType;

-

-function $LS(LayerType) : LayerType;

-

-function AtLayer<A>([LayerType]A, LayerType) : A;

-

-axiom (forall<A> f: [LayerType]A, ly: LayerType :: 

-  { AtLayer(f, ly) } 

-  AtLayer(f, ly) == f[ly]);

-

-axiom (forall<A> f: [LayerType]A, ly: LayerType :: 

-  { AtLayer(f, $LS(ly)) } 

-  AtLayer(f, $LS(ly)) == AtLayer(f, ly));

-

-type Field _;

-

-function FDim<T>(Field T) : int;

-

-function IndexField(int) : Field Box;

-

-axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);

-

-function IndexField_Inverse<T>(Field T) : int;

-

-axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);

-

-function MultiIndexField(Field Box, int) : Field Box;

-

-axiom (forall f: Field Box, i: int :: 

-  { MultiIndexField(f, i) } 

-  FDim(MultiIndexField(f, i)) == FDim(f) + 1);

-

-function MultiIndexField_Inverse0<T>(Field T) : Field T;

-

-function MultiIndexField_Inverse1<T>(Field T) : int;

-

-axiom (forall f: Field Box, i: int :: 

-  { MultiIndexField(f, i) } 

-  MultiIndexField_Inverse0(MultiIndexField(f, i)) == f

-     && MultiIndexField_Inverse1(MultiIndexField(f, i)) == i);

-

-function DeclType<T>(Field T) : ClassName;

-

-type NameFamily;

-

-function DeclName<T>(Field T) : NameFamily;

-

-function FieldOfDecl<alpha>(ClassName, NameFamily) : Field alpha;

-

-axiom (forall<T> cl: ClassName, nm: NameFamily :: 

-  { FieldOfDecl(cl, nm): Field T } 

-  DeclType(FieldOfDecl(cl, nm): Field T) == cl

-     && DeclName(FieldOfDecl(cl, nm): Field T) == nm);

-

-function $IsGhostField<T>(Field T) : bool;

-

-axiom (forall<T> h: Heap, k: Heap, v: T, t: Ty :: 

-  { $HeapSucc(h, k), $IsAlloc(v, t, h) } 

-  $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k));

-

-axiom (forall h: Heap, k: Heap, bx: Box, t: Ty :: 

-  { $HeapSucc(h, k), $IsAllocBox(bx, t, h) } 

-  $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k));

-

-const unique alloc: Field bool;

-

-axiom FDim(alloc) == 0 && !$IsGhostField(alloc);

-

-function _System.array.Length(a: ref) : int;

-

-axiom (forall o: ref :: 0 <= _System.array.Length(o));

-

-function Int(x: real) : int;

-

-axiom (forall x: real :: { Int(x): int } Int(x): int == int(x));

-

-function Real(x: int) : real;

-

-axiom (forall x: int :: { Real(x): real } Real(x): real == real(x));

-

-axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i);

-

-function {:inline true} _System.real.Trunc(x: real) : int

-{

-  Int(x)

-}

-

-type Heap = <alpha>[ref,Field alpha]alpha;

-

-function {:inline true} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha

-{

-  H[r, f]

-}

-

-function {:inline true} update<alpha>(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap

-{

-  H[r, f := v]

-}

-

-function $IsGoodHeap(Heap) : bool;

-

-function $IsHeapAnchor(Heap) : bool;

-

-var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);

-

-function $HeapSucc(Heap, Heap) : bool;

-

-axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: 

-  { update(h, r, f, x) } 

-  $IsGoodHeap(update(h, r, f, x)) ==> $HeapSucc(h, update(h, r, f, x)));

-

-axiom (forall a: Heap, b: Heap, c: Heap :: 

-  { $HeapSucc(a, b), $HeapSucc(b, c) } 

-  $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c));

-

-axiom (forall h: Heap, k: Heap :: 

-  { $HeapSucc(h, k) } 

-  $HeapSucc(h, k)

-     ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));

-

-function $HeapSuccGhost(Heap, Heap) : bool;

-

-axiom (forall h: Heap, k: Heap :: 

-  { $HeapSuccGhost(h, k) } 

-  $HeapSuccGhost(h, k)

-     ==> $HeapSucc(h, k)

-       && (forall<alpha> o: ref, f: Field alpha :: 

-        { read(k, o, f) } 

-        !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));

-

-type TickType;

-

-var $Tick: TickType;

-

-procedure $YieldHavoc(this: ref, rds: Set Box, nw: Set Box);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> 

-    $o == this || rds[$Box($o)] || nw[$Box($o)]

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> 

-    rds[$Box($o)] && !modi[$Box($o)] && $o != this

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box);

-  modifies $Heap;

-  ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)

-       || $o == this

-       || modi[$Box($o)]

-       || nw[$Box($o)]);

-  ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box))

-   returns (s: Set Box);

-  ensures (forall bx: Box :: 

-  { s[bx] } 

-  s[bx]

-     <==> read(newHeap, this, NW)[bx]

-       || (

-        $Unbox(bx) != null

-         && !read(prevHeap, $Unbox(bx): ref, alloc)

-         && read(newHeap, $Unbox(bx): ref, alloc)));

-

-

-

-type Set T = [T]bool;

-

-function Set#Card<T>(Set T) : int;

-

-axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));

-

-function Set#Empty<T>() : Set T;

-

-axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

-

-axiom (forall<T> 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>(T) : Set T;

-

-axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

-

-axiom (forall<T> r: T, o: T :: 

-  { Set#Singleton(r)[o] } 

-  Set#Singleton(r)[o] <==> r == o);

-

-axiom (forall<T> r: T :: 

-  { Set#Card(Set#Singleton(r)) } 

-  Set#Card(Set#Singleton(r)) == 1);

-

-function Set#UnionOne<T>(Set T, T) : Set T;

-

-axiom (forall<T> a: Set T, x: T, o: T :: 

-  { Set#UnionOne(a, x)[o] } 

-  Set#UnionOne(a, x)[o] <==> o == x || a[o]);

-

-axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]);

-

-axiom (forall<T> a: Set T, x: T, y: T :: 

-  { Set#UnionOne(a, x), a[y] } 

-  a[y] ==> Set#UnionOne(a, x)[y]);

-

-axiom (forall<T> a: Set T, x: T :: 

-  { Set#Card(Set#UnionOne(a, x)) } 

-  a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));

-

-axiom (forall<T> 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<T>(Set T, Set T) : Set T;

-

-axiom (forall<T> a: Set T, b: Set T, o: T :: 

-  { Set#Union(a, b)[o] } 

-  Set#Union(a, b)[o] <==> a[o] || b[o]);

-

-axiom (forall<T> a: Set T, b: Set T, y: T :: 

-  { Set#Union(a, b), a[y] } 

-  a[y] ==> Set#Union(a, b)[y]);

-

-axiom (forall<T> a: Set T, b: Set T, y: T :: 

-  { Set#Union(a, b), b[y] } 

-  b[y] ==> Set#Union(a, b)[y]);

-

-axiom (forall<T> a: Set T, 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<T>(Set T, Set T) : Set T;

-

-axiom (forall<T> a: Set T, b: Set T, o: T :: 

-  { Set#Intersection(a, b)[o] } 

-  Set#Intersection(a, b)[o] <==> a[o] && b[o]);

-

-axiom (forall<T> a: Set T, b: Set T :: 

-  { Set#Union(Set#Union(a, b), b) } 

-  Set#Union(Set#Union(a, b), b) == Set#Union(a, b));

-

-axiom (forall<T> a: Set T, b: Set T :: 

-  { Set#Union(a, Set#Union(a, b)) } 

-  Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));

-

-axiom (forall<T> a: Set T, b: Set T :: 

-  { Set#Intersection(Set#Intersection(a, b), b) } 

-  Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));

-

-axiom (forall<T> a: Set T, b: Set T :: 

-  { Set#Intersection(a, Set#Intersection(a, b)) } 

-  Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

-

-axiom (forall<T> a: Set T, 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<T>(Set T, Set T) : Set T;

-

-axiom (forall<T> a: Set T, b: Set T, o: T :: 

-  { Set#Difference(a, b)[o] } 

-  Set#Difference(a, b)[o] <==> a[o] && !b[o]);

-

-axiom (forall<T> a: Set T, b: Set T, y: T :: 

-  { Set#Difference(a, b), b[y] } 

-  b[y] ==> !Set#Difference(a, b)[y]);

-

-axiom (forall<T> a: Set T, 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<T>(Set T, Set T) : bool;

-

-axiom (forall<T> 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]));

-

-function Set#Equal<T>(Set T, Set T) : bool;

-

-axiom (forall<T> 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<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b);

-

-function Set#Disjoint<T>(Set T, Set T) : bool;

-

-axiom (forall<T> 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]));

-

-type ISet T = [T]bool;

-

-function ISet#Empty<T>() : Set T;

-

-axiom (forall<T> o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]);

-

-function ISet#UnionOne<T>(ISet T, T) : ISet T;

-

-axiom (forall<T> a: ISet T, x: T, o: T :: 

-  { ISet#UnionOne(a, x)[o] } 

-  ISet#UnionOne(a, x)[o] <==> o == x || a[o]);

-

-axiom (forall<T> a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]);

-

-axiom (forall<T> a: ISet T, x: T, y: T :: 

-  { ISet#UnionOne(a, x), a[y] } 

-  a[y] ==> ISet#UnionOne(a, x)[y]);

-

-function ISet#Union<T>(ISet T, ISet T) : ISet T;

-

-axiom (forall<T> a: ISet T, b: ISet T, o: T :: 

-  { ISet#Union(a, b)[o] } 

-  ISet#Union(a, b)[o] <==> a[o] || b[o]);

-

-axiom (forall<T> a: ISet T, b: ISet T, y: T :: 

-  { ISet#Union(a, b), a[y] } 

-  a[y] ==> ISet#Union(a, b)[y]);

-

-axiom (forall<T> a: Set T, b: Set T, y: T :: 

-  { ISet#Union(a, b), b[y] } 

-  b[y] ==> ISet#Union(a, b)[y]);

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Union(a, b) } 

-  ISet#Disjoint(a, b)

-     ==> ISet#Difference(ISet#Union(a, b), a) == b

-       && ISet#Difference(ISet#Union(a, b), b) == a);

-

-function ISet#Intersection<T>(ISet T, ISet T) : ISet T;

-

-axiom (forall<T> a: ISet T, b: ISet T, o: T :: 

-  { ISet#Intersection(a, b)[o] } 

-  ISet#Intersection(a, b)[o] <==> a[o] && b[o]);

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Union(ISet#Union(a, b), b) } 

-  ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b));

-

-axiom (forall<T> a: Set T, b: Set T :: 

-  { ISet#Union(a, ISet#Union(a, b)) } 

-  ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b));

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Intersection(ISet#Intersection(a, b), b) } 

-  ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b));

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Intersection(a, ISet#Intersection(a, b)) } 

-  ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b));

-

-function ISet#Difference<T>(ISet T, ISet T) : ISet T;

-

-axiom (forall<T> a: ISet T, b: ISet T, o: T :: 

-  { ISet#Difference(a, b)[o] } 

-  ISet#Difference(a, b)[o] <==> a[o] && !b[o]);

-

-axiom (forall<T> a: ISet T, b: ISet T, y: T :: 

-  { ISet#Difference(a, b), b[y] } 

-  b[y] ==> !ISet#Difference(a, b)[y]);

-

-function ISet#Subset<T>(ISet T, ISet T) : bool;

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Subset(a, b) } 

-  ISet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));

-

-function ISet#Equal<T>(ISet T, ISet T) : bool;

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Equal(a, b) } 

-  ISet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Equal(a, b) } 

-  ISet#Equal(a, b) ==> a == b);

-

-function ISet#Disjoint<T>(ISet T, ISet T) : bool;

-

-axiom (forall<T> a: ISet T, b: ISet T :: 

-  { ISet#Disjoint(a, b) } 

-  ISet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));

-

-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 $IsGoodMultiSet<T>(ms: MultiSet T) : bool;

-

-axiom (forall<T> ms: MultiSet T :: 

-  { $IsGoodMultiSet(ms) } 

-  $IsGoodMultiSet(ms)

-     <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));

-

-function MultiSet#Card<T>(MultiSet T) : int;

-

-axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));

-

-axiom (forall<T> 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<T>() : MultiSet T;

-

-axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);

-

-axiom (forall<T> s: MultiSet T :: 

-  { MultiSet#Card(s) } 

-  (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty())

-     && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));

-

-function MultiSet#Singleton<T>(T) : MultiSet T;

-

-axiom (forall<T> r: T, o: T :: 

-  { MultiSet#Singleton(r)[o] } 

-  (MultiSet#Singleton(r)[o] == 1 <==> r == o)

-     && (MultiSet#Singleton(r)[o] == 0 <==> r != o));

-

-axiom (forall<T> r: T :: 

-  { MultiSet#Singleton(r) } 

-  MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));

-

-function MultiSet#UnionOne<T>(MultiSet T, T) : MultiSet T;

-

-axiom (forall<T> a: MultiSet T, x: T, o: T :: 

-  { MultiSet#UnionOne(a, x)[o] } 

-  0 < MultiSet#UnionOne(a, x)[o] <==> o == x || 0 < a[o]);

-

-axiom (forall<T> a: MultiSet T, x: T :: 

-  { MultiSet#UnionOne(a, x) } 

-  MultiSet#UnionOne(a, x)[x] == a[x] + 1);

-

-axiom (forall<T> a: MultiSet T, x: T, y: T :: 

-  { MultiSet#UnionOne(a, x), a[y] } 

-  0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);

-

-axiom (forall<T> a: MultiSet T, x: T, y: T :: 

-  { MultiSet#UnionOne(a, x), a[y] } 

-  x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);

-

-axiom (forall<T> a: MultiSet T, x: T :: 

-  { MultiSet#Card(MultiSet#UnionOne(a, x)) } 

-  MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);

-

-function MultiSet#Union<T>(MultiSet T, MultiSet T) : MultiSet T;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 

-  { MultiSet#Union(a, b)[o] } 

-  MultiSet#Union(a, b)[o] == a[o] + b[o]);

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Card(MultiSet#Union(a, b)) } 

-  MultiSet#Card(MultiSet#Union(a, b)) == MultiSet#Card(a) + MultiSet#Card(b));

-

-function MultiSet#Intersection<T>(MultiSet T, MultiSet T) : MultiSet T;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 

-  { MultiSet#Intersection(a, b)[o] } 

-  MultiSet#Intersection(a, b)[o] == Math#min(a[o], b[o]));

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } 

-  MultiSet#Intersection(MultiSet#Intersection(a, b), b)

-     == MultiSet#Intersection(a, b));

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } 

-  MultiSet#Intersection(a, MultiSet#Intersection(a, b))

-     == MultiSet#Intersection(a, b));

-

-function MultiSet#Difference<T>(MultiSet T, MultiSet T) : MultiSet T;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: 

-  { MultiSet#Difference(a, b)[o] } 

-  MultiSet#Difference(a, b)[o] == Math#clip(a[o] - b[o]));

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T :: 

-  { MultiSet#Difference(a, b), b[y], a[y] } 

-  a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0);

-

-axiom (forall<T> a: MultiSet T, 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)));

-

-function MultiSet#Subset<T>(MultiSet T, MultiSet T) : bool;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Subset(a, b) } 

-  MultiSet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <= b[o]));

-

-function MultiSet#Equal<T>(MultiSet T, MultiSet T) : bool;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Equal(a, b) } 

-  MultiSet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == b[o]));

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Equal(a, b) } 

-  MultiSet#Equal(a, b) ==> a == b);

-

-function MultiSet#Disjoint<T>(MultiSet T, MultiSet T) : bool;

-

-axiom (forall<T> a: MultiSet T, b: MultiSet T :: 

-  { MultiSet#Disjoint(a, b) } 

-  MultiSet#Disjoint(a, b)

-     <==> (forall o: T :: { a[o] } { b[o] } a[o] == 0 || b[o] == 0));

-

-function MultiSet#FromSet<T>(Set T) : MultiSet T;

-

-axiom (forall<T> s: Set T, a: T :: 

-  { MultiSet#FromSet(s)[a] } 

-  (MultiSet#FromSet(s)[a] == 0 <==> !s[a])

-     && (MultiSet#FromSet(s)[a] == 1 <==> s[a]));

-

-axiom (forall<T> s: Set T :: 

-  { MultiSet#Card(MultiSet#FromSet(s)) } 

-  MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));

-

-function MultiSet#FromSeq<T>(Seq T) : MultiSet T;

-

-axiom (forall<T> s: Seq T :: 

-  { MultiSet#FromSeq(s) } 

-  $IsGoodMultiSet(MultiSet#FromSeq(s)));

-

-axiom (forall<T> s: Seq T :: 

-  { MultiSet#Card(MultiSet#FromSeq(s)) } 

-  MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s));

-

-axiom (forall<T> s: Seq T, v: T :: 

-  { MultiSet#FromSeq(Seq#Build(s, v)) } 

-  MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v));

-

-axiom (forall<T>  :: 

-  MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);

-

-axiom (forall<T> a: Seq T, b: Seq T :: 

-  { MultiSet#FromSeq(Seq#Append(a, b)) } 

-  MultiSet#FromSeq(Seq#Append(a, b))

-     == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)));

-

-axiom (forall<T> s: Seq T, i: int, v: T, x: T :: 

-  { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } 

-  0 <= i && i < Seq#Length(s)

-     ==> MultiSet#FromSeq(Seq#Update(s, i, v))[x]

-       == MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s, i))), 

-        MultiSet#Singleton(v))[x]);

-

-axiom (forall<T> s: Seq T, x: T :: 

-  { MultiSet#FromSeq(s)[x] } 

-  (exists i: int :: 

-      { Seq#Index(s, i) } 

-      0 <= i && i < Seq#Length(s) && x == Seq#Index(s, i))

-     <==> 0 < MultiSet#FromSeq(s)[x]);

-

-type Seq _;

-

-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());

-

-axiom (forall<T> t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t));

-

-function Seq#Singleton<T>(T) : Seq T;

-

-axiom (forall<T> t: T :: 

-  { Seq#Length(Seq#Singleton(t)) } 

-  Seq#Length(Seq#Singleton(t)) == 1);

-

-function Seq#Build<T>(s: Seq T, val: T) : Seq T;

-

-axiom (forall<T> s: Seq T, v: T :: 

-  { Seq#Length(Seq#Build(s, v)) } 

-  Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));

-

-axiom (forall<T> s: Seq T, i: int, v: T :: 

-  { Seq#Index(Seq#Build(s, v), i) } 

-  (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v)

-     && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));

-

-axiom (forall s: Seq Box, bx: Box, t: Ty :: 

-  { $Is(Seq#Build(s, bx), TSeq(t)) } 

-  $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t)));

-

-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)) } 

-  Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));

-

-axiom (forall s0: Seq Box, s1: Seq Box, t: Ty :: 

-  { $Is(Seq#Append(s0, s1), t) } 

-  $Is(s0, t) && $Is(s1, t) ==> $Is(Seq#Append(s0, s1), t));

-

-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);

-

-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: 

-  { Seq#Index(Seq#Append(s0, s1), n) } 

-  (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))));

-

-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)) } 

-  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) } 

-  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)));

-

-function Seq#Contains<T>(Seq T, T) : bool;

-

-axiom (forall<T> s: Seq T, x: T :: 

-  { Seq#Contains(s, x) } 

-  Seq#Contains(s, x)

-     <==> (exists i: int :: 

-      { Seq#Index(s, i) } 

-      0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

-

-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, v: T, x: T :: 

-  { Seq#Contains(Seq#Build(s, v), x) } 

-  Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, 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));

-

-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) } Seq#Equal(a, b) ==> a == b);

-

-function Seq#SameUntil<T>(Seq T, Seq T, int) : bool;

-

-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: 

-  { Seq#SameUntil(s0, s1, n) } 

-  Seq#SameUntil(s0, s1, n)

-     <==> (forall j: int :: 

-      { Seq#Index(s0, j) } { Seq#Index(s1, j) } 

-      0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));

-

-function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;

-

-axiom (forall<T> s: Seq T, n: int :: 

-  { Seq#Length(Seq#Take(s, n)) } 

-  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n);

-

-axiom (forall<T> s: Seq T, n: int, j: int :: 

-  {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) } 

-  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)) } 

-  0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n);

-

-axiom (forall<T> s: Seq T, n: int, j: int :: 

-  {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } 

-  0 <= n && 0 <= j && j < Seq#Length(s) - n

-     ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));

-

-axiom (forall<T> s: Seq T, n: int, k: int :: 

-  {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) } 

-  0 <= n && n <= k && k < Seq#Length(s)

-     ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k));

-

-axiom (forall<T> s: Seq T, t: Seq T :: 

-  { Seq#Append(s, t) } 

-  Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s

-     && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

-

-function Seq#FromArray(h: Heap, a: ref) : Seq Box;

-

-axiom (forall h: Heap, a: ref :: 

-  { Seq#Length(Seq#FromArray(h, a)) } 

-  Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

-

-axiom (forall h: Heap, a: ref :: 

-  { Seq#FromArray(h, a) } 

-  (forall i: int :: 

-    { read(h, a, IndexField(i)) } { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } 

-    0 <= i && i < Seq#Length(Seq#FromArray(h, a))

-       ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

-

-axiom (forall h0: Heap, h1: Heap, a: ref :: 

-  { Seq#FromArray(h1, a), $HeapSucc(h0, h1) } 

-  $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && $HeapSucc(h0, h1)

-       && (forall i: int :: 

-        0 <= i && i < _System.array.Length(a)

-           ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i)))

-     ==> Seq#FromArray(h0, a) == Seq#FromArray(h1, a));

-

-axiom (forall h: Heap, i: int, v: Box, a: ref :: 

-  { Seq#FromArray(update(h, a, IndexField(i), v), a) } 

-  0 <= i && i < _System.array.Length(a)

-     ==> Seq#FromArray(update(h, a, IndexField(i), v), a)

-       == Seq#Update(Seq#FromArray(h, a), i, v));

-

-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));

-

-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));

-

-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));

-

-axiom (forall h: Heap, a: ref, n0: int, n1: int :: 

-  { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } 

-  n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a)

-     ==> Seq#Take(Seq#FromArray(h, a), n1)

-       == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field Box)));

-

-axiom (forall<T> s: Seq T, v: T, n: int :: 

-  { Seq#Drop(Seq#Build(s, v), n) } 

-  0 <= n && n <= Seq#Length(s)

-     ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v));

-

-function Seq#Rank<T>(Seq T) : int;

-

-axiom (forall s: Seq Box, i: int :: 

-  { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) } 

-  0 <= i && i < Seq#Length(s)

-     ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s));

-

-axiom (forall<T> s: Seq T, i: int :: 

-  { Seq#Rank(Seq#Drop(s, i)) } 

-  0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s));

-

-axiom (forall<T> s: Seq T, i: int :: 

-  { Seq#Rank(Seq#Take(s, i)) } 

-  0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s));

-

-axiom (forall<T> s: Seq T, i: int, j: int :: 

-  { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) } 

-  0 <= i && i < j && j <= Seq#Length(s)

-     ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s));

-

-axiom (forall<T> s: Seq T, n: int :: 

-  { Seq#Drop(s, n) } 

-  n == 0 ==> Seq#Drop(s, n) == s);

-

-axiom (forall<T> s: Seq T, n: int :: 

-  { Seq#Take(s, n) } 

-  n == 0 ==> Seq#Take(s, n) == Seq#Empty());

-

-axiom (forall<T> s: Seq T, m: int, n: int :: 

-  { Seq#Drop(Seq#Drop(s, m), n) } 

-  0 <= m && 0 <= n && m + n <= Seq#Length(s)

-     ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n));

-

-type Map _ _;

-

-function Map#Domain<U,V>(Map U V) : [U]bool;

-

-function Map#Elements<U,V>(Map U V) : [U]V;

-

-function Map#Card<U,V>(Map U V) : int;

-

-axiom (forall<U,V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));

-

-function Map#Empty<U,V>() : Map U V;

-

-axiom (forall<U,V> u: U :: 

-  { Map#Domain(Map#Empty(): Map U V)[u] } 

-  !Map#Domain(Map#Empty(): Map U V)[u]);

-

-axiom (forall<U,V> 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])));

-

-function Map#Glue<U,V>([U]bool, [U]V, Ty) : Map U V;

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { Map#Domain(Map#Glue(a, b, t)) } 

-  Map#Domain(Map#Glue(a, b, t)) == a);

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { Map#Elements(Map#Glue(a, b, t)) } 

-  Map#Elements(Map#Glue(a, b, t)) == b);

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { $Is(Map#Glue(a, b, t), t) } 

-  $Is(Map#Glue(a, b, t), t));

-

-function Map#Build<U,V>(Map U V, U, V) : Map U V;

-

-axiom (forall<U,V> m: Map U V, u: U, u': U, v: V :: 

-  { Map#Domain(Map#Build(m, u, v))[u'] } { 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']));

-

-axiom (forall<U,V> m: Map U V, u: U, v: V :: 

-  { Map#Card(Map#Build(m, u, v)) } 

-  Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));

-

-axiom (forall<U,V> m: Map U V, u: U, v: V :: 

-  { Map#Card(Map#Build(m, u, v)) } 

-  !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);

-

-function Map#Equal<U,V>(Map U V, Map U V) : bool;

-

-axiom (forall<U,V> m: Map U V, m': Map U V :: 

-  { Map#Equal(m, m') } 

-  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]));

-

-axiom (forall<U,V> m: Map U V, m': Map U V :: 

-  { Map#Equal(m, m') } 

-  Map#Equal(m, m') ==> m == m');

-

-function Map#Disjoint<U,V>(Map U V, Map U V) : bool;

-

-axiom (forall<U,V> 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]));

-

-type IMap _ _;

-

-function IMap#Domain<U,V>(IMap U V) : [U]bool;

-

-function IMap#Elements<U,V>(IMap U V) : [U]V;

-

-function IMap#Empty<U,V>() : IMap U V;

-

-axiom (forall<U,V> u: U :: 

-  { IMap#Domain(IMap#Empty(): IMap U V)[u] } 

-  !IMap#Domain(IMap#Empty(): IMap U V)[u]);

-

-function IMap#Glue<U,V>([U]bool, [U]V, Ty) : IMap U V;

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { IMap#Domain(IMap#Glue(a, b, t)) } 

-  IMap#Domain(IMap#Glue(a, b, t)) == a);

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { IMap#Elements(IMap#Glue(a, b, t)) } 

-  IMap#Elements(IMap#Glue(a, b, t)) == b);

-

-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty :: 

-  { $Is(IMap#Glue(a, b, t), t) } 

-  $Is(IMap#Glue(a, b, t), t));

-

-function IMap#Build<U,V>(IMap U V, U, V) : IMap U V;

-

-axiom (forall<U,V> m: IMap U V, u: U, u': U, v: V :: 

-  { IMap#Domain(IMap#Build(m, u, v))[u'] } 

-    { IMap#Elements(IMap#Build(m, u, v))[u'] } 

-  (u' == u

-       ==> IMap#Domain(IMap#Build(m, u, v))[u']

-         && IMap#Elements(IMap#Build(m, u, v))[u'] == v)

-     && (u' != u

-       ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u']

-         && IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u']));

-

-function IMap#Equal<U,V>(IMap U V, IMap U V) : bool;

-

-axiom (forall<U,V> m: IMap U V, m': IMap U V :: 

-  { IMap#Equal(m, m') } 

-  IMap#Equal(m, m')

-     <==> (forall u: U :: IMap#Domain(m)[u] == IMap#Domain(m')[u])

-       && (forall u: U :: 

-        IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u]));

-

-axiom (forall<U,V> m: IMap U V, m': IMap U V :: 

-  { IMap#Equal(m, m') } 

-  IMap#Equal(m, m') ==> m == m');

-

-function INTERNAL_add_boogie(x: int, y: int) : int;

-

-axiom (forall x: int, y: int :: 

-  { INTERNAL_add_boogie(x, y): int } 

-  INTERNAL_add_boogie(x, y): int == x + y);

-

-function INTERNAL_sub_boogie(x: int, y: int) : int;

-

-axiom (forall x: int, y: int :: 

-  { INTERNAL_sub_boogie(x, y): int } 

-  INTERNAL_sub_boogie(x, y): int == x - y);

-

-function INTERNAL_mul_boogie(x: int, y: int) : int;

-

-axiom (forall x: int, y: int :: 

-  { INTERNAL_mul_boogie(x, y): int } 

-  INTERNAL_mul_boogie(x, y): int == x * y);

-

-function INTERNAL_div_boogie(x: int, y: int) : int;

-

-axiom (forall x: int, y: int :: 

-  { INTERNAL_div_boogie(x, y): int } 

-  INTERNAL_div_boogie(x, y): int == x div y);

-

-function INTERNAL_mod_boogie(x: int, y: int) : int;

-

-axiom (forall x: int, y: int :: 

-  { INTERNAL_mod_boogie(x, y): int } 

-  INTERNAL_mod_boogie(x, y): int == x mod y);

-

-function {:never_pattern true} INTERNAL_lt_boogie(x: int, y: int) : bool;

-

-axiom (forall x: int, y: int :: 

-  {:never_pattern true} { INTERNAL_lt_boogie(x, y): bool } 

-  INTERNAL_lt_boogie(x, y): bool == (x < y));

-

-function {:never_pattern true} INTERNAL_le_boogie(x: int, y: int) : bool;

-

-axiom (forall x: int, y: int :: 

-  {:never_pattern true} { INTERNAL_le_boogie(x, y): bool } 

-  INTERNAL_le_boogie(x, y): bool == (x <= y));

-

-function {:never_pattern true} INTERNAL_gt_boogie(x: int, y: int) : bool;

-

-axiom (forall x: int, y: int :: 

-  {:never_pattern true} { INTERNAL_gt_boogie(x, y): bool } 

-  INTERNAL_gt_boogie(x, y): bool == (x > y));

-

-function {:never_pattern true} INTERNAL_ge_boogie(x: int, y: int) : bool;

-

-axiom (forall x: int, y: int :: 

-  {:never_pattern true} { INTERNAL_ge_boogie(x, y): bool } 

-  INTERNAL_ge_boogie(x, y): bool == (x >= y));

-

-const unique class._System.object: ClassName;

-

-// Tclass._System.object Tag

-axiom Tag(Tclass._System.object()) == Tagclass._System.object;

-

-const unique Tagclass._System.object: TyTag;

-

-// Box/unbox axiom for Tclass._System.object

-axiom (forall bx: Box :: 

-  { $IsBox(bx, Tclass._System.object()) } 

-  $IsBox(bx, Tclass._System.object())

-     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.object()));

-

-// object: Class $Is

-axiom (forall $o: ref :: 

-  { $Is($o, Tclass._System.object()) } 

-  $Is($o, Tclass._System.object()));

-

-// object: Class $IsAlloc

-axiom (forall $o: ref, $h: Heap :: 

-  { $IsAlloc($o, Tclass._System.object(), $h) } 

-  $IsAlloc($o, Tclass._System.object(), $h) <==> $o == null || read($h, $o, alloc));

-

-const unique class._System.array: ClassName;

-

-function Tclass._System.array(Ty) : Ty;

-

-// Tclass._System.array Tag

-axiom (forall #$arg: Ty :: 

-  { Tclass._System.array(#$arg) } 

-  Tag(Tclass._System.array(#$arg)) == Tagclass._System.array);

-

-const unique Tagclass._System.array: TyTag;

-

-// Tclass._System.array injectivity 0

-axiom (forall #$arg: Ty :: 

-  { Tclass._System.array(#$arg) } 

-  Tclass._System.array_0(Tclass._System.array(#$arg)) == #$arg);

-

-function Tclass._System.array_0(Ty) : Ty;

-

-// Box/unbox axiom for Tclass._System.array

-axiom (forall #$arg: Ty, bx: Box :: 

-  { $IsBox(bx, Tclass._System.array(#$arg)) } 

-  $IsBox(bx, Tclass._System.array(#$arg))

-     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.array(#$arg)));

-

-// array.: Allocation axiom

-axiom (forall #$arg: Ty, $i0: int, $h: Heap, $o: ref :: 

-  { read($h, $o, IndexField($i0)), Tclass._System.array(#$arg) } 

-  $IsGoodHeap($h)

-       && $o != null

-       && dtype($o) == Tclass._System.array(#$arg)

-       && 

-      0 <= $i0

-       && $i0 < _System.array.Length($o)

-     ==> $IsBox(read($h, $o, IndexField($i0)), #$arg)

-       && (read($h, $o, alloc) ==> $IsAllocBox(read($h, $o, IndexField($i0)), #$arg, $h)));

-

-// array: Class $Is

-axiom (forall #$arg: Ty, $o: ref :: 

-  { $Is($o, Tclass._System.array(#$arg)) } 

-  $Is($o, Tclass._System.array(#$arg))

-     <==> $o == null || dtype($o) == Tclass._System.array(#$arg));

-

-// array: Class $IsAlloc

-axiom (forall #$arg: Ty, $o: ref, $h: Heap :: 

-  { $IsAlloc($o, Tclass._System.array(#$arg), $h) } 

-  $IsAlloc($o, Tclass._System.array(#$arg), $h)

-     <==> $o == null || read($h, $o, alloc));

-

-// array.Length: Allocation axiom

-axiom (forall #$arg: Ty, $h: Heap, $o: ref :: 

-  $IsGoodHeap($h) && $o != null && dtype($o) == Tclass._System.array(#$arg)

-     ==> $Is(_System.array.Length($o), TInt)

-       && (read($h, $o, alloc) ==> $IsAlloc(_System.array.Length($o), TInt, $h)));

-

-function Tclass._System.___hFunc0(Ty) : Ty;

-

-// Tclass._System.___hFunc0 Tag

-axiom (forall #$T0: Ty :: 

-  { Tclass._System.___hFunc0(#$T0) } 

-  Tag(Tclass._System.___hFunc0(#$T0)) == Tagclass._System.___hFunc0);

-

-const unique Tagclass._System.___hFunc0: TyTag;

-

-// Tclass._System.___hFunc0 injectivity 0

-axiom (forall #$T0: Ty :: 

-  { Tclass._System.___hFunc0(#$T0) } 

-  Tclass._System.___hFunc0_0(Tclass._System.___hFunc0(#$T0)) == #$T0);

-

-function Tclass._System.___hFunc0_0(Ty) : Ty;

-

-// Box/unbox axiom for Tclass._System.___hFunc0

-axiom (forall #$T0: Ty, bx: Box :: 

-  { $IsBox(bx, Tclass._System.___hFunc0(#$T0)) } 

-  $IsBox(bx, Tclass._System.___hFunc0(#$T0))

-     ==> $Box($Unbox(bx): HandleType) == bx

-       && $Is($Unbox(bx): HandleType, Tclass._System.___hFunc0(#$T0)));

-

-function Handle0([Heap]Box, [Heap]bool, [Heap]Set Box) : HandleType;

-

-function Apply0(Ty, HandleType, Heap) : Box;

-

-function Requires0(Ty, HandleType, Heap) : bool;

-

-function Reads0(Ty, HandleType, Heap) : Set Box;

-

-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: 

-  { Apply0(t0, Handle0(h, r, rd), heap) } 

-  Apply0(t0, Handle0(h, r, rd), heap) == h[heap]);

-

-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: 

-  { Requires0(t0, Handle0(h, r, rd), heap) } 

-  r[heap] ==> Requires0(t0, Handle0(h, r, rd), heap));

-

-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box, bx: Box :: 

-  { Reads0(t0, Handle0(h, r, rd), heap)[bx] } 

-  Reads0(t0, Handle0(h, r, rd), heap)[bx] == rd[heap][bx]);

-

-function {:inline true} _System.___hFunc0.requires(t0: Ty, heap: Heap, f: HandleType) : bool

-{

-  Requires0(t0, f, heap)

-}

-

-function {:inline true} _System.___hFunc0.requires#canCall(t0: Ty, heap: Heap, f: HandleType) : bool

-{

-  true

-}

-

-function {:inline true} _System.___hFunc0.reads(t0: Ty, heap: Heap, f: HandleType) : Set Box

-{

-  Reads0(t0, f, heap)

-}

-

-function {:inline true} _System.___hFunc0.reads#canCall(t0: Ty, heap: Heap, f: HandleType) : bool

-{

-  true

-}

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Reads0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h0)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Reads0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h1)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Requires0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h0)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Requires0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h1)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Apply0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h0)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));

-

-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: 

-  { $HeapSucc(h0, h1), Apply0(t0, f, h1) } 

-  $HeapSucc(h0, h1)

-       && 

-      $IsGoodHeap(h0)

-       && $IsGoodHeap(h1)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)

-       && (forall<a> o: ref, fld: Field a :: 

-        o != null

-             && read(h0, o, alloc)

-             && read(h1, o, alloc)

-             && Reads0(t0, f, h1)[$Box(o)]

-           ==> read(h0, o, fld) == read(h1, o, fld))

-     ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));

-

-axiom (forall t0: Ty, h: Heap, f: HandleType :: 

-  { Apply0(t0, f, h) } 

-  $IsGoodHeap(h)

-       && 

-      $Is(f, Tclass._System.___hFunc0(t0))

-       && $IsAlloc(f, Tclass._System.___hFunc0(t0), h)

-     ==> $IsBox(Apply0(t0, f, h), t0) && $IsAllocBox(Apply0(t0, f, h), t0, h));

-

-const unique class._module.__default: ClassName;

-

-function Tclass._module.__default() : Ty;

-

-// Tclass._module.__default Tag

-axiom Tag(Tclass._module.__default()) == Tagclass._module.__default;

-

-const unique Tagclass._module.__default: TyTag;

-

-// Box/unbox axiom for Tclass._module.__default

-axiom (forall bx: Box :: 

-  { $IsBox(bx, Tclass._module.__default()) } 

-  $IsBox(bx, Tclass._module.__default())

-     ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._module.__default()));

-

-// _default: Class $Is

-axiom (forall $o: ref :: 

-  { $Is($o, Tclass._module.__default()) } 

-  $Is($o, Tclass._module.__default())

-     <==> $o == null || dtype($o) == Tclass._module.__default());

-

-// _default: Class $IsAlloc

-axiom (forall $o: ref, $h: Heap :: 

-  { $IsAlloc($o, Tclass._module.__default(), $h) } 

-  $IsAlloc($o, Tclass._module.__default(), $h)

-     <==> $o == null || read($h, $o, alloc));

-

-procedure CheckWellformed$$_module.__default.test();

-  free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;

-  modifies $Heap, $Tick;

-

-

-

-implementation CheckWellformed$$_module.__default.test()

-{

-  var $_Frame: <beta>[ref,Field beta]bool;

-

-    // AddMethodImpl: test, CheckWellformed$$_module.__default.test

-    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 

-  $o != null && read($Heap, $o, alloc) ==> false);

-    assume {:captureState "Bug136.dfy(4,7): initial state"} true;

-    havoc $Heap;

-    assume (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-    assume $HeapSucc(old($Heap), $Heap);

-}

-

-

-

-procedure InterModuleCall$$_module.__default.test();

-  modifies $Heap, $Tick;

-  // frame condition

-  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  // boilerplate

-  free ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-procedure IntraModuleCall$$_module.__default.test();

-  modifies $Heap, $Tick;

-  // frame condition

-  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  // boilerplate

-  free ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-procedure Impl$$_module.__default.test() returns ($_reverifyPost: bool);

-  free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;

-  modifies $Heap, $Tick;

-  // frame condition

-  free ensures (forall<alpha> $o: ref, $f: Field alpha :: 

-  { read($Heap, $o, $f) } 

-  $o != null && read(old($Heap), $o, alloc)

-     ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));

-  // boilerplate

-  free ensures $HeapSucc(old($Heap), $Heap);

-

-

-

-implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool)

-{

-  var $_Frame: <beta>[ref,Field beta]bool;

-

-    // AddMethodImpl: test, Impl$$_module.__default.test

-    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 

-  $o != null && read($Heap, $o, alloc) ==> false);

-    assume {:captureState "Bug136.dfy(5,1): initial state"} true;

-    $_reverifyPost := false;

-    // ----- assume statement ----- Bug136.dfy(6,5)

-    assume true;

-    assume false;

-    // ----- assert statement ----- Bug136.dfy(7,5)

-    assume true;

-    assert true;

-}

-

-

 

 Dafny program verifier finished with 2 verified, 0 errors