// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"


type elements;

type struct;

var $Heap: [ref,name]any;
function cast<S,T>(S) returns (T);
function IsHeap(h: [ref,name]any) returns (bool);

const unique $allocated: name;

const unique $elements: name;

const unique $inv: name;

const unique $writable: name;

const unique $sharingMode: name;

const unique $SharingMode_Unshared: name;

const unique $SharingMode_LockProtected: name;

function ClassRepr(class: name) returns (ref);

axiom (forall c0: name, c1: name :: c0 != c1 ==> ClassRepr(c0) != ClassRepr(c1));

axiom (forall T: name :: !($typeof(ClassRepr(T)) <: System.Object));

axiom (forall T: name :: ClassRepr(T) != null);

axiom (forall T: name, h: [ref,name]any :: { h[ClassRepr(T), $writable] } IsHeap(h) ==> cast(h[ClassRepr(T), $writable]):bool);

function IsDirectlyModifiableField(f: name) returns (bool);

axiom !IsDirectlyModifiableField($allocated);

axiom IsDirectlyModifiableField($elements);

axiom !IsDirectlyModifiableField($inv);

axiom !IsDirectlyModifiableField($writable);

function IsStaticField(f: name) returns (bool);

axiom !IsStaticField($allocated);

axiom !IsStaticField($elements);

axiom !IsStaticField($inv);

axiom !IsStaticField($writable);

function ValueArrayGet(elements, int) returns (any);

function ValueArraySet(elements, int, any) returns (elements);

function RefArrayGet(elements, int) returns (ref);

function RefArraySet(elements, int, ref) returns (elements);

axiom (forall A: elements, i: int, x: any :: ValueArrayGet(ValueArraySet(A, i, x), i) == x);

axiom (forall A: elements, i: int, j: int, x: any :: i != j ==> ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j));

axiom (forall A: elements, i: int, x: ref :: RefArrayGet(RefArraySet(A, i, x), i) == x);

axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j));

function ArrayIndex(arr: ref, dim: int, indexAtDim: int, remainingIndexContribution: int) returns (int);

