Increase the name mangling to avoid name clashes in the Boogie program. In IL,

members of a type can have the same name.

2 files changed, 354 insertions, 354 deletions

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index d33b6a17..a0f72ae1 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -480,23 +480,23 @@ var $Receiver: [Ref][Ref]Ref;
 

 var {:thread_local} $Exception: Ref;

 

-const unique RegressionTestInput.RealNumbers: Type;

+const unique RegressionTestInput.RealNumbers$type: Type;

 

-const {:extern} unique System.Object: Type;

+const {:extern} unique System.Object$type: Type;

 

-axiom $Subtype(RegressionTestInput.RealNumbers, System.Object);

+axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.RealNumbers, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);

 

-procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real)

+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real)

 {

   var d: Real;

   var $localExc: Ref;

@@ -504,7 +504,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

     d := d$in;

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

-    call System.Console.WriteLine$System.Double(d);

+    call System.Console.WriteLine$System.Double43(d);

     if ($Exception != null)

     {

         return;

@@ -516,11 +516,11 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref)

+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref)

 {

   var o: Ref;

   var $localExc: Ref;

@@ -528,7 +528,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

     o := o$in;

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real(Read($Heap, o, $BoxField)));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, Box2Real(Read($Heap, o, $BoxField)));

     if ($Exception != null)

     {

         return;

@@ -540,7 +540,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

 

 

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

+procedure RegressionTestInput.RealNumbers.RealOperations5($this: Ref);

 

 

 

@@ -548,7 +548,7 @@ const unique $real_literal_3_0: Real;
 

 const unique $real_literal_4_0: Real;

 

-implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)

+implementation RegressionTestInput.RealNumbers.RealOperations5($this: Ref)

 {

   var d: Real;

   var d2: Real;

@@ -560,28 +560,28 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;

     d2 := $real_literal_4_0;

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealPlus(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealMinus(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealTimes(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealDivide(d, d2));

     if ($Exception != null)

     {

         return;

@@ -593,20 +593,20 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
 

 

 

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

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

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)

+implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -627,45 +627,45 @@ implementation RegressionTestInput.RealNumbers.#cctor()
 

 

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;

 

-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object);

+axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field: Field;

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field: Field;

 

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref);

+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref);

 

 

 

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref)

+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

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

-    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));

+    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field))));

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

     return;

 }

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref)

+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));

-    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));

-    call System.Object.#ctor($this);

+    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field, Int2Box(0));

+    $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(0));

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -686,37 +686,37 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
 

 

 

-const unique RegressionTestInput.CreateStruct: Type;

+const unique RegressionTestInput.CreateStruct$type: Type;

 

-axiom $Subtype(RegressionTestInput.CreateStruct, System.Object);

+axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.CreateStruct, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);

 

-procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

+procedure RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref);

 

 

 

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

+procedure RegressionTestInput.S298.#default_ctor(this: Ref);

 

 

 

-const unique RegressionTestInput.S: Type;

+const unique RegressionTestInput.S$type: Type;

 

-const {:extern} unique System.ValueType: Type;

+const {:extern} unique System.ValueType$type: Type;

 

-axiom $Subtype(System.ValueType, System.Object);

+axiom $Subtype(System.ValueType$type, System.Object$type);

 

-axiom $DisjointSubtree(System.ValueType, System.Object);

+axiom $DisjointSubtree(System.ValueType$type, System.Object$type);

 

-axiom $Subtype(RegressionTestInput.S, System.ValueType);

+axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);

 

-axiom $DisjointSubtree(RegressionTestInput.S, System.ValueType);

+axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);

 

-const unique RegressionTestInput.S.x: Field;

+const unique RegressionTestInput.S.x$field: Field;

 

-const unique RegressionTestInput.S.b: Field;

+const unique RegressionTestInput.S.b$field: Field;

 

-implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

+implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref)

 {

   var $tmp0: Ref;

   var s: Ref;

@@ -725,13 +725,13 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

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

     call $tmp0 := Alloc();

-    call RegressionTestInput.S.#default_ctor($tmp0);

-    assume $DynamicType($tmp0) == RegressionTestInput.S;

+    call RegressionTestInput.S298.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == RegressionTestInput.S$type;

     s := $tmp0;

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

-    assert Box2Int(Read($Heap, s, RegressionTestInput.S.x)) == 0;

+    assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 0;

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

-    assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b));

