// Copyright (c) 2010, Microsoft Corp.
// Bytecode Translator prelude

type HeapType = [Ref][Field]Union;

procedure {:inline 1} Alloc() returns (x: Ref);
  modifies $Alloc;



implementation {:inline 1} Alloc() returns (x: Ref)
{
    assume $Alloc[x] == false && x != null;
    $Alloc[x] := true;
}



function {:builtin "MapAdd"} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapSub"} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapMul"} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapDiv"} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapMod"} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapConst"} DelegateMapconstint(int) : [Delegate]int;

function {:builtin "MapConst"} DelegateMapconstbool(bool) : [Delegate]bool;

function {:builtin "MapAnd"} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;

function {:builtin "MapOr"} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;

function {:builtin "MapNot"} DelegateMapnot([Delegate]bool) : [Delegate]bool;

function {:builtin "MapIte"} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;

function {:builtin "MapIte"} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;

function {:builtin "MapLe"} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool;

function {:builtin "MapLt"} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool;

function {:builtin "MapGe"} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool;

function {:builtin "MapGt"} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool;

function {:builtin "MapEq"} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool;

function {:builtin "MapIff"} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;

function {:builtin "MapImp"} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;

axiom MultisetEmpty == DelegateMapconstint(0);

function IsRef(u: Union) : bool;

axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x)));

axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x)));

axiom (forall x: Real :: { Real2Union(x) } Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x)));

axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x)));

axiom (forall x: Ref :: { Struct2Union(x) } Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x)));

function $TypeOfInv(Ref) : Type;

axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);

procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);



implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
{
    $result := $TypeOf($DynamicType(this));
}



axiom Union2Int($DefaultHeapValue) == 0;

axiom Union2Bool($DefaultHeapValue) == false;

axiom Union2Ref($DefaultHeapValue) == null;

function $ThreadDelegate(Ref) : Ref;

procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref);



implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
{
    assume $ThreadDelegate(this) == start$in;
}



procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref);



implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
{
    call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
}



procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);



implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
{
    $Exception := null;
    call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
}



procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);



procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref);



implementation {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
{
    assume $ThreadDelegate(this) == start$in;
}



procedure {:inline 1} System.Threading.Thread.Start(this: Ref);



implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
{
    call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
}



procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);



implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
{
    $Exception := null;
    call System.Threading.ThreadStart.Invoke(this);
}



procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);



procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref);



implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
{
  var d: Delegate;

    if (a == null)
    {
        c := b;
    }
    else if (b == null)
    {
        c := a;
    }
    else
    {
        call c := Alloc();
        assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b);
        assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
    }
}



procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref);



implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
{
  var d: Delegate;

    if (a == null)
    {
        c := null;
    }
    else if (b == null)
    {
        c := a;
    }
    else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty)
    {
        c := null;
    }
    else
    {
        call c := Alloc();
        assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
        assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0;
    }
}



procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);



implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
{
    call c := Alloc();
    assume $RefToDelegate(c) == d;
    assume $RefToDelegateMultiset(c) == MultisetSingleton(d);
}



procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);



procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);



implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool)
{
    $result := a$in == b$in;
}



implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool)
{
    $result := a$in != b$in;
}



var $Heap: HeapType;

function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Union
{
  H[o][f]
}

function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Union) : HeapType
{
  H[o := H[o][f := v]]
}

var $ArrayContents: [Ref][int]Union;

function $ArrayLength(Ref) : int;

type {:datatype} Delegate;

type DelegateMultiset = [Delegate]int;

const unique MultisetEmpty: DelegateMultiset;

function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset
{
  MultisetEmpty[x := 1]
}

function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
{
  DelegateMapadd(x, y)
}

function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
{
  DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0))
}

type Field;

type Union;

const unique $DefaultHeapValue: Union;

type Ref;

const unique null: Ref;

type {:datatype} Type;

type Real;

const unique $DefaultReal: Real;

procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref);