axiom (forall a: ref, d: int, x: int, y: int, x': int, y': int :: ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y') ==> x == x' && y == y');

axiom (forall a: ref, T: name, i: int, r: int, heap: [ref,name]any :: $typeof(a) <: RefArray(T, r) ==> $Is(RefArrayGet(cast(heap[a, $elements]):elements, i), T));

function $Rank(ref) returns (int);

axiom (forall a: ref :: 1 <= $Rank(a));

axiom (forall a: ref, T: name, r: int :: { $Is(a, ValueArray(T, r)) } $Is(a, ValueArray(T, r)) ==> $Rank(a) == r);

axiom (forall a: ref, T: name, r: int :: { $Is(a, RefArray(T, r)) } $Is(a, RefArray(T, r)) ==> $Rank(a) == r);

function $Length(ref) returns (int);

axiom (forall a: ref :: { $Length(a) } 0 <= $Length(a));

function $DimLength(ref, int) returns (int);

axiom (forall a: ref, i: int :: 0 <= $DimLength(a, i));

axiom (forall a: ref :: $Rank(a) == 1 ==> $DimLength(a, 0) == $Length(a));

function $LBound(ref, int) returns (int);

function $UBound(ref, int) returns (int);

axiom (forall a: ref, i: int :: { $LBound(a, i) } $LBound(a, i) == 0);

axiom (forall a: ref, i: int :: { $UBound(a, i) } $UBound(a, i) == $DimLength(a, i) - 1);

const unique System.Array: name;

axiom $IsClass(System.Array);

axiom System.Array <: System.Object;

function $ElementType(name) returns (name);

function ValueArray(elementType: name, rank: int) returns (name);

axiom (forall T: name, r: int :: { ValueArray(T, r) } ValueArray(T, r) <: System.Array);

function RefArray(elementType: name, rank: int) returns (name);

axiom (forall T: name, r: int :: { RefArray(T, r) } RefArray(T, r) <: System.Array);

axiom (forall T: name, U: name, r: int :: U <: T ==> RefArray(U, r) <: RefArray(T, r));

axiom (forall A: name, r: int :: $ElementType(ValueArray(A, r)) == A);

axiom (forall A: name, r: int :: $ElementType(RefArray(A, r)) == A);

axiom (forall A: name, r: int, T: name :: { T <: RefArray(A, r) } T <: RefArray(A, r) ==> T == RefArray($ElementType(T), r) && $ElementType(T) <: A);

axiom (forall A: name, r: int, T: name :: { T <: ValueArray(A, r) } T <: ValueArray(A, r) ==> T == ValueArray(A, r));

axiom (forall A: name, r: int, T: name :: RefArray(A, r) <: T ==> System.Array <: T || (T == RefArray($ElementType(T), r) && A <: $ElementType(T)));

axiom (forall A: name, r: int, T: name :: ValueArray(A, r) <: T ==> System.Array <: T || T == ValueArray(A, r));

function $ArrayPtr(elementType: name) returns (name);

function $StructGet(struct, name) returns (any);

function $StructSet(struct, name, any) returns (struct);

axiom (forall s: struct, f: name, x: any :: $StructGet($StructSet(s, f, x), f) == x);

axiom (forall s: struct, f: name, f': name, x: any :: f != f' ==> $StructGet($StructSet(s, f, x), f') == $StructGet(s, f'));

function ZeroInit(s: struct, typ: name) returns (bool);

function $typeof(ref) returns (name);

function Implements(class: name, interface: name) returns (bool);

axiom (forall T: name, J: name :: { Implements(T, J) } Implements(T, J) ==> T <: J);

function InterfaceExtends(subIntf: name, superIntf: name) returns (bool);

axiom (forall J: name, K: name :: { InterfaceExtends(J, K) } InterfaceExtends(J, K) ==> J <: K);

function $IsClass(name) returns (bool);

axiom (forall C: name :: { $IsClass(C) } $IsClass(C) ==> C <: C);

function AsDirectSubClass(sub: name, base: name) returns (sub': name);

function OneClassDown(sub: name, base: name) returns (directSub: name);

axiom (forall A: name, B: name, C: name :: { C <: AsDirectSubClass(B, A) } C <: AsDirectSubClass(B, A) ==> OneClassDown(C, A) == B);

function $IsInterface(name) returns (bool);

axiom (forall J: name :: { $IsInterface(J) } $IsInterface(J) ==> J <: System.Object);

function $IsValueType(name) returns (bool);

axiom (forall T: name :: $IsValueType(T) ==> (forall U: name :: T <: U ==> T == U) && (forall U: name :: U <: T ==> T == U));

const unique System.Object: name;

axiom $IsClass(System.Object);

function $IsTokenForType(struct, name) returns (bool);

function TypeObject(name) returns (ref);

const unique System.Type: name;

axiom System.Type <: System.Object;

axiom (forall T: name :: { TypeObject(T) } $IsNotNull(TypeObject(T), System.Type));

function $Is(ref, name) returns (bool);

axiom (forall o: ref, T: name :: { $Is(o, T) } $Is(o, T) <==> o == null || $typeof(o) <: T);

function $IsNotNull(ref, name) returns (bool);

axiom (forall o: ref, T: name :: { $IsNotNull(o, T) } $IsNotNull(o, T) <==> o != null && $Is(o, T));

function $As(ref, name) returns (ref);

axiom (forall o: ref, T: name :: $Is(o, T) ==> $As(o, T) == o);

axiom (forall o: ref, T: name :: !$Is(o, T) ==> $As(o, T) == null);

axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, RefArray(A, r)) ==> heap[o, $inv] == $typeof(o));

axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, ValueArray(A, r)) ==> heap[o, $inv] == $typeof(o));