+    assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b$field));

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

     $result := s;

     return;

@@ -739,11 +739,11 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref)

 {

   var s: Ref;

   var $localExc: Ref;

@@ -751,9 +751,9 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

     s := s$in;

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

-    $Heap := Write($Heap, s, RegressionTestInput.S.x, Int2Box(3));

+    $Heap := Write($Heap, s, RegressionTestInput.S.x$field, Int2Box(3));

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

-    assert Box2Int(Read($Heap, s, RegressionTestInput.S.x)) == 3;

+    assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 3;

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

     $result := s;

     return;

@@ -761,16 +761,16 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)

+implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -791,21 +791,21 @@ implementation RegressionTestInput.CreateStruct.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithArrayTypes: Type;

+const unique RegressionTestInput.ClassWithArrayTypes$type: Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes, System.Object);

+axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

 

-var RegressionTestInput.ClassWithArrayTypes.s: Ref;

+var RegressionTestInput.ClassWithArrayTypes.s$field: Ref;

 

-const unique RegressionTestInput.ClassWithArrayTypes.a: Field;

+const unique RegressionTestInput.ClassWithArrayTypes.a$field: Field;

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main1();

+procedure RegressionTestInput.ClassWithArrayTypes.Main112();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main1()

+implementation RegressionTestInput.ClassWithArrayTypes.Main112()

 {

   var s: Ref;

   var $tmp1: Ref;

@@ -838,11 +838,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main2();

+procedure RegressionTestInput.ClassWithArrayTypes.Main213();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main2()

+implementation RegressionTestInput.ClassWithArrayTypes.Main213()

 {

   var $tmp3: Ref;

   var t: Ref;

@@ -853,11 +853,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;

     call $tmp3 := Alloc();

     assume $ArrayLength($tmp3) == 1 * 5;

-    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    RegressionTestInput.ClassWithArrayTypes.s$field := $tmp3;

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

-    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0 := Int2Box(2)]];

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

-    assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

+    assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;

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

     call $tmp4 := Alloc();

     assume $ArrayLength($tmp4) == 1 * 4;

@@ -867,18 +867,18 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

     assert Box2Int($ArrayContents[t][0]) == 1;

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

-    assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

+    assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;

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

     return;

 }

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int)

 {

   var x: int;

   var _loc0: Ref;

@@ -888,12 +888,12 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
 

     x := x$in;

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

-    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]];

+    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x := Int2Box(42)]];

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

-    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];

+    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x + 1 := Int2Box(43)]];

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

-    _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a));

-    _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a));

+    _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));

+    _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));

     assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;

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

     return;

@@ -901,11 +901,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref)

 {

   var xs: Ref;

   var $localExc: Ref;

@@ -922,7 +922,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($
     if (!(if xs != null then $ArrayLength(xs) <= 0 else true))

     {

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

-        $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];

+        $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];

     }

     else

     {

@@ -934,17 +934,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)

+implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));

-    call System.Object.#ctor($this);

+    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field, Ref2Box(null));

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -961,22 +961,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
 

 implementation RegressionTestInput.ClassWithArrayTypes.#cctor()

 {

-    RegressionTestInput.ClassWithArrayTypes.s := null;

+    RegressionTestInput.ClassWithArrayTypes.s$field := null;

 }

 

 

 

-const unique RegressionTestInput.BitwiseOperations: Type;

+const unique RegressionTestInput.BitwiseOperations$type: Type;

 

-axiom $Subtype(RegressionTestInput.BitwiseOperations, System.Object);

+axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);

 

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

+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -992,11 +992,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 

 

 

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

+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -1012,11 +1012,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 

 

 

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

+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -1032,11 +1032,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1050,16 +1050,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)

+implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1080,36 +1080,36 @@ implementation RegressionTestInput.BitwiseOperations.#cctor()
 

 

 

-const unique RegressionTestInput.AsyncAttribute: Type;

