8 files changed, 0 insertions, 4314 deletions
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
deleted file mode 100644
index 51a4ba86..00000000
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ /dev/null
@@ -1,212 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-
-namespace RegressionTestInput {
-
-  [AttributeUsage(AttributeTargets.Method)]
-  public class AsyncAttribute : Attribute { }
-
-  public class Class0 {
-
-    static int StaticInt;
-
-    static int StaticMethod(int x) {
-      return x + 1;
-    }
-
-    void M(int x) {
-      int y = (5 / x) + (x = 3);
-      Contract.Assert(x == 3 && y <= 8);
-      StaticInt = y;
-      Contract.Assert(y == StaticInt);
-    }
-
-    // Test to make sure we generate unique procedure names
-    void M(int x, int y) { }
-    void M(bool b) { }
-    void M(Class0 c) { }
-
-    int NonVoid() {
-      return 3 + StaticInt + StaticMethod(3);
-    }
-
-    int OutParam(out int x) {
-      x = 3 + StaticInt;
-      return x;
-    }
-
-    int RefParam(ref int x) {
-      x = x + 1;
-      StaticInt = x;
-      return x;
-    }
-
-    int AssignToInParam(int x) {
-      x = x + 1;
-      StaticInt = x;
-      return x;
-    }
-
-    [AsyncAttribute]
-    int MethodThatRepresentsAnAynchronousMethod(int x) {
-      return x;
-    }
-
-    int CallAsyncMethod(int y) {
-      return MethodThatRepresentsAnAynchronousMethod(y);
-    }
-
-
-  }
-  class ClassWithBoolTypes {
-    static bool staticB;
-    bool b;
-
-    static bool M(int x, int y) {
-      return x < y;
-    }
-
-    public ClassWithBoolTypes(bool z) {
-      this.b = z;
-      if (z) ClassWithBoolTypes.staticB = z;
-    }
-
-    public static void Main() {
-      ClassWithBoolTypes.M(3, 4);
-    }
-  }
-
-  class ClassWithArrayTypes
-  {
-    public static void Main1()
-    {
-      int[] s = new int[5];
-      s[0] = 2;
-      Contract.Assert(s[0] == 2);
-
-      int[] t = new int[4];
-      t[0] = 1;
-      Contract.Assert(t[0] == 1);
-
-      Contract.Assert(s[0] == 2);
-    }
-
-    public static int[] s;
-    public static void Main2()
-    {
-      s = new int[5];
-      s[0] = 2;
-      Contract.Assert(s[0] == 2);
-
-      int[] t = new int[4];
-      t[0] = 1;
-      Contract.Assert(t[0] == 1);
-
-      Contract.Assert(s[0] == 2);
-    }
-
-    public int[] a;
-    public void Main3(int x)
-    {
-      a[x] = 42;
-      a[x + 1] = 43;
-      Contract.Assert(a[x + 1] == a[x] + 1);
-    }
-
-    public void Main4(int[] xs) {
-      if (xs != null && xs.Length > 0) {
-        a[0] = xs[0];
-      }
-    }
-  }
-
-  public class WriteToTheHeapAValueReadFromTheHeap {
-    int x;
-    int y;
-    public void M() {
-      this.y = this.x;
-    }
-  }
-
-  public struct S {
-    public int x;
-    public bool b;
-  }
-
-  public class CreateStruct {
-    public S Create() {
-      var s = new S();
-      Contract.Assert(s.x == 0);
-      Contract.Assert(s.b == false);
-      return s;
-    }
-    S AssignThreeToSDotX(S s) {
-      s.x = 3;
-      Contract.Assert(s.x == 3);
-      return s;
-    }
-
-  }
-
-  public class RefParameters {
-    public static void M(ref int x) {
-      x++;
-    }
-  }
-
-  public class RealNumbers {
-    public void WriteDouble(double d) {
-      Console.WriteLine(d);
-    }
-    public void ObjectToDouble(object o) {
-      WriteDouble((double)o);
-    }
-    public void RealOperations() {
-      double d = 3.0;
-      double d2 = 4.0;
-      WriteDouble(d + d2);
-      WriteDouble(d - d2);
-      WriteDouble(d * d2);
-      WriteDouble(d / d2);
-    }
-  }
-
-  public class BitwiseOperations {
-    public int BitwiseAnd(int x, int y) { return x & y; }
-    public int BitwiseOr(int x, int y) { return x | y; }
-    public int ExclusiveOr(int x, int y) { return x ^ y; }
-    public int BitwiseNegation(int x) { return ~x; }
-  }
-
-  public class NestedGeneric {
-    public class C {
-      public class G<T> where T : new() {
-        public G(int x) {
-          var y = new T(); // test to make sure index is calculated correctly for type function
-        }
-      }
-    }
-  }
-  public class TestForClassesDifferingOnlyInBeingGeneric {
-    public int x;
-  }
-
-  public class TestForClassesDifferingOnlyInBeingGeneric<T> {
-    public int x;
-  }
-
-  public struct StructContainingStruct {
-    public double d;
-    public S s;
-
-    public StructContainingStruct ReturnCopy(StructContainingStruct s) {
-      StructContainingStruct t = s;
-      return t;
-    }
-
-  }
-
-}
diff --git a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs b/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs
deleted file mode 100644
index b3cc080a..00000000
--- a/BCT/RegressionTests/RegressionTestInput/Properties/AssemblyInfo.cs
+++ /dev/null
@@ -1,36 +0,0 @@
-using System.Reflection;
-using System.Runtime.CompilerServices;
-using System.Runtime.InteropServices;
-
-// General Information about an assembly is controlled through the following 
-// set of attributes. Change these attribute values to modify the information
-// associated with an assembly.
-[assembly: AssemblyTitle("RegressionTestInput")]
-[assembly: AssemblyDescription("")]
-[assembly: AssemblyConfiguration("")]
-[assembly: AssemblyCompany("")]
-[assembly: AssemblyProduct("RegressionTestInput")]
-[assembly: AssemblyCopyright("Copyright ©  2010")]
-[assembly: AssemblyTrademark("")]
-[assembly: AssemblyCulture("")]
-
-// Setting ComVisible to false makes the types in this assembly not visible 
-// to COM components.  If you need to access a type in this assembly from 
-// COM, set the ComVisible attribute to true on that type.
-[assembly: ComVisible(false)]
-
-// The following GUID is for the ID of the typelib if this project is exposed to COM
-[assembly: Guid("dc8e9afb-ef4e-4954-8f86-1a79bb0d77e4")]
-
-// Version information for an assembly consists of the following four values:
-//
-//      Major Version
-//      Minor Version 
-//      Build Number
-//      Revision
-//
-// You can specify all the values or you can default the Build and Revision Numbers 
-// by using the '*' as shown below:
-// [assembly: AssemblyVersion("1.0.*")]
-[assembly: AssemblyVersion("1.0.0.0")]
-[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj b/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj
deleted file mode 100644
index 6cf94c40..00000000
--- a/BCT/RegressionTests/RegressionTestInput/RegressionTestInput.csproj
+++ /dev/null
@@ -1,54 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <PropertyGroup>
-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
-    <ProductVersion>8.0.30703</ProductVersion>
-    <SchemaVersion>2.0</SchemaVersion>
-    <ProjectGuid>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</ProjectGuid>
-    <OutputType>Library</OutputType>
-    <AppDesignerFolder>Properties</AppDesignerFolder>
-    <RootNamespace>RegressionTestInput</RootNamespace>
-    <AssemblyName>RegressionTestInput</AssemblyName>
-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
-    <FileAlignment>512</FileAlignment>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
-    <DebugSymbols>true</DebugSymbols>
-    <DebugType>full</DebugType>
-    <Optimize>false</Optimize>
-    <OutputPath>bin\Debug\</OutputPath>
-    <DefineConstants>DEBUG;TRACE</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
-    <DebugType>pdbonly</DebugType>
-    <Optimize>true</Optimize>
-    <OutputPath>bin\Release\</OutputPath>
-    <DefineConstants>TRACE</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-  </PropertyGroup>
-  <ItemGroup>
-    <Reference Include="System" />
-    <Reference Include="System.Core" />
-    <Reference Include="System.Xml.Linq" />
-    <Reference Include="System.Data.DataSetExtensions" />
-    <Reference Include="Microsoft.CSharp" />
-    <Reference Include="System.Data" />
-    <Reference Include="System.Xml" />
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="Class1.cs" />
-    <Compile Include="Properties\AssemblyInfo.cs" />
-  </ItemGroup>
-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
-       Other similar extension points exist, see Microsoft.Common.targets.
-  <Target Name="BeforeBuild">
-  </Target>
-  <Target Name="AfterBuild">
-  </Target>
-  -->
-</Project>
-\ No newline at end of file
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
deleted file mode 100644
index 0a2a515a..00000000
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ /dev/null
@@ -1,1893 +0,0 @@
-// 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);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
-{
-  var xs: Ref;
-  var $localExc: Ref;
-  var $label: int;
-
-    xs := xs$in;
-    assume {:breadcrumb 13} true;
-    if (xs != null)
-    {
-    }
-    else
-    {
-    }
-
-    if ((if xs != null then $ArrayLength(xs) > 0 else false))
-    {
-        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        assume $this != null;
-        assume xs != null;
-        $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
-    }
-    else
-    {
-    }
-}
-
-
-
-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;
-}
-
-
diff --git a/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs b/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs
deleted file mode 100644
index a0fd3275..00000000
--- a/BCT/RegressionTests/TranslationTest/Properties/AssemblyInfo.cs
+++ /dev/null
@@ -1,35 +0,0 @@
-using System.Reflection;
-using System.Runtime.CompilerServices;
-using System.Runtime.InteropServices;
-
-// General Information about an assembly is controlled through the following 
-// set of attributes. Change these attribute values to modify the information
-// associated with an assembly.
-[assembly: AssemblyTitle("TranslationTest")]
-[assembly: AssemblyDescription("")]
-[assembly: AssemblyConfiguration("")]
-[assembly: AssemblyCompany("")]
-[assembly: AssemblyProduct("TranslationTest")]
-[assembly: AssemblyCopyright("Copyright ©  2010")]
-[assembly: AssemblyTrademark("")]
-[assembly: AssemblyCulture("")]
-
-// Setting ComVisible to false makes the types in this assembly not visible 
-// to COM components.  If you need to access a type in this assembly from 
-// COM, set the ComVisible attribute to true on that type.
-[assembly: ComVisible(false)]
-
-// The following GUID is for the ID of the typelib if this project is exposed to COM
-[assembly: Guid("f448ac99-c5e7-424c-8bdb-243e8276d4d7")]
-
-// Version information for an assembly consists of the following four values:
-//
-//      Major Version
-//      Minor Version 
-//      Build Number
-//      Revision
-//
-// You can specify all the values or you can default the Build and Revision Numbers 
-// by using the '*' as shown below:
-[assembly: AssemblyVersion("1.0.0.0")]
-[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
deleted file mode 100644
index b552ee36..00000000
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ /dev/null
@@ -1,1879 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.
-// Bytecode Translator prelude
-
-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 $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);
-
-
-
-var F$RegressionTestInput.StructContainingStruct.d: [Ref]Real;
-
-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));
-
-var F$RegressionTestInput.StructContainingStruct.s: [Ref]Ref;
-
-implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_ctor($this: Ref)
-{
-  var $tmp0: Ref;
-
-    F$RegressionTestInput.StructContainingStruct.d[$this] := $DefaultReal;
-    call $tmp0 := Alloc();
-    call RegressionTestInput.S.#default_ctor($tmp0);
-    assume $DynamicType($tmp0) == T$RegressionTestInput.S();
-    F$RegressionTestInput.StructContainingStruct.s[$this] := $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();
-    F$RegressionTestInput.StructContainingStruct.d[other] := F$RegressionTestInput.StructContainingStruct.d[this];
-    call $tmp1 := RegressionTestInput.S.#copy_ctor(F$RegressionTestInput.StructContainingStruct.s[this]);
-    F$RegressionTestInput.StructContainingStruct.s[other] := $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));
-
-var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
-
-var F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int;
-
-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;
-    F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this];
-}
-
-
-
-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;
-
-    F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;
-    F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 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);
-
-
-
-var F$RegressionTestInput.S.x: [Ref]int;
-
-var F$RegressionTestInput.S.b: [Ref]bool;
-
-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 F$RegressionTestInput.S.x[s_Ref] == 0;
-    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
-    assume s_Ref != null;
-    assert !F$RegressionTestInput.S.b[s_Ref];
-    $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;
-    F$RegressionTestInput.S.x[s] := 3;
-    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
-    assume s != null;
-    assert F$RegressionTestInput.S.x[s] == 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;
-
-var F$RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref;
-
-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[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][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[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Union(43)]];
-    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
-    assume $this != null;
-    $tmp0 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
-    assume $tmp0 != null;
-    assume $this != null;
-    $tmp1 := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
-    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);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)
-{
-  var xs: Ref;
-  var $localExc: Ref;
-  var $label: int;
-
-    xs := xs$in;
-    assume {:breadcrumb 13} true;
-    if (xs != null)
-    {
-    }
-    else
-    {
-    }
-
-    if ((if xs != null then $ArrayLength(xs) > 0 else false))
-    {
-        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        assume $this != null;
-        assume xs != null;
-        $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
-    }
-    else
-    {
-    }
-}
-
-
-
-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;
-
-    F$RegressionTestInput.ClassWithArrayTypes.a[$this] := 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));
-
-var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: [Ref]int;
-
-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;
-
-    F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x[$this] := 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)
-{
-    F$RegressionTestInput.S.x[$this] := 0;
-    F$RegressionTestInput.S.b[$this] := false;
-}
-
-
-
-implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref) returns (other: Ref)
-{
-    call other := Alloc();
-    assume $DynamicType(other) == T$RegressionTestInput.S();
-    F$RegressionTestInput.S.x[other] := F$RegressionTestInput.S.x[this];
-    F$RegressionTestInput.S.b[other] := F$RegressionTestInput.S.b[this];
-}
-
-
-
-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));
-
-var F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
-
-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;
-
-    F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 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;
-
-var F$RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;
-
-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;
-    F$RegressionTestInput.ClassWithBoolTypes.b[$this] := 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;
-    F$RegressionTestInput.ClassWithBoolTypes.b[$this] := 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;
-}
-
-
diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
deleted file mode 100644
index 446c23b2..00000000
--- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
+++ /dev/null
@@ -1,98 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <PropertyGroup>
-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
-    <ProductVersion>
-    </ProductVersion>
-    <SchemaVersion>2.0</SchemaVersion>
-    <ProjectGuid>{A112AFBA-D6F6-44A4-A683-C3D458A68D84}</ProjectGuid>
-    <OutputType>Library</OutputType>
-    <AppDesignerFolder>Properties</AppDesignerFolder>
-    <RootNamespace>TranslationTest</RootNamespace>
-    <AssemblyName>TranslationTest</AssemblyName>
-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
-    <FileAlignment>512</FileAlignment>
-    <ProjectTypeGuids>{3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
-    <DebugSymbols>true</DebugSymbols>
-    <DebugType>full</DebugType>
-    <Optimize>false</Optimize>
-    <OutputPath>bin\Debug\</OutputPath>
-    <DefineConstants>DEBUG;TRACE</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
-    <DebugType>pdbonly</DebugType>
-    <Optimize>true</Optimize>
-    <OutputPath>bin\Release\</OutputPath>
-    <DefineConstants>TRACE</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-  </PropertyGroup>
-  <ItemGroup>
-    <Reference Include="Core">
-      <HintPath>..\..\Binaries\Core.dll</HintPath>
-    </Reference>
-    <Reference Include="Microsoft.VisualStudio.QualityTools.UnitTestFramework, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
-    <Reference Include="System" />
-    <Reference Include="System.Core">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
-    </Reference>
-  </ItemGroup>
-  <ItemGroup>
-    <CodeAnalysisDependentAssemblyPaths Condition=" '$(VS100COMNTOOLS)' != '' " Include="$(VS100COMNTOOLS)..\IDE\PrivateAssemblies">
-      <Visible>False</Visible>
-    </CodeAnalysisDependentAssemblyPaths>
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="Properties\AssemblyInfo.cs" />
-    <Compile Include="UnitTest0.cs" />
-  </ItemGroup>
-  <ItemGroup>
-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj">
-      <Project>{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}</Project>
-      <Name>MetadataHelper</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Metadata\Sources\PeReader\PeReader.csproj">
-      <Project>{34B9A0CE-DF18-4CBC-8F7A-90C2B74338D5}</Project>
-      <Name>PeReader</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\CodeModel\CodeModel.csproj">
-      <Project>{035FEA7F-0D36-4AE4-B694-EC45191B9AF2}</Project>
-      <Name>CodeModel</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\MutableCodeModel\MutableCodeModel.csproj">
-      <Project>{319E150C-8F33-49E7-81CA-30F02F9BA90A}</Project>
-      <Name>MutableCodeModel</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\..\..\..\CCICodePlex\Ast\Sources\NewILToCodeModel\NewILToCodeModel.csproj">
-      <Project>{A555D4CB-F16F-4049-A8CF-180B8A05C755}</Project>
-      <Name>NewILToCodeModel</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\..\BytecodeTranslator\BytecodeTranslator.csproj">
-      <Project>{9C8E4D74-0251-479D-ADAC-A9A469977301}</Project>
-      <Name>BytecodeTranslator</Name>
-    </ProjectReference>
-    <ProjectReference Include="..\RegressionTestInput\RegressionTestInput.csproj">
-      <Project>{3D13D2CC-6387-46FA-BDC2-4BEEFC460118}</Project>
-      <Name>RegressionTestInput</Name>
-    </ProjectReference>
-  </ItemGroup>
-  <ItemGroup>
-    <EmbeddedResource Include="SplitFieldsHeapInput.txt" />
-  </ItemGroup>
-  <ItemGroup>
-    <EmbeddedResource Include="GeneralHeapInput.txt" />
-  </ItemGroup>
-  <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
-       Other similar extension points exist, see Microsoft.Common.targets.
-  <Target Name="BeforeBuild">
-  </Target>
-  <Target Name="AfterBuild">
-  </Target>
-  -->
-</Project>
-\ No newline at end of file
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
deleted file mode 100644
index 62ce9155..00000000
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ /dev/null
@@ -1,107 +0,0 @@
-using System;
-using System.Text;
-using System.Collections.Generic;
-using System.Linq;
-using Microsoft.VisualStudio.TestTools.UnitTesting;
-using System.IO;
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-using BytecodeTranslator;
-
-namespace TranslationTest {
-  /// <summary>
-  /// Summary description for UnitTest0
-  /// </summary>
-  [TestClass]
-  public class UnitTest0 {
-    public UnitTest0() {
-      //
-      // TODO: Add constructor logic here
-      //
-    }
-
-    private TestContext testContextInstance;
-
-    /// <summary>
-    ///Gets or sets the test context which provides
-    ///information about and functionality for the current test run.
-    ///</summary>
-    public TestContext TestContext {
-      get {
-        return testContextInstance;
-      }
-      set {
-        testContextInstance = value;
-      }
-    }
-
-    #region Additional test attributes
-    //
-    // You can use the following additional attributes as you write your tests:
-    //
-    // Use ClassInitialize to run code before running the first test in the class
-    // [ClassInitialize()]
-    // public static void MyClassInitialize(TestContext testContext) { }
-    //
-    // Use ClassCleanup to run code after all tests in a class have run
-    // [ClassCleanup()]
-    // public static void MyClassCleanup() { }
-    //
-    // Use TestInitialize to run code before running each test 
-    // [TestInitialize()]
-    // public void MyTestInitialize() { }
-    //
-    // Use TestCleanup to run code after each test has run
-    // [TestCleanup()]
-    // public void MyTestCleanup() { }
-    //
-    #endregion
-
-    private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {
-      var options = new Options();
-      options.monotonicHeap = true;
-      options.dereference = Options.Dereference.Assume;
-      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, options, null, false);
-      var fileName = Path.ChangeExtension(assemblyName, "bpl");
-      var s = File.ReadAllText(fileName);
-      return s;
-    }
-
-    [TestMethod]
-    public void SplitFieldsHeap() {
-      string dir = TestContext.DeploymentDirectory;
-      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
-      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.SplitFieldsHeapInput.txt");
-      StreamReader reader = new StreamReader(resource);
-      string expected = reader.ReadToEnd();
-      var result = ExecuteTest(fullPath, new SplitFieldsHeap());
-      if (result != expected) {
-        string resultFile = Path.GetFullPath("SplitFieldsHeapOutput.txt");
-        File.WriteAllText(resultFile, result);
-        var msg = String.Format("Output didn't match: SplitFieldsHeapInput.txt \"{0}\"", resultFile);
-        Assert.Fail(msg);
-      }
-    }
-
-    [TestMethod]
-    public void GeneralHeap() {
-      string dir = TestContext.DeploymentDirectory;
-      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
-      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.GeneralHeapInput.txt");
-      StreamReader reader = new StreamReader(resource);
-      string expected = reader.ReadToEnd();
-      var result = ExecuteTest(fullPath, new GeneralHeap());
-      if (result != expected) {
-        string resultFile = Path.GetFullPath("GeneralHeapOutput.txt");
-        File.WriteAllText(resultFile, result);
-        var msg = String.Format("Output didn't match: GeneralHeapInput.txt \"{0}\"", resultFile);
-        Assert.Fail(msg);
-      }
-    }
-
-  }
-}
- 
-\ No newline at end of file