implementation {:inline 1} $BoxFromBool(b: bool) returns (r: Ref)
{
    call r := Alloc();
    assume $BoxedValue(r) == Bool2Union(b);
}



procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref);



implementation {:inline 1} $BoxFromInt(i: int) returns (r: Ref)
{
    call r := Alloc();
    assume $BoxedValue(r) == Int2Union(i);
}



procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref);



implementation {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref)
{
    call rf := Alloc();
    assume $BoxedValue(rf) == Real2Union(r);
}



procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref);



implementation {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref)
{
    call r := Alloc();
    assume $BoxedValue(r) == Struct2Union(s);
}



procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref);



implementation {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref)
{
    if (IsRef(u))
    {
        r := Union2Ref(u);
    }
    else
    {
        call r := Alloc();
        assume $BoxedValue(r) == u;
    }
}



function $BoxedValue(r: Ref) : Union;

function {:inline true} $Unbox2Bool(r: Ref) : bool
{
  Union2Bool($BoxedValue(r))
}

function {:inline true} $Unbox2Int(r: Ref) : int
{
  Union2Int($BoxedValue(r))
}

function {:inline true} $Unbox2Real(r: Ref) : Real
{
  Union2Real($BoxedValue(r))
}

function {:inline true} $Unbox2Struct(r: Ref) : Ref
{
  Union2Struct($BoxedValue(r))
}

function {:inline true} $Unbox2Union(r: Ref) : Union
{
  $BoxedValue(r)
}

function Union2Bool(u: Union) : bool;

function Union2Int(u: Union) : int;

function Union2Ref(u: Union) : Ref;

function Union2Real(u: Union) : Real;

function Union2Struct(u: Union) : Ref;

function Bool2Union(boolValue: bool) : Union;

function Int2Union(intValue: int) : Union;

function Ref2Union(refValue: Ref) : Union;

function Real2Union(realValue: Real) : Union;

function Struct2Union(structValue: Ref) : Union;

function {:inline true} Union2Union(u: Union) : Union
{
  u
}

function Int2Real(int) : Real;

function Real2Int(Real) : int;

function RealPlus(Real, Real) : Real;

function RealMinus(Real, Real) : Real;

function RealTimes(Real, Real) : Real;

function RealDivide(Real, Real) : Real;

function RealModulus(Real, Real) : Real;

function RealLessThan(Real, Real) : bool;

function RealLessThanOrEqual(Real, Real) : bool;

function RealGreaterThan(Real, Real) : bool;

function RealGreaterThanOrEqual(Real, Real) : bool;

function BitwiseAnd(int, int) : int;

function BitwiseOr(int, int) : int;

function BitwiseExclusiveOr(int, int) : int;

function BitwiseNegation(int) : int;

function RightShift(int, int) : int;

function LeftShift(int, int) : int;

function $DynamicType(Ref) : Type;

function $TypeOf(Type) : Ref;

function $As(Ref, Type) : Ref;

function $Subtype(Type, Type) : bool;

function $DisjointSubtree(Type, Type) : bool;

var $Alloc: [Ref]bool;

function {:builtin "MapImp"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool;

function {:builtin "MapConst"} $allocConstBool(bool) : [Ref]bool;

function $RefToDelegate(Ref) : Delegate;

function $RefToDelegateMultiset(Ref) : DelegateMultiset;

function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate;

var {:thread_local} $Exception: Ref;





function {:constructor} T$RegressionTestInput.StructContainingStruct() : Type;

function {:constructor} {:extern} T$System.ValueType() : Type;

function {:constructor} {:extern} T$System.Object() : Type;

axiom (forall $T: Type :: { $Subtype(T$System.Object(), $T) } $Subtype(T$System.Object(), $T) <==> T$System.Object() == $T);

axiom (forall $T: Type :: { $Subtype(T$System.ValueType(), $T) } $Subtype(T$System.ValueType(), $T) <==> T$System.ValueType() == $T || $Subtype(T$System.Object(), $T));

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) } $Subtype(T$RegressionTestInput.StructContainingStruct(), $T) <==> T$RegressionTestInput.StructContainingStruct() == $T || $Subtype(T$System.ValueType(), $T));