function IsAllocated(h: [ref,name]any, o: any) returns (bool);

axiom (forall h: [ref,name]any, o: ref, f: name :: { IsAllocated(h, h[o, f]) } IsHeap(h) ==> IsAllocated(h, h[o, f]));

axiom (forall h: [ref,name]any, s: struct, f: name :: { IsAllocated(h, $StructGet(s, f)) } IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f)));

axiom (forall h: [ref,name]any, e: elements, i: int :: { IsAllocated(h, RefArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i)));

axiom (forall h: [ref,name]any, o: ref :: { h[o, $allocated] } IsAllocated(h, o) ==> cast(h[o, $allocated]):bool);

axiom (forall h: [ref,name]any, c: name :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> cast(h[ClassRepr(c), $allocated]):bool);

function DeclType(field: name) returns (class: name);

function AsNonNullRefField(field: name, T: name) returns (f: name);

function AsRefField(field: name, T: name) returns (f: name);

function AsRangeField(field: name, T: name) returns (f: name);

axiom (forall f: name, T: name :: { AsNonNullRefField(f, T) } AsNonNullRefField(f, T) == f ==> AsRefField(f, T) == f);

axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRefField(f, T)] } IsHeap(h) ==> $Is(cast(h[o, AsRefField(f, T)]):ref, T));

axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsNonNullRefField(f, T)] } IsHeap(h) ==> cast(h[o, AsNonNullRefField(f, T)]):ref != null);

axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRangeField(f, T)] } IsHeap(h) ==> InRange(cast(h[o, AsRangeField(f, T)]):int, T));

const unique System.String: name;

axiom (forall h: [ref,name]any, s: ref :: IsHeap(h) && $typeof(s) == System.String ==> h[s, $inv] == $typeof(s) && cast(h[s, $writable]):bool);

function AsOwnedField(f: name) returns (name);

axiom (forall h: [ref,name]any, o: ref, f: name :: { h[o, AsOwnedField(f)] } IsHeap(h) && cast(h[o, $inv]):name <: DeclType(AsOwnedField(f)) ==> cast(h[o, AsOwnedField(f)]):ref == null || $typeof(cast(h[o, AsOwnedField(f)]):ref) == System.String || !cast(h[cast(h[o, AsOwnedField(f)]):ref, $writable]):bool);

axiom (forall h: [ref,name]any, o: ref :: { h[o, $writable] } IsHeap(h) && !cast(h[o, $writable]):bool ==> cast(h[o, $inv]):name == $typeof(o));

function Box(any, ref) returns (ref);

function Unbox(ref) returns (any);

axiom (forall x: any, p: ref :: { Unbox(Box(x, p)) } Unbox(Box(x, p)) == x);

axiom (forall heap: [ref,name]any, x: any, p: ref :: { heap[Box(x, p), $inv] } IsHeap(heap) ==> heap[Box(x, p), $inv] == $typeof(Box(x, p)));

function UnboxedType(ref) returns (name);

function BoxTester(p: ref, typ: name) returns (ref);

axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } UnboxedType(p) == typ <==> BoxTester(p, typ) != null);

const unique System.Int16: name;

axiom $IsValueType(System.Int16);

const unique System.Int32: name;

axiom $IsValueType(System.Int32);

const unique System.Int64: name;

axiom $IsValueType(System.Int64);

const unique System.Byte: name;

axiom $IsValueType(System.Byte);

const unique System.Int16.MinValue: int;

const unique System.Int16.MaxValue: int;

const unique System.Int32.MinValue: int;

const unique System.Int32.MaxValue: int;

const unique System.Int64.MinValue: int;

const unique System.Int64.MaxValue: int;

axiom System.Int64.MinValue < System.Int32.MinValue;

axiom System.Int32.MinValue < System.Int16.MinValue;

axiom System.Int16.MinValue < System.Int16.MaxValue;

