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

type HeapType = [Ref][Field]Box;

var $Alloc: [Ref]bool;

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"} mapadd([Delegate]int, [Delegate]int) : [Delegate]int;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

axiom MultisetEmpty == mapconstint(0);

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 Box2Int($DefaultBox) == 0;

axiom Box2Bool($DefaultBox) == false;

axiom Box2Ref($DefaultBox) == null;

axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);

axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);

axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x);

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 {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);



implementation {:inline 1} 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 {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);



implementation {:inline 1} 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 $Delegate(c) == MultisetPlus($Delegate(a), $Delegate(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($Delegate(a), $Delegate(b)) == MultisetEmpty)
    {
        c := null;
    }
    else
    {
        call c := Alloc();
        assume $Delegate(c) == MultisetMinus($Delegate(a), $Delegate(b));
    }
}



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



implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
{
    call c := Alloc();
    assume $Delegate(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 isControlEnabled: [Ref]bool;

var isControlChecked: [Ref]bool;

procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);



implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool)
{
    $Exception := null;
    isControlEnabled[$this] := value$in;
}



procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);



implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref)
{
  var enabledness: bool;

    $Exception := null;
    enabledness := isControlEnabled[$this];
    $result := Box2Ref(Bool2Box(enabledness));
}



procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);



implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref)
{
  var check: bool;

    $Exception := null;
    check := Box2Bool(Ref2Box(value$in));
    isControlChecked[$this] := check;
}



procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);



implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref)
{
  var isChecked: bool;

    $Exception := null;
    isChecked := isControlChecked[$this];
    $result := Box2Ref(Bool2Box(isChecked));
}



const unique $BoxField: Field;

var $Heap: HeapType;

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

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

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

function $ArrayLength(Ref) : int;

type {:datatype} Delegate;

type DelegateMultiset = [Delegate]int;

const unique MultisetEmpty: DelegateMultiset;

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

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

function {:inline} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
{
  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))
}

type Field;

type Box;

const unique $DefaultBox: Box;

type Ref;

const unique null: Ref;

type {:datatype} Type;

type Real;

const unique $DefaultReal: Real;

function Box2Bool(Box) : bool;

function Box2Int(Box) : int;

function Box2Ref(Box) : Ref;

function Box2Real(Box) : Real;

function Bool2Box(bool) : Box;

function Int2Box(int) : Box;

function Ref2Box(Ref) : Box;

function Real2Box(Real) : Box;

function {:inline true} Box2Box(b: Box) : Box
{
  b
}

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;

function $Delegate(Ref) : DelegateMultiset;

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

var {:thread_local} $Exception: Ref;





function {:constructor} T$RegressionTestInput.RealNumbers() : 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$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);



procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);



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

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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
    return;
}



procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref);



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

    o := o$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real(Read($Heap, o, $BoxField)));
    if ($Exception != null)
    {
        return;
    }

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
    return;
}



procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref);



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;

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
    d_Real := $real_literal_3_0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
    d2_Real := $real_literal_4_0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\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 {:sourceFile "C:\dev\BoogieCodePlex\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 {:sourceFile "C:\dev\BoogieCodePlex\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 {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
    if ($Exception != null)
    {
        return;
    }

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
    return;
}



procedure RegressionTestInput.RealNumbers.#ctor($this: Ref);



procedure {:extern} System.Object.#ctor($this: Ref);



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
    return;
}



procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref);



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

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

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



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



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

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

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.S(), $T) } $Subtype(T$RegressionTestInput.S(), $T) <==> T$RegressionTestInput.S() == $T || $Subtype(T$System.ValueType(), $T));

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 $tmp1: Ref;
  var $localExc: Ref;
  var $label: int;

    call $tmp0 := Alloc();
    call RegressionTestInput.S.#default_ctor($tmp0);
    assume $DynamicType($tmp0) == T$RegressionTestInput.S();
    s_Ref := $tmp0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
    call $tmp1 := Alloc();
    call RegressionTestInput.S.#default_ctor($tmp1);
    assume $DynamicType($tmp1) == T$RegressionTestInput.S();
    s_Ref := $tmp1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
    assert Box2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
    assert !Box2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b));
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
    $result := s_Ref;
    return;
}



procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
    $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
    assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
    $result := s;
    return;
}



procedure RegressionTestInput.CreateStruct.#ctor($this: Ref);



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
    call $tmp0 := Alloc();
    assume $ArrayLength($tmp0) == 1 * 5;
    s_Ref := $tmp0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
    $ArrayContents := $ArrayContents[s_Ref := $ArrayContents[s_Ref][0 := Int2Box(2)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
    call $tmp1 := Alloc();
    assume $ArrayLength($tmp1) == 1 * 4;
    t_Ref := $tmp1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
    return;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main2();



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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
    call $tmp0 := Alloc();
    assume $ArrayLength($tmp0) == 1 * 5;
    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
    call $tmp1 := Alloc();
    assume $ArrayLength($tmp1) == 1 * 4;
    t_Ref := $tmp1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
    return;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int);



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

    x := x$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
    _loc0_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
    _loc1_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
    assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
    return;
}



procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref);



implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
{
  var xs: Ref;
  var $localExc: Ref;
  var $label: int;

    xs := xs$in;
    if (xs != null)
    {
    }
    else
    {
    }

    if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
    {
        assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
        $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
    }
    else
    {
    }

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
    return;
}



procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref);



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

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

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



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

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

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



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} 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);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} 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);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
    $result := BitwiseExclusiveOr(x, y);
    return;
}



procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
    $result := BitwiseNegation(x);
    return;
}



procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref);



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



procedure {:extern} System.Attribute.#ctor($this: Ref);



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

    call System.Attribute.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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

    x$out := x$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
    x$out := x$out + 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
    return;
}



procedure RegressionTestInput.RefParameters.#ctor($this: Ref);



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Box);



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

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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
    CS$0$0000_Box := $DefaultBox;
    call $tmp0 := Alloc();
    $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000_Box));
    if ($tmp0 != null)
    {
        CS$0$0000_Box := $DefaultBox;
        __temp_2_Box := CS$0$0000_Box;
    }
    else
    {
        call $tmp2 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
        $tmp1 := Box2Box($tmp2);
        if ($Exception != null)
        {
            return;
        }

        __temp_3_Box := $tmp1;
        __temp_2_Box := __temp_3_Box;
    }

    y_Box := __temp_2_Box;
    return;
}



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, Int2Box(0));
    $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Box(false));
}



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



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, Int2Box(Box2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
    $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Box(Box2Bool(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);



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

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

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



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

    x := x$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
    $result := x + 1;
    return;
}



procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);



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

    x := x$in;
    __temp_1_int := 5 / x;
    x := 3;
    y_int := __temp_1_int + 3;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
    if (x == 3)
    {
    }
    else
    {
    }

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



procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
    return;
}



procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool);



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

    b := b$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
    return;
}



procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref);



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

    c := c$in;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
    return;
}



procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);



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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} 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);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
    x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
    $result := x$out;
    return;
}



procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
    x$out := x$out + 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
    F$RegressionTestInput.Class0.StaticInt := x$out;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
    $result := x$out;
    return;
}



procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
    x := x + 1;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
    F$RegressionTestInput.Class0.StaticInt := x;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
    $result := x;
    return;
}



procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
    $result := x;
    return;
}



procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int);



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
    call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);
    if ($Exception != null)
    {
        return;
    }

    $result := $tmp0;
    return;
}



procedure RegressionTestInput.Class0.#ctor($this: Ref);



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

    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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



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;
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
    $result := x < y;
    return;
}



procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool);



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, Bool2Box(false));
    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
    call System.Object.#ctor($this);
    if ($Exception != null)
    {
        return;
    }

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

    return;
}



procedure RegressionTestInput.ClassWithBoolTypes.Main();



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

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

    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
    return;
}



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



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