procedure RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref);



const unique F$RegressionTestInput.StructContainingStruct.d: Field;

procedure RegressionTestInput.S.#default_ctor($this: Ref);



function {:constructor} T$RegressionTestInput.S() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

const unique F$RegressionTestInput.StructContainingStruct.s: Field;

implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref)
{
  var $tmp0: Ref;

    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.d, Real2Union($DefaultReal));
    call $tmp0 := Alloc();
    call RegressionTestInput.S.#default_ctor($tmp0);
    assume $DynamicType($tmp0) == T$RegressionTestInput.S();
    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp0));
}



procedure RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref);
  free ensures this != other;



procedure RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref);
  free ensures this != other;



implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor(this: Ref) returns (other: Ref)
{
  var $tmp1: Ref;

    call other := Alloc();
    assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct();
    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.d, Real2Union(Union2Real(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.d))));
    call $tmp1 := RegressionTestInput.S.#copy_ctor(Union2Ref(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.s)));
    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp1));
}



procedure RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref);
  free ensures $result == null || $Alloc[$result];
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionTestInput.StructContainingStruct($this: Ref, s$in: Ref) returns ($result: Ref)
{
  var s: Ref;
  var t_Ref: Ref;
  var $localExc: Ref;
  var $label: int;

    s := s$in;
    assume {:breadcrumb 0} true;
    call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);
    $result := t_Ref;
    return;
}



function {:constructor} T$RegressionTestInput.RealNumbers() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RealNumbers(), $T) } $Subtype(T$RegressionTestInput.RealNumbers(), $T) <==> T$RegressionTestInput.RealNumbers() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real)
{
  var d: Real;
  var $localExc: Ref;
  var $label: int;

    d := d$in;
    assume {:breadcrumb 1} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
    call System.Console.WriteLine$System.Double(d);
    if ($Exception != null)
    {
        return;
    }
}



procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref)
{
  var o: Ref;
  var $localExc: Ref;
  var $label: int;

    o := o$in;
    assume {:breadcrumb 2} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o));
    if ($Exception != null)
    {
        return;
    }
}



procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



const unique $real_literal_3_0: Real;

const unique $real_literal_4_0: Real;

implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
{
  var d_Real: Real;
  var d2_Real: Real;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 3} true;
    d_Real := $real_literal_3_0;
    d2_Real := $real_literal_4_0;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));
    if ($Exception != null)
    {
        return;
    }

    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));
    if ($Exception != null)
    {
        return;
    }

    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));
    if ($Exception != null)
    {
        return;
    }

    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
    if ($Exception != null)
    {
        return;
    }
}



procedure RegressionTestInput.RealNumbers.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



procedure {:extern} System.Object.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 4} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.RealNumbers.#cctor();



implementation T$RegressionTestInput.RealNumbers.#cctor()
{
}



function {:constructor} T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) } $Subtype(T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap(), $T) <==> T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap() == $T || $Subtype(T$System.Object(), $T));

const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 5} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
    assume $this != null;
    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(Union2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
}



procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Union(0));
    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(0));
    assume {:breadcrumb 6} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();



implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
{
}



function {:constructor} T$RegressionTestInput.CreateStruct() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.CreateStruct(), $T) } $Subtype(T$RegressionTestInput.CreateStruct(), $T) <==> T$RegressionTestInput.CreateStruct() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);
  free ensures $result == null || $Alloc[$result];
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



const unique F$RegressionTestInput.S.x: Field;

const unique F$RegressionTestInput.S.b: Field;

implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)
{
  var s_Ref: Ref;
  var $tmp0: Ref;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 7} true;
    call $tmp0 := Alloc();
    call RegressionTestInput.S.#default_ctor($tmp0);
    assume $DynamicType($tmp0) == T$RegressionTestInput.S();
    s_Ref := $tmp0;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
    assume s_Ref != null;
    assert Union2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
    assume s_Ref != null;
    assert !Union2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b));
    $result := s_Ref;
    return;
}



procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref);
  free ensures $result == null || $Alloc[$result];
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref)
{
  var s: Ref;
  var $localExc: Ref;
  var $label: int;

    s := s$in;
    assume {:breadcrumb 8} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
    $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Union(3));
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
    assume s != null;
    assert Union2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
    $result := s;
    return;
}



procedure RegressionTestInput.CreateStruct.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 9} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.CreateStruct.#cctor();



implementation T$RegressionTestInput.CreateStruct.#cctor()
{
}



function {:constructor} T$RegressionTestInput.ClassWithArrayTypes() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithArrayTypes(), $T) <==> T$RegressionTestInput.ClassWithArrayTypes() == $T || $Subtype(T$System.Object(), $T));

var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;

const unique F$RegressionTestInput.ClassWithArrayTypes.a: Field;

procedure RegressionTestInput.ClassWithArrayTypes.Main1();
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
  var s_Ref: Ref;
  var $tmp0: Ref;
  var t_Ref: Ref;
  var $tmp1: Ref;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 10} true;
    call $tmp0 := Alloc();
    assume $ArrayLength($tmp0) == 1 * 5;
    s_Ref := $tmp0;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
    assume s_Ref != null;
    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
    call $tmp1 := Alloc();
    assume $ArrayLength($tmp1) == 1 * 4;
    t_Ref := $tmp1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
    assume t_Ref != null;
    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
    assume s_Ref != null;
    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main2();
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
  var $tmp0: Ref;
  var t_Ref: Ref;
  var $tmp1: Ref;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 11} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
    call $tmp0 := Alloc();
    assume $ArrayLength($tmp0) == 1 * 5;
    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]];
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;
    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
    call $tmp1 := Alloc();
    assume $ArrayLength($tmp1) == 1 * 4;
    t_Ref := $tmp1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
    assume t_Ref != null;
    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
    assume F$RegressionTestInput.ClassWithArrayTypes.s != null;
    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int)
{
  var x: int;
  var $tmp0: Ref;
  var $tmp1: Ref;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 12} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
    assume $this != null;
    $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Union(42)]];
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
    assume $this != null;
    $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Union(43)]];
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
    assume $this != null;
    $tmp0 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
    assume $tmp0 != null;
    assume $this != null;
    $tmp1 := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
    assume $tmp1 != null;
    assert Union2Int($ArrayContents[$tmp0][x + 1]) == Union2Int($ArrayContents[$tmp1][x]) + 1;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Union(null));
    assume {:breadcrumb 14} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor();



implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
{
    F$RegressionTestInput.ClassWithArrayTypes.s := null;
}



function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T: Type) : Type;

axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1(T) == $T || $Subtype(T$System.Object(), $T));

const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;

procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Union(0));
    assume {:breadcrumb 15} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor();



implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor()
{
}



function {:constructor} T$RegressionTestInput.BitwiseOperations() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) } $Subtype(T$RegressionTestInput.BitwiseOperations(), $T) <==> T$RegressionTestInput.BitwiseOperations() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
  var x: int;
  var y: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    y := y$in;
    assume {:breadcrumb 16} true;
    $result := BitwiseAnd(x, y);
    return;
}



procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
  var x: int;
  var y: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    y := y$in;
    assume {:breadcrumb 17} true;
    $result := BitwiseOr(x, y);
    return;
}



procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
  var x: int;
  var y: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    y := y$in;
    assume {:breadcrumb 18} true;
    $result := BitwiseExclusiveOr(x, y);
    return;
}



procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int)
{
  var x: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 19} true;
    $result := BitwiseNegation(x);
    return;
}



procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 20} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.BitwiseOperations.#cctor();



implementation T$RegressionTestInput.BitwiseOperations.#cctor()
{
}



function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;

function {:constructor} {:extern} T$System.Attribute() : Type;