axiom System.Int16.MaxValue < System.Int32.MaxValue;

axiom System.Int32.MaxValue < System.Int64.MaxValue;

function InRange(i: int, T: name) returns (bool);

axiom (forall i: int :: InRange(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue);

axiom (forall i: int :: InRange(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue);

axiom (forall i: int :: InRange(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue);

axiom (forall i: int :: { InRange(i, System.Byte) } InRange(i, System.Byte) <==> 0 <= i && i < 256);

function $RealToInt(real) returns (int);

function $IntToReal(int) returns (real);

function $SizeIs(name, int) returns (bool);

function $IfThenElse(bool, any, any) returns (any);

axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } b ==> $IfThenElse(b, x, y) == x);

axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } !b ==> $IfThenElse(b, x, y) == y);

function #neg(int) returns (int);

function #rneg(real) returns (real);

function #rdiv(real, real) returns (real);

function #and(int, int) returns (int);

function #or(int, int) returns (int);

function #xor(int, int) returns (int);

function #shl(int, int) returns (int);

function #shr(int, int) returns (int);

axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y);

axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y);

axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y);

axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0);

axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0);

axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y);

axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y);

axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y);

axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);

axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i);

axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2);

axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i);

axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2);

const unique $UnknownRef: ref;

const unique System.IComparable: name;

const unique Microsoft.Singularity.Applications.ThreadTest: name;

const unique System.Threading.Thread: name;

const unique System.Collections.IEnumerable: name;

const unique System.Threading.ThreadStart: name;

const unique System.ICloneable: name;

const unique System.MulticastDelegate: name;

const unique System.Delegate: name;

const unique $stringLiteral0: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral0, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral0, $allocated]):bool) && $IsNotNull($stringLiteral0, System.String) && $Length($stringLiteral0) == 13;

const unique $stringLiteral1: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral1, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral1, $allocated]):bool) && $IsNotNull($stringLiteral1, System.String) && $Length($stringLiteral1) == 14;

const unique $stringLiteral2: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral2, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral2, $allocated]):bool) && $IsNotNull($stringLiteral2, System.String) && $Length($stringLiteral2) == 11;

const unique $stringLiteral3: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral3, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral3, $allocated]):bool) && $IsNotNull($stringLiteral3, System.String) && $Length($stringLiteral3) == 18;

const unique $stringLiteral4: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral4, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral4, $allocated]):bool) && $IsNotNull($stringLiteral4, System.String) && $Length($stringLiteral4) == 19;

const unique $stringLiteral5: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral5, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral5, $allocated]):bool) && $IsNotNull($stringLiteral5, System.String) && $Length($stringLiteral5) == 14;

const unique $stringLiteral6: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral6, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral6, $allocated]):bool) && $IsNotNull($stringLiteral6, System.String) && $Length($stringLiteral6) == 15;

const unique $stringLiteral7: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral7, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral7, $allocated]):bool) && $IsNotNull($stringLiteral7, System.String) && $Length($stringLiteral7) == 11;

const unique $stringLiteral8: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral8, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral8, $allocated]):bool) && $IsNotNull($stringLiteral8, System.String) && $Length($stringLiteral8) == 19;

const unique $stringLiteral9: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral9, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral9, $allocated]):bool) && $IsNotNull($stringLiteral9, System.String) && $Length($stringLiteral9) == 20;

const unique $stringLiteral10: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral10, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral10, $allocated]):bool) && $IsNotNull($stringLiteral10, System.String) && $Length($stringLiteral10) == 22;

const unique $stringLiteral11: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral11, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral11, $allocated]):bool) && $IsNotNull($stringLiteral11, System.String) && $Length($stringLiteral11) == 21;

