1 files changed, 53 insertions, 9 deletions
diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
index 918bf1f7..35328269 100644
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
@@ -204,12 +204,53 @@ var $Method: [int][int]int;
 
 var $Receiver: [int][int]int;
 
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
+
+const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
+{
+    assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));
+    assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
+    return;
+}
+
+
+
+procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
+
+
+
+procedure System.Object.#ctor(this: int);
+
+
+
+implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
+{
+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);
+    $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);
+    call System.Object.#ctor(this);
+    return;
+}
+
+
+
 procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
 
 
 
+procedure System.Attribute.#ctor(this: int);
+
+
+
 implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
 {
+    call System.Attribute.#ctor(this);
     return;
 }
 
@@ -249,7 +290,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this:
   var z: bool;
 
     z := z$in;
+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.staticB] := Bool2Box(false);
+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);
     assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
+    call System.Object.#ctor(this);
     assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
     $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);
     assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
@@ -382,7 +426,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t
   var xs: int;
 
     xs := xs$in;
-    if (!(!(xs != 0) || $ArrayLength[xs] <= 0))
+    if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true))
     {
         assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;
         $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][0 := $ArrayContents[xs][0]]];
@@ -403,6 +447,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
 
 implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
 {
+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.s] := Int2Box(0);
+    $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0);
+    call System.Object.#ctor(this);
     return;
 }
 
@@ -438,21 +485,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
   var x: int;
   var __temp_1: int;
   var $tmp5: int;
-  var __temp_2: int;
-  var __temp_3: int;
   var local_0: int;
 
     x := x$in;
     $tmp5 := x;
     assert $tmp5 != 0;
     __temp_1 := 5 / $tmp5;
-    __temp_2 := 3;
-    assert {:sourceFile "Class1.cs"} {:sourceLine 21} true;
-    __temp_3 := __temp_2;
-    x := __temp_3;
-    local_0 := __temp_1 + __temp_2;
+    x := 3;
+    local_0 := __temp_1 + 3;
     assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
-    assert x == 3 && local_0 <= 8;
+    assert (if x == 3 then local_0 <= 8 else false);
     assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
     RegressionTestInput.Class0.StaticInt := local_0;
     assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
@@ -639,6 +681,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int);
 
 implementation RegressionTestInput.Class0.#ctor(this: int)
 {
+    $Heap[this, RegressionTestInput.Class0.StaticInt] := Int2Box(0);
+    call System.Object.#ctor(this);
     return;
 }