function {:constructor} {:extern} T$System.Runtime.InteropServices._Attribute() : Type;

axiom (forall $T: Type :: { $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) } $Subtype(T$System.Runtime.InteropServices._Attribute(), $T) <==> T$System.Runtime.InteropServices._Attribute() == $T);

axiom (forall $T: Type :: { $Subtype(T$System.Attribute(), $T) } $Subtype(T$System.Attribute(), $T) <==> T$System.Attribute() == $T || $Subtype(T$System.Object(), $T) || $Subtype(T$System.Runtime.InteropServices._Attribute(), $T));

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) } $Subtype(T$RegressionTestInput.AsyncAttribute(), $T) <==> T$RegressionTestInput.AsyncAttribute() == $T || $Subtype(T$System.Attribute(), $T));

procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



procedure {:extern} System.Attribute.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 21} true;
    call System.Attribute.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.AsyncAttribute.#cctor();



implementation T$RegressionTestInput.AsyncAttribute.#cctor()
{
}



function {:constructor} T$RegressionTestInput.RefParameters() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.RefParameters(), $T) } $Subtype(T$RegressionTestInput.RefParameters(), $T) <==> T$RegressionTestInput.RefParameters() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)
{
  var $localExc: Ref;
  var $label: int;

    x$out := x$in;
    assume {:breadcrumb 22} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
    x$out := x$out + 1;
}



procedure RegressionTestInput.RefParameters.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 23} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.RefParameters.#cctor();



implementation T$RegressionTestInput.RefParameters.#cctor()
{
}



function {:constructor} T$RegressionTestInput.NestedGeneric() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric(), $T) <==> T$RegressionTestInput.NestedGeneric() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 24} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



function {:constructor} T$RegressionTestInput.NestedGeneric.C() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C(), $T) <==> T$RegressionTestInput.NestedGeneric.C() == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 25} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