+const unique RegressionTestInput.AsyncAttribute$type: Type;

 

-const {:extern} unique System.Attribute: Type;

+const {:extern} unique System.Attribute$type: Type;

 

-axiom $Subtype(System.Attribute, System.Object);

+axiom $Subtype(System.Attribute$type, System.Object$type);

 

-axiom $DisjointSubtree(System.Attribute, System.Object);

+axiom $DisjointSubtree(System.Attribute$type, System.Object$type);

 

-const {:extern} unique System.Runtime.InteropServices._Attribute: Type;

+const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;

 

-axiom $Subtype(System.Attribute, System.Runtime.InteropServices._Attribute);

+axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);

 

-axiom $Subtype(RegressionTestInput.AsyncAttribute, System.Attribute);

+axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

 

-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute, System.Attribute);

+axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

 

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

+procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)

+implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Attribute.#ctor($this);

+    call System.Attribute.#ctor45($this);

     if ($Exception != null)

     {

         return;

@@ -1130,17 +1130,17 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 

 

 

-const unique RegressionTestInput.RefParameters: Type;

+const unique RegressionTestInput.RefParameters$type: Type;

 

-axiom $Subtype(RegressionTestInput.RefParameters, System.Object);

+axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.RefParameters, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);

 

-procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);

 

 

 

-implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)

+implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)

 {

   var $localExc: Ref;

   var $label: int;

@@ -1154,16 +1154,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RefParameters.#ctor($this: Ref)

+implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1184,22 +1184,22 @@ implementation RegressionTestInput.RefParameters.#cctor()
 

 

 

-const unique RegressionTestInput.NestedGeneric: Type;

+const unique RegressionTestInput.NestedGeneric$type: Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric, System.Object);

+axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);

 

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

+procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);

 

 

 

-implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)

+implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1210,22 +1210,22 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
 

 

 

-const unique RegressionTestInput.NestedGeneric.C: Type;

+const unique RegressionTestInput.NestedGeneric.C$type: Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric.C, System.Object);

+axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

 

-procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

+procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);

 

 

 

-implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)

+implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1236,21 +1236,21 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
 

 

 

-function RegressionTestInput.NestedGeneric.C.G(arg0: Type) : Type;

+function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;

 

 function Child0(in: Type) : Type;

 

-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G(arg0)) == arg0);

+axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);

 

-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)

+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)

 {

   var x: int;

   var CS$0$0000: Box;

@@ -1265,7 +1265,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 

     x := x$in;

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

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1282,7 +1282,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

     else

     {

-        call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        call $tmp7 := System.Activator.CreateInstance``12(Child0($DynamicType($this)));

         $tmp6 := Box2Box($tmp7);

         if ($Exception != null)

         {

@@ -1329,7 +1329,7 @@ implementation RegressionTestInput.NestedGeneric.#cctor()
 

 

 

-implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

+implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref)

 {

 }

 

@@ -1343,25 +1343,25 @@ procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref);
 

 implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref)

 {

-    $Heap := Write($Heap, other, RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x))));

-    $Heap := Write($Heap, other, RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b))));

+    $Heap := Write($Heap, other, RegressionTestInput.S.x$field, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x$field))));

+    $Heap := Write($Heap, other, RegressionTestInput.S.b$field, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b$field))));

 }

 

 

 

-const unique RegressionTestInput.Class0: Type;

+const unique RegressionTestInput.Class0$type: Type;

 

-axiom $Subtype(RegressionTestInput.Class0, System.Object);

+axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.Class0, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);

 

-var RegressionTestInput.Class0.StaticInt: int;

+var RegressionTestInput.Class0.StaticInt$field: int;

 

-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

+implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1375,11 +1375,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)

 {

   var x: int;

   var __temp_1: int;

@@ -1401,20 +1401,20 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 

     assert (if x == 3 then y <= 8 else false);

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

-    RegressionTestInput.Class0.StaticInt := y;

+    RegressionTestInput.Class0.StaticInt$field := y;

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

-    assert y == RegressionTestInput.Class0.StaticInt;

+    assert y == RegressionTestInput.Class0.StaticInt$field;

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

     return;

 }

 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)

 {

   var x: int;

   var y: int;

@@ -1429,11 +1429,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)

 {

   var b: bool;

   var $localExc: Ref;

@@ -1446,11 +1446,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref)

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)

 {

   var c: Ref;

   var $localExc: Ref;

@@ -1463,41 +1463,41 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int)

+implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)

 {

   var $tmp8: int;

   var $localExc: Ref;

   var $label: int;

 

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

-    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);

     if ($Exception != null)

     {

         return;

     }

 

-    $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp8;

+    $result := 3 + RegressionTestInput.Class0.StaticInt$field + $tmp8;

     return;

 }

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)

 {

   var $localExc: Ref;

   var $label: int;

 

     x$out := x$in;

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

-    x$out := 3 + RegressionTestInput.Class0.StaticInt;

+    x$out := 3 + RegressionTestInput.Class0.StaticInt$field;

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

     $result := x$out;

     return;

@@ -1505,11 +1505,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)

 {

   var $localExc: Ref;

   var $label: int;

@@ -1518,7 +1518,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;

     x$out := x$out + 1;

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

-    RegressionTestInput.Class0.StaticInt := x$out;

+    RegressionTestInput.Class0.StaticInt$field := x$out;

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

     $result := x$out;

     return;

@@ -1526,11 +1526,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1540,7 +1540,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;

     x := x + 1;

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

-    RegressionTestInput.Class0.StaticInt := x;

+    RegressionTestInput.Class0.StaticInt$field := x;

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

     $result := x;

     return;

@@ -1548,11 +1548,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int)

+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1566,11 +1566,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)

 {

   var y: int;

   var $tmp9: int;

@@ -1579,7 +1579,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

     y := y$in;

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

-    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

+    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);

     if ($Exception != null)

     {

         return;

@@ -1591,16 +1591,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.#ctor($this: Ref)

+implementation RegressionTestInput.Class0.#ctor39($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1617,26 +1617,26 @@ procedure RegressionTestInput.Class0.#cctor();
 

 implementation RegressionTestInput.Class0.#cctor()

 {

-    RegressionTestInput.Class0.StaticInt := 0;

+    RegressionTestInput.Class0.StaticInt$field := 0;

 }

 

 

 

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

+const unique RegressionTestInput.ClassWithBoolTypes$type: Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes, System.Object);

+axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

 

-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

+var RegressionTestInput.ClassWithBoolTypes.staticB$field: bool;

 

-const unique RegressionTestInput.ClassWithBoolTypes.b: Field;

+const unique RegressionTestInput.ClassWithBoolTypes.b$field: Field;

 

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)

 {

   var x: int;

   var y: int;

@@ -1652,32 +1652,32 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)

 {

   var z: bool;

   var $localExc: Ref;

   var $label: int;

 

     z := z$in;

-    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));

+    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(false));

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

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

     }

 

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

-    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));

+    $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(z));

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

     if (z)

     {

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

-        RegressionTestInput.ClassWithBoolTypes.staticB := z;

+        RegressionTestInput.ClassWithBoolTypes.staticB$field := z;

     }

     else

     {

@@ -1688,18 +1688,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes.Main();

+procedure RegressionTestInput.ClassWithBoolTypes.Main42();

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.Main()

+implementation RegressionTestInput.ClassWithBoolTypes.Main42()

 {

   var $tmp10: bool;

   var $localExc: Ref;

   var $label: int;

 

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

-    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

+    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);

     if ($Exception != null)

     {

         return;

@@ -1717,7 +1717,7 @@ procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
 

 implementation RegressionTestInput.ClassWithBoolTypes.#cctor()

 {

-    RegressionTestInput.ClassWithBoolTypes.staticB := false;

+    RegressionTestInput.ClassWithBoolTypes.staticB$field := false;

 }

 

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 2f6b0041..d2b5950a 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -466,23 +466,23 @@ var $Receiver: [Ref][Ref]Ref;
 

 var {:thread_local} $Exception: Ref;

 

-const unique RegressionTestInput.RealNumbers: Type;

+const unique RegressionTestInput.RealNumbers$type: Type;

 

-const {:extern} unique System.Object: Type;

+const {:extern} unique System.Object$type: Type;

 

-axiom $Subtype(RegressionTestInput.RealNumbers, System.Object);

+axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.RealNumbers, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type);

 

-procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real);