const unique $stringLiteral12: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral12, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral12, $allocated]):bool) && $IsNotNull($stringLiteral12, System.String) && $Length($stringLiteral12) == 23;

const unique $stringLiteral13: ref;

axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral13, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral13, $allocated]):bool) && $IsNotNull($stringLiteral13, System.String) && $Length($stringLiteral13) == 22;

axiom $IsClass(Microsoft.Singularity.Applications.ThreadTest);

axiom Microsoft.Singularity.Applications.ThreadTest <: System.Object && AsDirectSubClass(Microsoft.Singularity.Applications.ThreadTest, System.Object) == Microsoft.Singularity.Applications.ThreadTest;

axiom (forall $K: name :: { Microsoft.Singularity.Applications.ThreadTest <: $K } Microsoft.Singularity.Applications.ThreadTest <: $K <==> Microsoft.Singularity.Applications.ThreadTest == $K || System.Object <: $K);

function Inv_Microsoft.Singularity.Applications.ThreadTest(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) } Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest } { Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest ==> Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap));

procedure Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod();
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



implementation Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod()
{
  var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block1513$LoopPreheader: [ref,name]any;

  entry:
    assume IsHeap($Heap);
    goto block1479;

  block1479:
    goto block1496;

  block1496:
    // ----- load constant First thread!  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13)
    stack0o := $stringLiteral0;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant First thread!   ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13)
    stack0o := $stringLiteral1;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13)
    call Microsoft.Singularity.DebugStub.Print$System.String(stack0o);
    // ----- load constant 0  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,18)
    i := 0;
    goto block1513$LoopPreheader;

  block1513:
    // ----- default loop invariant: $inv field  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29)
    assert (forall $o: ref :: $Heap$block1513$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool != true);
    assert (forall $o: ref :: cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
    // ----- load constant 10  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29)
    stack0i := 10;
    // ----- binary operator  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29)
    stack0b := i >= stack0i;
    // ----- branch  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29)
    goto true1513to1547, false1513to1530;

  true1513to1547:
    assume stack0b == true;
    goto block1547;

  false1513to1530:
    assume stack0b == false;
    goto block1530;

  block1547:
    // ----- load constant First thread done!  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13)
    stack0o := $stringLiteral3;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant First thread done!   ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13)
    stack0o := $stringLiteral4;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13)
    call Microsoft.Singularity.DebugStub.Print$System.String(stack0o);
    // ----- return  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(31,10)
    return;

  block1530:
    // ----- load constant [0] ...      ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17)
    stack0o := $stringLiteral2;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17)
    // Commented out, to avoid problems with the theorem prover nondeterministically choosing this error over the one 12 lines above: call System.Console.WriteLine$System.String(stack0o);
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(26,17)
    call System.Threading.Thread.Yield();
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,37)
    local1 := i;
    // ----- load constant 1
    stack0i := 1;
    // ----- binary operator
    stack0i := local1 + stack0i;
    // ----- copy
    i := stack0i;
    // ----- copy
    stack0i := local1;
    // ----- branch
    goto block1513;

  block1513$LoopPreheader:
    $Heap$block1513$LoopPreheader := $Heap;
    goto block1513;

}



axiom $IsClass(System.String);

axiom System.String <: System.Object && AsDirectSubClass(System.String, System.Object) == System.String;

axiom $IsInterface(System.IComparable);

axiom (forall $K: name :: { System.IComparable <: $K } System.IComparable <: $K <==> System.IComparable == $K || System.Object == $K);

axiom Implements(System.String, System.IComparable);

axiom $IsInterface(System.ICloneable);

axiom (forall $K: name :: { System.ICloneable <: $K } System.ICloneable <: $K <==> System.ICloneable == $K || System.Object == $K);

axiom Implements(System.String, System.ICloneable);

axiom $IsInterface(System.Collections.IEnumerable);

axiom (forall $K: name :: { System.Collections.IEnumerable <: $K } System.Collections.IEnumerable <: $K <==> System.Collections.IEnumerable == $K || System.Object == $K);