function {:constructor} T$RegressionTestInput.NestedGeneric.C.G`1(T: Type) : Type;

axiom (forall T: Type, $T: Type :: { $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) } $Subtype(T$RegressionTestInput.NestedGeneric.C.G`1(T), $T) <==> T$RegressionTestInput.NestedGeneric.C.G`1(T) == $T || $Subtype(T$System.Object(), $T));

procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)
{
  var x: int;
  var CS$0$0000_Union: Union;
  var $tmp0: Union;
  var $tmp1: Union;
  var $tmp2: Ref;
  var y_Union: Union;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 26} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
    CS$0$0000_Union := $DefaultHeapValue;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
    call $tmp2 := $BoxFromUnion(CS$0$0000_Union);
    if ($tmp2 != null)
    {
    }
    else
    {
        call $tmp1 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
        $tmp0 := Union2Union($tmp1);
        if ($Exception != null)
        {
            return;
        }
    }

    y_Union := (if $tmp2 != null then $DefaultHeapValue else $tmp0);
}



procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor();



implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor()
{
}



procedure T$RegressionTestInput.NestedGeneric.C.#cctor();



implementation T$RegressionTestInput.NestedGeneric.C.#cctor()
{
}



procedure T$RegressionTestInput.NestedGeneric.#cctor();



implementation T$RegressionTestInput.NestedGeneric.#cctor()
{
}



implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
{
    $Heap := Write($Heap, $this, F$RegressionTestInput.S.x, Int2Union(0));
    $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Union(false));
}



implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref)
{
    call other := Alloc();
    assume $DynamicType(other) == T$RegressionTestInput.S();
    $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Union(Union2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
    $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Union(Union2Bool(Read($Heap, this, F$RegressionTestInput.S.b))));
}



function {:constructor} T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) } $Subtype(T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric(), $T) <==> T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric() == $T || $Subtype(T$System.Object(), $T));

const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;

procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Union(0));
    assume {:breadcrumb 27} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor();



implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor()
{
}



function {:constructor} T$RegressionTestInput.Class0() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.Class0(), $T) } $Subtype(T$RegressionTestInput.Class0(), $T) <==> T$RegressionTestInput.Class0() == $T || $Subtype(T$System.Object(), $T));

var F$RegressionTestInput.Class0.StaticInt: int;

procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
{
  var x: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 28} true;
    $result := x + 1;
    return;
}



procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
{
  var x: int;
  var y_int: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 29} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
    x := 3;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
    y_int := 3 + 5 / x;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
    if (x != 3)
    {
    }
    else
    {
    }

    assert (if x != 3 then false else !(y_int > 8));
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
    F$RegressionTestInput.Class0.StaticInt := y_int;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
    assert y_int == F$RegressionTestInput.Class0.StaticInt;
}



procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int)
{
  var x: int;
  var y: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    y := y$in;
    assume {:breadcrumb 30} true;
}



procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool)
{
  var b: bool;
  var $localExc: Ref;
  var $label: int;

    b := b$in;
    assume {:breadcrumb 31} true;
}



procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref)
{
  var c: Ref;
  var $localExc: Ref;
  var $label: int;

    c := c$in;
    assume {:breadcrumb 32} true;
}



procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int)
{
  var $tmp0: int;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 33} true;
    call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
    if ($Exception != null)
    {
        return;
    }

    $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp0;
    return;
}



procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
  var $localExc: Ref;
  var $label: int;

    x$out := x$in;
    assume {:breadcrumb 34} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
    x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
    $result := x$out;
    return;
}



procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
  var $localExc: Ref;
  var $label: int;

    x$out := x$in;
    assume {:breadcrumb 35} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
    x$out := x$out + 1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
    F$RegressionTestInput.Class0.StaticInt := x$out;
    $result := x$out;
    return;
}



procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int)
{
  var x: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 36} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
    x := x + 1;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
    F$RegressionTestInput.Class0.StaticInt := x;
    $result := x;
    return;
}



procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int)
{
  var x: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    assume {:breadcrumb 37} true;
    $result := x;
    return;
}



procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int)
{
  var y: int;
  var $tmp0: int;
  var $localExc: Ref;
  var $label: int;

    y := y$in;
    assume {:breadcrumb 38} true;
    call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);
    if ($Exception != null)
    {
        return;
    }

    $result := $tmp0;
    return;
}



procedure RegressionTestInput.Class0.#ctor($this: Ref);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.Class0.#ctor($this: Ref)
{
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 39} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.Class0.#cctor();



implementation T$RegressionTestInput.Class0.#cctor()
{
    F$RegressionTestInput.Class0.StaticInt := 0;
}



function {:constructor} T$RegressionTestInput.ClassWithBoolTypes() : Type;

axiom (forall $T: Type :: { $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) } $Subtype(T$RegressionTestInput.ClassWithBoolTypes(), $T) <==> T$RegressionTestInput.ClassWithBoolTypes() == $T || $Subtype(T$System.Object(), $T));

var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;

const unique F$RegressionTestInput.ClassWithBoolTypes.b: Field;

procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)
{
  var x: int;
  var y: int;
  var $localExc: Ref;
  var $label: int;

    x := x$in;
    y := y$in;
    assume {:breadcrumb 40} true;
    $result := x < y;
    return;
}



procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool);
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool)
{
  var z: bool;
  var $localExc: Ref;
  var $label: int;

    z := z$in;
    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(false));
    assume {:breadcrumb 41} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(z));
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
    if (z)
    {
        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
        F$RegressionTestInput.ClassWithBoolTypes.staticB := z;
    }
    else
    {
    }
}



procedure RegressionTestInput.ClassWithBoolTypes.Main();
  free ensures $allocImp(old($Alloc), $Alloc) == $allocConstBool(true);



implementation RegressionTestInput.ClassWithBoolTypes.Main()
{
  var $tmp0: bool;
  var $localExc: Ref;
  var $label: int;

    assume {:breadcrumb 42} true;
    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
    call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
    if ($Exception != null)
    {
        return;
    }
}



procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor();



implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor()
{
    F$RegressionTestInput.ClassWithBoolTypes.staticB := false;
}