+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real)

+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real)

 {

   var d: Real;

   var $localExc: Ref;

@@ -490,7 +490,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

     d := d$in;

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

-    call System.Console.WriteLine$System.Double(d);

+    call System.Console.WriteLine$System.Double43(d);

     if ($Exception != null)

     {

         return;

@@ -502,11 +502,11 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref)

+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref)

 {

   var o: Ref;

   var $localExc: Ref;

@@ -514,7 +514,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

     o := o$in;

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real($BoxField[o]));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, Box2Real($BoxField[o]));

     if ($Exception != null)

     {

         return;

@@ -526,7 +526,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
 

 

 

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

+procedure RegressionTestInput.RealNumbers.RealOperations5($this: Ref);

 

 

 

@@ -534,7 +534,7 @@ const unique $real_literal_3_0: Real;
 

 const unique $real_literal_4_0: Real;

 

-implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)

+implementation RegressionTestInput.RealNumbers.RealOperations5($this: Ref)

 {

   var d: Real;

   var d2: Real;

@@ -546,28 +546,28 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;

     d2 := $real_literal_4_0;

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealPlus(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealMinus(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealTimes(d, d2));

     if ($Exception != null)

     {

         return;

     }

 

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

-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2));

+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealDivide(d, d2));

     if ($Exception != null)

     {

         return;

@@ -579,20 +579,20 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
 

 

 

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

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

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)

+implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -613,21 +613,21 @@ implementation RegressionTestInput.RealNumbers.#cctor()
 

 

 

-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;

+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type;

 

-axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object);

+axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);

 

 var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;

 

 var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int;

 

-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref);

+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref);

 

 

 

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref)

+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

@@ -640,18 +640,18 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref)

+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

     RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;

     RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0;

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -672,37 +672,37 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
 

 

 

-const unique RegressionTestInput.CreateStruct: Type;

+const unique RegressionTestInput.CreateStruct$type: Type;

 

-axiom $Subtype(RegressionTestInput.CreateStruct, System.Object);

+axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.CreateStruct, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type);

 

-procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref);

+procedure RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref);

 

 

 

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

+procedure RegressionTestInput.S298.#default_ctor(this: Ref);

 

 

 

-const unique RegressionTestInput.S: Type;

+const unique RegressionTestInput.S$type: Type;

 

-const {:extern} unique System.ValueType: Type;

+const {:extern} unique System.ValueType$type: Type;

 

-axiom $Subtype(System.ValueType, System.Object);

+axiom $Subtype(System.ValueType$type, System.Object$type);

 

-axiom $DisjointSubtree(System.ValueType, System.Object);

+axiom $DisjointSubtree(System.ValueType$type, System.Object$type);

 

-axiom $Subtype(RegressionTestInput.S, System.ValueType);

+axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type);

 

-axiom $DisjointSubtree(RegressionTestInput.S, System.ValueType);

+axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);

 

 var RegressionTestInput.S.x: [Ref]int;

 

 var RegressionTestInput.S.b: [Ref]bool;

 

-implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

+implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref)

 {

   var $tmp0: Ref;

   var s: Ref;

@@ -711,8 +711,8 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

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

     call $tmp0 := Alloc();

-    call RegressionTestInput.S.#default_ctor($tmp0);

-    assume $DynamicType($tmp0) == RegressionTestInput.S;

+    call RegressionTestInput.S298.#default_ctor($tmp0);

+    assume $DynamicType($tmp0) == RegressionTestInput.S$type;

     s := $tmp0;

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

     assert RegressionTestInput.S.x[s] == 0;

@@ -725,11 +725,11 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref)

 {

   var s: Ref;

   var $localExc: Ref;

@@ -747,16 +747,16 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)

+implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -777,21 +777,21 @@ implementation RegressionTestInput.CreateStruct.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithArrayTypes: Type;