axiom Implements(System.String, System.Collections.IEnumerable);

axiom (forall $K: name :: { System.String <: $K } System.String <: $K <==> System.String == $K || System.Object <: $K || System.IComparable <: $K || System.ICloneable <: $K || System.Collections.IEnumerable <: $K);

axiom (forall $U: name :: { $U <: System.String } $U <: System.String ==> $U == System.String);

function Inv_System.String(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.String(this, heap) } Inv_System.String(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.String } { Inv_System.String($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.String ==> Inv_System.String($o, heap));

procedure System.Console.WriteLine$System.String(value$in: ref);
  requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



procedure Microsoft.Singularity.DebugStub.Print$System.String(value$in: ref);
  requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



procedure System.Threading.Thread.Yield();
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



procedure Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod();
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



implementation Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod()
{
  var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block2516$LoopPreheader: [ref,name]any;

  entry:
    assume IsHeap($Heap);
    goto block2482;

  block2482:
    goto block2499;

  block2499:
    // ----- load constant Second thread!  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13)
    stack0o := $stringLiteral5;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant Second thread!   ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13)
    stack0o := $stringLiteral6;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13)
    call Microsoft.Singularity.DebugStub.Print$System.String(stack0o);
    // ----- load constant 0  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,18)
    i := 0;
    goto block2516$LoopPreheader;

  block2516:
    // ----- default loop invariant: $inv field  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29)
    assert (forall $o: ref :: $Heap$block2516$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool != true);
    assert (forall $o: ref :: cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
    // ----- load constant 10  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29)
    stack0i := 10;
    // ----- binary operator  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29)
    stack0b := i >= stack0i;
    // ----- branch  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29)
    goto true2516to2550, false2516to2533;

  true2516to2550:
    assume stack0b == true;
    goto block2550;

  false2516to2533:
    assume stack0b == false;
    goto block2533;

  block2550:
    // ----- load constant Second thread done!  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13)
    stack0o := $stringLiteral8;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant Second thread done!   ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13)
    stack0o := $stringLiteral9;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13)
    call Microsoft.Singularity.DebugStub.Print$System.String(stack0o);
    // ----- return  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(46,10)
    return;

  block2533:
    // ----- load constant     ... [1]  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17)
    stack0o := $stringLiteral7;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17)
    // Commented out, to avoid problems with the theorem prover nondeterministically choosing this error over the one 12 lines above: call System.Console.WriteLine$System.String(stack0o);
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(41,17)
    call System.Threading.Thread.Yield();
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,37)
    local1 := i;
    // ----- load constant 1
    stack0i := 1;
    // ----- binary operator
    stack0i := local1 + stack0i;
    // ----- copy
    i := stack0i;
    // ----- copy
    stack0i := local1;
    // ----- branch
    goto block2516;

  block2516$LoopPreheader:
    $Heap$block2516$LoopPreheader := $Heap;
    goto block2516;

}



procedure Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int);
  requires args$in == null || (cast($Heap[args$in, $writable]):bool == true && cast($Heap[args$in, $inv]):name == $typeof(args$in));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures IsAllocated($Heap, $result);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



implementation Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int)
{
  var args: ref, stack0o: ref, stack1o: ref, stack50000o: ref, t1: ref, t2: ref, i: int, stack0i: int, stack0b: bool, local3: int, return.value: int, SS$Display.Return.Local: int, $Heap$block3825$LoopPreheader: [ref,name]any;

  entry:
    assume IsHeap($Heap);
    args := args$in;
    assume $Is(args, RefArray(System.String, 1));
    assume cast($Heap[args$in, $allocated]):bool == true;
    goto block3791;

  block3791:
    goto block3808;

  block3808:
    stack0o := null;
    // ----- load function  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    havoc stack1o;
    // ----- new object  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    havoc stack50000o;
    assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart;
    $Heap[stack50000o, $allocated] := true;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    assert stack50000o != null;
    call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o);
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    stack0o := stack50000o;
    // ----- new object  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    havoc stack50000o;
    assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread;
    $Heap[stack50000o, $allocated] := true;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    assert stack50000o != null;
    call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o);
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    stack0o := stack50000o;
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13)
    t1 := stack0o;
    stack0o := null;
    // ----- load function  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    havoc stack1o;
    // ----- new object  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    havoc stack50000o;
    assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart;
    $Heap[stack50000o, $allocated] := true;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    assert stack50000o != null;
    call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o);
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    stack0o := stack50000o;
    // ----- new object  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    havoc stack50000o;
    assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread;
    $Heap[stack50000o, $allocated] := true;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    assert stack50000o != null;
    call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o);
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    stack0o := stack50000o;
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13)
    t2 := stack0o;
    // ----- load constant Starting first thread.  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13)
    stack0o := $stringLiteral10;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(55,13)
    assert t1 != null;
    call System.Threading.Thread.Start(t1);
    // ----- load constant Started first thread.  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13)
    stack0o := $stringLiteral11;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant Starting second thread.  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13)
    stack0o := $stringLiteral12;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(59,13)
    assert t2 != null;
    call System.Threading.Thread.Start(t2);
    // ----- load constant Started second thread.  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13)
    stack0o := $stringLiteral13;
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13)
    call System.Console.WriteLine$System.String(stack0o);
    // ----- load constant 0  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,18)
    i := 0;
    goto block3825$LoopPreheader;

  block3825:
    // ----- default loop invariant: $inv field  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29)
    assert (forall $o: ref :: $Heap$block3825$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool != true);
    assert (forall $o: ref :: cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
    // ----- load constant 30  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29)
    stack0i := 30;
    // ----- binary operator  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29)
    stack0b := i >= stack0i;
    // ----- branch  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29)
    goto true3825to3859, false3825to3842;

  true3825to3859:
    assume stack0b == true;
    goto block3859;

  false3825to3842:
    assume stack0b == false;
    goto block3842;

  block3859:
    // ----- load constant 0  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(66,13)
    return.value := 0;
    // ----- branch
    goto block3876;

  block3842:
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(64,17)
    call System.Threading.Thread.Yield();
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,37)
    local3 := i;
    // ----- load constant 1
    stack0i := 1;
    // ----- binary operator
    stack0i := local3 + stack0i;
    // ----- copy
    i := stack0i;
    // ----- copy
    stack0i := local3;
    // ----- branch
    goto block3825;

  block3876:
    // ----- copy
    SS$Display.Return.Local := return.value;
    // ----- copy  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10)
    stack0i := return.value;
    // ----- return  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10)
    $result := stack0i;
    return;

  block3825$LoopPreheader:
    $Heap$block3825$LoopPreheader := $Heap;
    goto block3825;

}



axiom $IsClass(System.Threading.ThreadStart);

axiom $IsClass(System.MulticastDelegate);

axiom $IsClass(System.Delegate);

axiom System.Delegate <: System.Object && AsDirectSubClass(System.Delegate, System.Object) == System.Delegate;

axiom Implements(System.Delegate, System.ICloneable);

axiom (forall $K: name :: { System.Delegate <: $K } System.Delegate <: $K <==> System.Delegate == $K || System.Object <: $K || System.ICloneable <: $K);

function Inv_System.Delegate(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Delegate(this, heap) } Inv_System.Delegate(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Delegate } { Inv_System.Delegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Delegate ==> Inv_System.Delegate($o, heap));

axiom System.MulticastDelegate <: System.Delegate && AsDirectSubClass(System.MulticastDelegate, System.Delegate) == System.MulticastDelegate;

axiom (forall $K: name :: { System.MulticastDelegate <: $K } System.MulticastDelegate <: $K <==> System.MulticastDelegate == $K || System.Delegate <: $K);