+const unique RegressionTestInput.ClassWithArrayTypes$type: Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithArrayTypes, System.Object);

+axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);

 

 var RegressionTestInput.ClassWithArrayTypes.s: Ref;

 

 var RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref;

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main1();

+procedure RegressionTestInput.ClassWithArrayTypes.Main112();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main1()

+implementation RegressionTestInput.ClassWithArrayTypes.Main112()

 {

   var s: Ref;

   var $tmp1: Ref;

@@ -824,11 +824,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
 

 

 

-procedure RegressionTestInput.ClassWithArrayTypes.Main2();

+procedure RegressionTestInput.ClassWithArrayTypes.Main213();

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main2()

+implementation RegressionTestInput.ClassWithArrayTypes.Main213()

 {

   var $tmp3: Ref;

   var t: Ref;

@@ -860,11 +860,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int)

 {

   var x: int;

   var _loc0: Ref;

@@ -887,11 +887,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref)

+implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref)

 {

   var xs: Ref;

   var $localExc: Ref;

@@ -920,17 +920,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)

+implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

     RegressionTestInput.ClassWithArrayTypes.a[$this] := null;

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -952,17 +952,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
 

 

 

-const unique RegressionTestInput.BitwiseOperations: Type;

+const unique RegressionTestInput.BitwiseOperations$type: Type;

 

-axiom $Subtype(RegressionTestInput.BitwiseOperations, System.Object);

+axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);

 

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

+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -978,11 +978,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 

 

 

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

+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -998,11 +998,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 

 

 

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

+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int)

+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)

 {

   var x: int;

   var y: int;

@@ -1018,11 +1018,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1036,16 +1036,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)

+implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1066,36 +1066,36 @@ implementation RegressionTestInput.BitwiseOperations.#cctor()
 

 

 

-const unique RegressionTestInput.AsyncAttribute: Type;

+const unique RegressionTestInput.AsyncAttribute$type: Type;

 

-const {:extern} unique System.Attribute: Type;

+const {:extern} unique System.Attribute$type: Type;

 

-axiom $Subtype(System.Attribute, System.Object);

+axiom $Subtype(System.Attribute$type, System.Object$type);

 

-axiom $DisjointSubtree(System.Attribute, System.Object);

+axiom $DisjointSubtree(System.Attribute$type, System.Object$type);

 

-const {:extern} unique System.Runtime.InteropServices._Attribute: Type;

+const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type;

 

-axiom $Subtype(System.Attribute, System.Runtime.InteropServices._Attribute);

+axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type);

 

-axiom $Subtype(RegressionTestInput.AsyncAttribute, System.Attribute);

+axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

 

-axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute, System.Attribute);

+axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);

 

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

+procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)

+implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Attribute.#ctor($this);

+    call System.Attribute.#ctor45($this);

     if ($Exception != null)

     {

         return;

@@ -1116,17 +1116,17 @@ implementation RegressionTestInput.AsyncAttribute.#cctor()
 

 

 

-const unique RegressionTestInput.RefParameters: Type;

+const unique RegressionTestInput.RefParameters$type: Type;

 

-axiom $Subtype(RegressionTestInput.RefParameters, System.Object);

+axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.RefParameters, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);

 

-procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int);

+procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);

 

 

 

-implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int)

+implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)

 {

   var $localExc: Ref;

   var $label: int;

@@ -1140,16 +1140,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.RefParameters.#ctor($this: Ref)

+implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1170,22 +1170,22 @@ implementation RegressionTestInput.RefParameters.#cctor()
 

 

 

-const unique RegressionTestInput.NestedGeneric: Type;

+const unique RegressionTestInput.NestedGeneric$type: Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric, System.Object);

+axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);

 

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

+procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);

 

 

 

-implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)

+implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1196,22 +1196,22 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
 

 

 

-const unique RegressionTestInput.NestedGeneric.C: Type;

+const unique RegressionTestInput.NestedGeneric.C$type: Type;

 

-axiom $Subtype(RegressionTestInput.NestedGeneric.C, System.Object);

+axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);

 

-procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref);

+procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);

 

 

 

-implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)

+implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1222,21 +1222,21 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
 

 

 

-function RegressionTestInput.NestedGeneric.C.G(arg0: Type) : Type;

+function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;

 

 function Child0(in: Type) : Type;

 

-axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G(arg0)) == arg0);

+axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);

 

-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int);

+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);

 

 

 

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

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

 

 

 

-implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)

+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)

 {

   var x: int;

   var CS$0$0000: Box;

@@ -1251,7 +1251,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 

     x := x$in;

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

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1268,7 +1268,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
     }

     else

     {

-        call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        call $tmp7 := System.Activator.CreateInstance``12(Child0($DynamicType($this)));

         $tmp6 := Box2Box($tmp7);

         if ($Exception != null)

         {

@@ -1315,7 +1315,7 @@ implementation RegressionTestInput.NestedGeneric.#cctor()
 

 

 

-implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

+implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref)

 {

 }

 

@@ -1335,19 +1335,19 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re
 

 

 

-const unique RegressionTestInput.Class0: Type;

+const unique RegressionTestInput.Class0$type: Type;

 

-axiom $Subtype(RegressionTestInput.Class0, System.Object);

+axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.Class0, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);

 

 var RegressionTestInput.Class0.StaticInt: int;

 

-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

+implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1361,11 +1361,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)

 {

   var x: int;

   var __temp_1: int;

@@ -1396,11 +1396,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)

 {

   var x: int;

   var y: int;

@@ -1415,11 +1415,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)

 {

   var b: bool;

   var $localExc: Ref;

@@ -1432,11 +1432,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref)

+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)

 {

   var c: Ref;

   var $localExc: Ref;

@@ -1449,18 +1449,18 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int)

+implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)

 {

   var $tmp8: int;

   var $localExc: Ref;

   var $label: int;

 

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

-    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);

     if ($Exception != null)

     {

         return;

@@ -1472,11 +1472,11 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int)

+implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)

 {

   var $localExc: Ref;

   var $label: int;

@@ -1491,11 +1491,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)

 {

   var $localExc: Ref;

   var $label: int;

@@ -1512,11 +1512,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1534,11 +1534,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int)

+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)

 {

   var x: int;

   var $localExc: Ref;

@@ -1552,11 +1552,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)

 {

   var y: int;

   var $tmp9: int;

@@ -1565,7 +1565,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

     y := y$in;

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

-    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

+    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);

     if ($Exception != null)

     {

         return;

@@ -1577,16 +1577,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
 

 

 

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

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

 

 

 

-implementation RegressionTestInput.Class0.#ctor($this: Ref)

+implementation RegressionTestInput.Class0.#ctor39($this: Ref)

 {

   var $localExc: Ref;

   var $label: int;

 

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1608,21 +1608,21 @@ implementation RegressionTestInput.Class0.#cctor()
 

 

 

-const unique RegressionTestInput.ClassWithBoolTypes: Type;

+const unique RegressionTestInput.ClassWithBoolTypes$type: Type;

 

-axiom $Subtype(RegressionTestInput.ClassWithBoolTypes, System.Object);

+axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

 

-axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes, System.Object);

+axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);

 

 var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

 

 var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;

 

-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)

 {

   var x: int;

   var y: int;

@@ -1638,11 +1638,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 

 

 

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

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

 

 

 

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

+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)

 {

   var z: bool;

   var $localExc: Ref;

@@ -1651,7 +1651,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
     z := z$in;

     RegressionTestInput.ClassWithBoolTypes.b[$this] := false;

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

-    call System.Object.#ctor($this);

+    call System.Object.#ctor44($this);

     if ($Exception != null)

     {

         return;

@@ -1674,18 +1674,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 

 

 

-procedure RegressionTestInput.ClassWithBoolTypes.Main();

+procedure RegressionTestInput.ClassWithBoolTypes.Main42();

 

 

 

-implementation RegressionTestInput.ClassWithBoolTypes.Main()

+implementation RegressionTestInput.ClassWithBoolTypes.Main42()

 {

   var $tmp10: bool;

   var $localExc: Ref;

   var $label: int;

 

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

-    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

+    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);

     if ($Exception != null)

     {

         return;