function Inv_System.MulticastDelegate(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.MulticastDelegate(this, heap) } Inv_System.MulticastDelegate(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.MulticastDelegate } { Inv_System.MulticastDelegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.MulticastDelegate ==> Inv_System.MulticastDelegate($o, heap));

axiom System.Threading.ThreadStart <: System.MulticastDelegate && AsDirectSubClass(System.Threading.ThreadStart, System.MulticastDelegate) == System.Threading.ThreadStart;

axiom (forall $K: name :: { System.Threading.ThreadStart <: $K } System.Threading.ThreadStart <: $K <==> System.Threading.ThreadStart == $K || System.MulticastDelegate <: $K);

axiom (forall $U: name :: { $U <: System.Threading.ThreadStart } $U <: System.Threading.ThreadStart ==> $U == System.Threading.ThreadStart);

function Inv_System.Threading.ThreadStart(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.ThreadStart(this, heap) } Inv_System.Threading.ThreadStart(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.ThreadStart } { Inv_System.Threading.ThreadStart($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.ThreadStart ==> Inv_System.Threading.ThreadStart($o, heap));

procedure System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(this: ref, object$in: ref, method$in: ref);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);
  ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.ThreadStart;



axiom $IsClass(System.Threading.Thread);

axiom System.Threading.Thread <: System.Object && AsDirectSubClass(System.Threading.Thread, System.Object) == System.Threading.Thread;

axiom (forall $K: name :: { System.Threading.Thread <: $K } System.Threading.Thread <: $K <==> System.Threading.Thread == $K || System.Object <: $K);

axiom (forall $U: name :: { $U <: System.Threading.Thread } $U <: System.Threading.Thread ==> $U == System.Threading.Thread);

function Inv_System.Threading.Thread(object: ref, heap: [ref,name]any) returns (result: bool);

axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.Thread(this, heap) } Inv_System.Threading.Thread(this, heap) <==> true);

axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.Thread } { Inv_System.Threading.Thread($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.Thread ==> Inv_System.Threading.Thread($o, heap));

procedure System.Threading.Thread..ctor$System.Threading.ThreadStart(this: ref, start$in: ref);
  requires start$in == null || (cast($Heap[start$in, $writable]):bool == true && cast($Heap[start$in, $inv]):name == $typeof(start$in));
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Threading.Thread <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);
  ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.Thread;
  ensures $Heap[this, $sharingMode] == $SharingMode_Unshared;



procedure System.Threading.Thread.Start(this: ref);
  requires cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == $typeof(this);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);



procedure Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(Microsoft.Singularity.Applications.ThreadTest <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);
  ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == Microsoft.Singularity.Applications.ThreadTest;
  ensures $Heap[this, $sharingMode] == $SharingMode_Unshared;



implementation Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref)
{

  entry:
    assume IsHeap($Heap);
    assume $IsNotNull(this, Microsoft.Singularity.Applications.ThreadTest);
    assume cast($Heap[this, $allocated]):bool == true;
    assume cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object;
    goto block4777;

  block4777:
    goto block4794;

  block4794:
    // ----- call  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,18)
    assert this != null;
    call System.Object..ctor(this);
    // ----- return  ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,28)
    assert this != null;
    assert cast($Heap[this, $writable]):bool == true && System.Object <: cast($Heap[this, $inv]):name;
    assert cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object;
    assert Inv_Microsoft.Singularity.Applications.ThreadTest(this, $Heap);
    $Heap[this, $inv] := Microsoft.Singularity.Applications.ThreadTest;
    return;

}



procedure System.Object..ctor(this: ref);
  modifies $Heap;
  free ensures IsHeap($Heap);
  free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Object <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]);
  free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true);
  free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool);
  free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]);
  ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object;
  ensures $Heap[this, $sharingMode] == $SharingMode_Unshared;



type ref, name, any;
const null : ref;