Merge

86 files changed, 856 insertions, 475 deletions

diff --git a/.hgignore b/.hgignore
index 20fc1f34..e6566879 100644
--- a/.hgignore
+++ b/.hgignore
@@ -7,7 +7,7 @@ syntax: regexp
 ^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$

 ^Binaries/BytecodeTranslator$

 ^BCT/Binaries/.*$

-^Chalice/tests/(examples|permission-model|refinements)/.*\.bpl

+^Chalice/tests/(examples|permission-model|refinements|general-tests|regressions)/.*\.bpl

 Test/([^/]*)/Output

 Test/([^/]*)/([^/]*)\.sx

 Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe)

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index eb4b3672..ea171b25 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -949,7 +949,7 @@ namespace BytecodeTranslator
       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       sink.AddDelegate(type.ResolvedType, methodToCall.ResolvedMethod);

-      Bpl.Constant constant = sink.FindOrAddDelegateMethodConstant(methodToCall.ResolvedMethod);

+      Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(methodToCall.ResolvedMethod);

       Bpl.Expr methodExpr = Bpl.Expr.Ident(constant);

       Bpl.Expr instanceExpr = TranslatedExpressions.Pop();

 

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 664db230..751d8baa 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -207,6 +207,9 @@ namespace BytecodeTranslator {
       Bpl.Variable v;

       string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;

       fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);

+      // Need to append something to the name to avoid name clashes with other members (of a different

+      // type) that have the same name.

+      fieldname += "$field";

       Bpl.IToken tok = field.Token();

 

       if (field.IsStatic) {

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 1f9518b5..d1c6ec84 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -238,6 +238,10 @@ namespace BytecodeTranslator {
     {

         string typename = TypeHelper.GetTypeName(type);

         typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

+        // Need to append something to the name to avoid name clashes with other members (of a different

+        // type) that have the same name.

+        typename += "$type";

+

         Bpl.IToken tok = type.Token();

         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType);

         Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null);

@@ -248,6 +252,8 @@ namespace BytecodeTranslator {
       System.Diagnostics.Debug.Assert(parameterCount > 0);

       string typename = TypeHelper.GetTypeName(type);

       typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);

+      // Need to append something to the name to avoid name clashes.

+      typename += "$type";

       Bpl.IToken tok = type.Token();

       Bpl.VariableSeq inputs = new Bpl.VariableSeq();

       for (int i = 0; i < parameterCount; i++) {

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index 9f755a30..f94f0044 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -105,8 +105,7 @@ namespace BytecodeTranslator.Phone {
           bool isStatic = UriHelper.isArgumentURILocallyCreatedStatic(expr, host, out target) ||

                          UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target);

           if (!isStatic)

-            potentialBackKeyNavigationTargets.Add(target);

-          target = "--Other non inferrable target--";

+            target = "--Other non inferrable target--";

         } catch (InvalidOperationException) { 

         }

       }

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index be363277..18d735af 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -432,9 +432,10 @@ namespace BytecodeTranslator {
           for (index = 0; index < dispatchProcOutvars.Length; index++) {

             outs.Add(Bpl.Expr.Ident(dispatchProcOutvars[index]));

           }

-          Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn);

+          Bpl.Constant c = sink.FindOrCreateDelegateMethodConstant(defn);

+          var procInfo = sink.FindOrCreateProcedure(defn);

           Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c));

-          Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs);

+          Bpl.CallCmd callCmd = new Bpl.CallCmd(token, procInfo.Decl.Name, ins, outs);

           ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd);

         }

         Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 5a4de710..b2c1177e 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -425,6 +425,10 @@ namespace BytecodeTranslator {
 

       if (!this.declaredMethods.TryGetValue(key, out procInfo)) {

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+        // The method can be generic (or have a parameter whose type is a type parameter of the method's

+        // containing class) and then there can be name clashes.

+        MethodName += key.ToString();

+

         if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo;

 

         Bpl.Formal thisVariable = null;

@@ -636,6 +640,8 @@ namespace BytecodeTranslator {
       var key = structType.InternedKey;

       if (!this.declaredStructDefaultCtors.TryGetValue(key, out procAndFormalMap)) {

         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+        // The type can be generic and then there can be name clashes. So append the key to make it unique.

+        typename += key.ToString();

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

         var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

@@ -1105,7 +1111,7 @@ namespace BytecodeTranslator {
     private Dictionary<IMethodDefinition, Bpl.Constant> delegateMethods = new Dictionary<IMethodDefinition, Bpl.Constant>();

     internal IContractAwareHost host;

 

-    public Bpl.Constant FindOrAddDelegateMethodConstant(IMethodDefinition defn)

+    public Bpl.Constant FindOrCreateDelegateMethodConstant(IMethodDefinition defn)

     {

       if (delegateMethods.ContainsKey(defn))

         return delegateMethods[defn];

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index ad264c48..a17165ee 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -127,6 +127,7 @@ namespace BytecodeTranslator {
       s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray");

       s = s.Replace('!', '$');

       s = s.Replace('*', '$');

+      s = s.Replace('+', '$');

       s = s.Replace('(', '$');

       s = s.Replace(')', '$');

       s = s.Replace(',', '$');

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;

diff --git a/Chalice/chalice.bat b/Chalice/chalice.bat
index 3d1f4b78..62fdb308 100644
--- a/Chalice/chalice.bat
+++ b/Chalice/chalice.bat
@@ -1,5 +1,5 @@
 @echo off

 

-call scala -cp "%~dp0\target\scala-2.8.1.final\classes" chalice.Chalice -nologo %*

+call scala -cp "%~dp0\target\scala-2.8.1.final\classes" chalice.Chalice /boogieOpt:nologo %*

 

 exit /B 0

diff --git a/Chalice/src/main/scala/Chalice.scala b/Chalice/src/main/scala/Chalice.scala
index 3b0bd70d..594273cb 100644
--- a/Chalice/src/main/scala/Chalice.scala
+++ b/Chalice/src/main/scala/Chalice.scala
@@ -115,8 +115,8 @@ object Chalice {
           "0: use multiplication directly (can cause performance problems)\n"+

           "1: fix Permission$denominator as constant (possibly unsound)\n"+

           "2: use a function and provide some (redundant) axioms\n"+

-          "3: use an uninterpreted function and axiomatize the properties of multiplication")/*,

-      "boogieOpt:<arg>, /bo:<arg>" -> "specify additional Boogie options"*/

+          "3: use an uninterpreted function and axiomatize the properties of multiplication"),

+      "boogieOpt:<arg>, /bo:<arg>" -> "specify additional Boogie options"

     )

     lazy val help = {

       val maxLength = math.min((nonBooleanOptions.keys++options.keys).map(s => s.length+1).max,14)

@@ -146,13 +146,20 @@ object Chalice {
          else percentageSupport = in

        } catch { case _ => CommandLineError("/percentageSupport takes integer argument", help); }

      }

-     else if (a.startsWith("-") || a.startsWith("/"))

-			boogieArgs += ("\"" + a + "\"" + " ")

-				// other arguments starting with "-" or "/" are sent to Boogie.exe

-				/* [MHS] Quote whole argument to not confuse Boogie with arguments that

-				 * contain spaces, e.g. if Chalice is invoked as

-				 *   chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice

-				 */

+     else if (a.startsWith("-boogieOpt:") || a.startsWith("/boogieOpt:"))

+            boogieArgs += ("\"/" + a.substring(11) + "\"" + " ")

+     else if (a.startsWith("-bo:") || a.startsWith("/bo:"))

+            boogieArgs += ("\"/" + a.substring(4) + "\"" + " ")

+                /* [MHS] Quote whole argument to not confuse Boogie with arguments that

+                 * contain spaces, e.g. if Chalice is invoked as

+                 *   chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice

+                 */

+     else if (a.startsWith("-z3opt:") || a.startsWith("/z3opt:"))

+            boogieArgs += ("\"/z3opt:" + a.substring(7) + "\"" + " ")

+     else if (a.startsWith("-") || a.startsWith("/")) {

+       CommandLineError("unkonwn command line parameter: "+a.substring(1), help)

+       return

+     }

      else inputs += a

     }

     

@@ -182,9 +189,10 @@ object Chalice {
     // parse programs

     val parser = new Parser();

     val parseResults = if (files.isEmpty) {

-     List(parser.parseStdin)

+      println("No input file provided. Use 'chalice /help' for a list of all available command line options. Reading from stdin...")

+      List(parser.parseStdin)

     } else for (file <- files) yield {

-     parser.parseFile(file)

+      parser.parseFile(file)

     }

 

     // report errors and merge declarations

diff --git a/Chalice/src/main/scala/SmokeTest.scala b/Chalice/src/main/scala/SmokeTest.scala
index 8a8f46eb..9f23d144 100644
--- a/Chalice/src/main/scala/SmokeTest.scala
+++ b/Chalice/src/main/scala/SmokeTest.scala
@@ -80,7 +80,7 @@ object SmokeTest {
     })

     

     verificationResult +

-    (if (realErrors > 0) "The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.\n" else "") + 

+    (if (realErrors > 0 && smokeTestWarnings > 0) "The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.\n" else "") + 

     smokeResult + (if (smokeResult != "") "\n" else "") +

     status

   }

diff --git a/Chalice/tests/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice
index 563d72b6..abac4f5c 100644
--- a/Chalice/tests/examples/ProdConsChannel.chalice
+++ b/Chalice/tests/examples/ProdConsChannel.chalice
@@ -42,85 +42,4 @@ class Program {
       receive c := ch

     }

   }

-

-  // variations

-  method Main0() {  // error: debt remains after body

-    var ch := new Ch

-    fork tk0 := Producer(ch)

-    fork tk1 := Consumer(ch)

-    // join tk0

-    join tk1

-  }

-  method Main1() {

-    var ch := new Ch

-    fork tk0 := Producer(ch)

-    fork tk1 := Consumer(ch)

-    join tk0

-    // join tk1

-  }  // no problem

-  method Producer0(ch: Ch)  // error: debt remains after body

-    requires ch != null

-    ensures credit(ch)

-  {

-    var i := 0

-    while (i < 25)

-    {

-      var x := i*i

-      var c := new Cell { val := x }

-      send ch(c)

-      i := i + 1

-    }

-    // send ch(null)

-  }

-  method Producer1(ch: Ch)

-    requires ch != null

-    ensures credit(ch)

-  {

-    var i := 0

-    while (i < 25)

-    {

-      var x := i*i

-      var c := new Cell { val := x }

-      send ch(c)

-      i := i + 1 + c.val  // error: can no longer read c.val

-    }

-    send ch(null)

-  }

-  method Consumer0(ch: Ch)

-    requires rd(ch.mu) && waitlevel << ch.mu

-    requires credit(ch)

-    ensures rd(ch.mu)

-  {

-    var c: Cell

-    receive c := ch

-    while (c != null && c.val == 7)  // this consumer may end early, but that's allowed

-      invariant rd(ch.mu) && waitlevel << ch.mu

-      invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)

-    {

-      var i := c.val

-      receive c := ch

-    }

-  }

-  method Consumer1(ch: Ch)

-    requires rd(ch.mu) && waitlevel << ch.mu

-    requires credit(ch)

-    ensures rd(ch.mu)

-  {

-    var c: Cell

-    receive c := ch

-    if (c != null) {

-      assert 0 <= c.val  // follows from where clause

-    }

-  }

-  method Consumer2(ch: Ch)

-    requires rd(ch.mu) && waitlevel << ch.mu

-    requires credit(ch)

-    ensures rd(ch.mu)

-  {

-    var c: Cell

-    receive c := ch

-    if (c != null) {

-      assert c.val < 2  // error: does not follow from where clause

-    }

-  }

 }

diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt
index 167898fb..4d91605c 100644
--- a/Chalice/tests/examples/ProdConsChannel.output.txt
+++ b/Chalice/tests/examples/ProdConsChannel.output.txt
@@ -1,11 +1,4 @@
 Verification of ProdConsChannel.chalice using parameters="" 

 

-  47.3: Method body is not allowed to leave any debt.
-  61.3: Method body is not allowed to leave any debt.
-  85.20: Location might not be readable.
-  123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
-  80.5: The end of the while-loop is unreachable.
-
-Boogie program verifier finished with 4 errors and 1 smoke test warnings.

+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt
index bd34d380..ccb4e93c 100644
--- a/Chalice/tests/examples/UnboundedThreads.output.txt
+++ b/Chalice/tests/examples/UnboundedThreads.output.txt
@@ -2,5 +2,4 @@ Verification of UnboundedThreads.chalice using parameters=""
 

   40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27  for C.f.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt
index 468e5921..ce5b5844 100644
--- a/Chalice/tests/examples/linkedlist.output.txt
+++ b/Chalice/tests/examples/linkedlist.output.txt
@@ -2,5 +2,4 @@ Verification of linkedlist.chalice using parameters=""
 

   49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/ImplicitLocals.chalice b/Chalice/tests/general-tests/ImplicitLocals.chalice
index 15ebe8e0..15ebe8e0 100644
--- a/Chalice/tests/examples/ImplicitLocals.chalice
+++ b/Chalice/tests/general-tests/ImplicitLocals.chalice
diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/general-tests/ImplicitLocals.output.txt
index db26bba6..db26bba6 100644
--- a/Chalice/tests/examples/ImplicitLocals.output.txt
+++ b/Chalice/tests/general-tests/ImplicitLocals.output.txt
diff --git a/Chalice/tests/examples/LoopLockChange.chalice b/Chalice/tests/general-tests/LoopLockChange.chalice
index 5ccce089..5ccce089 100644
--- a/Chalice/tests/examples/LoopLockChange.chalice
+++ b/Chalice/tests/general-tests/LoopLockChange.chalice
diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/general-tests/LoopLockChange.output.txt
index 19e84f93..19e84f93 100644
--- a/Chalice/tests/examples/LoopLockChange.output.txt
+++ b/Chalice/tests/general-tests/LoopLockChange.output.txt
diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/general-tests/RockBand-automagic.chalice
index 8a64b691..8a64b691 100644
--- a/Chalice/tests/examples/RockBand-automagic.chalice
+++ b/Chalice/tests/general-tests/RockBand-automagic.chalice
diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/general-tests/RockBand-automagic.output.txt
index 2e62b457..2e62b457 100644
--- a/Chalice/tests/examples/RockBand-automagic.output.txt
+++ b/Chalice/tests/general-tests/RockBand-automagic.output.txt
diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/general-tests/SmokeTestTest.chalice
index 6ff283ec..6ff283ec 100644
--- a/Chalice/tests/examples/SmokeTestTest.chalice
+++ b/Chalice/tests/general-tests/SmokeTestTest.chalice
diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/general-tests/SmokeTestTest.output.txt
index 3d1cd786..3d1cd786 100644
--- a/Chalice/tests/examples/SmokeTestTest.output.txt
+++ b/Chalice/tests/general-tests/SmokeTestTest.output.txt
diff --git a/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice b/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice
new file mode 100644
index 00000000..2d2f9b91
--- /dev/null
+++ b/Chalice/tests/general-tests/VariationsOfProdConsChannel.chalice
@@ -0,0 +1,88 @@
+class Cell {

+  var val: int

+}

+

+channel Ch(c: Cell) where

+  c != null ==> acc(c.val) && 0 <= c.val && credit(this)

+

+class Program {

+  method Main0() {  // error: debt remains after body

+    var ch := new Ch

+    fork tk0 := Producer(ch)

+    fork tk1 := Consumer(ch)

+    // join tk0

+    join tk1

+  }

+  method Main1() {

+    var ch := new Ch

+    fork tk0 := Producer(ch)

+    fork tk1 := Consumer(ch)

+    join tk0

+    // join tk1

+  }  // no problem

+  method Producer0(ch: Ch)  // error: debt remains after body

+    requires ch != null

+    ensures credit(ch)

+  {

+    var i := 0

+    while (i < 25)

+    {

+      var x := i*i

+      var c := new Cell { val := x }

+      send ch(c)

+      i := i + 1

+    }

+    // send ch(null)

+  }

+  method Producer1(ch: Ch)

+    requires ch != null

+    ensures credit(ch)

+  {

+    var i := 0

+    while (i < 25)

+    {

+      var x := i*i

+      var c := new Cell { val := x }

+      send ch(c)

+      i := i + 1 + c.val  // error: can no longer read c.val

+    }

+    send ch(null)

+  }

+  method Consumer0(ch: Ch)

+    requires rd(ch.mu) && waitlevel << ch.mu

+    requires credit(ch)

+    ensures rd(ch.mu)

+  {

+    var c: Cell

+    receive c := ch

+    while (c != null && c.val == 7)  // this consumer may end early, but that's allowed

+      invariant rd(ch.mu) && waitlevel << ch.mu

+      invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)

+    {

+      var i := c.val

+      receive c := ch

+    }

+  }

+  method Consumer1(ch: Ch)

+    requires rd(ch.mu) && waitlevel << ch.mu

+    requires credit(ch)

+    ensures rd(ch.mu)

+  {

+    var c: Cell

+    receive c := ch

+    if (c != null) {

+      assert 0 <= c.val  // follows from where clause

+    }

+  }

+  method Consumer2(ch: Ch)

+    requires rd(ch.mu) && waitlevel << ch.mu

+    requires credit(ch)

+    ensures rd(ch.mu)

+  {

+    var c: Cell

+    receive c := ch

+    if (c != null) {

+      assert c.val < 2  // error: does not follow from where clause

+    }

+  }

+}

diff --git a/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt b/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt
new file mode 100644
index 00000000..d5b9c9ee
--- /dev/null
+++ b/Chalice/tests/general-tests/VariationsOfProdConsChannel.output.txt
@@ -0,0 +1,13 @@
+Verification of VariationsOfProdConsChannel.chalice using parameters="" 

+

+The program did not typecheck.

+11.5: call of undeclared member Producer in class Program

+<undefined position>: Invalid token type. Program does not declare a method Producer.

+12.5: call of undeclared member Consumer in class Program

+<undefined position>: Invalid token type. Program does not declare a method Consumer.

+14.10: the first argument of a join async must be a token

+18.5: call of undeclared member Producer in class Program

+<undefined position>: Invalid token type. Program does not declare a method Producer.

+19.5: call of undeclared member Consumer in class Program

+<undefined position>: Invalid token type. Program does not declare a method Consumer.

+20.10: the first argument of a join async must be a token

diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/general-tests/cell-defaults.chalice
index eb826f89..eb826f89 100644
--- a/Chalice/tests/examples/cell-defaults.chalice
+++ b/Chalice/tests/general-tests/cell-defaults.chalice
diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/general-tests/cell-defaults.output.txt
index 138a5717..138a5717 100644
--- a/Chalice/tests/examples/cell-defaults.output.txt
+++ b/Chalice/tests/general-tests/cell-defaults.output.txt
diff --git a/Chalice/tests/examples/counter.chalice b/Chalice/tests/general-tests/counter.chalice
index 828cf005..828cf005 100644
--- a/Chalice/tests/examples/counter.chalice
+++ b/Chalice/tests/general-tests/counter.chalice
diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/general-tests/counter.output.txt
index 1d5be0ea..1d5be0ea 100644
--- a/Chalice/tests/examples/counter.output.txt
+++ b/Chalice/tests/general-tests/counter.output.txt
diff --git a/Chalice/tests/general-tests/generate_reference.bat b/Chalice/tests/general-tests/generate_reference.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/general-tests/generate_reference.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/general-tests/generate_reference_all.bat b/Chalice/tests/general-tests/generate_reference_all.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/general-tests/generate_reference_all.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/examples/prog0.chalice b/Chalice/tests/general-tests/prog0.chalice
index fb835a24..fb835a24 100644
--- a/Chalice/tests/examples/prog0.chalice
+++ b/Chalice/tests/general-tests/prog0.chalice
diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/general-tests/prog0.output.txt
index 5b329874..5b329874 100644
--- a/Chalice/tests/examples/prog0.output.txt
+++ b/Chalice/tests/general-tests/prog0.output.txt
diff --git a/Chalice/tests/examples/prog1.chalice b/Chalice/tests/general-tests/prog1.chalice
index 133de36d..133de36d 100644
--- a/Chalice/tests/examples/prog1.chalice
+++ b/Chalice/tests/general-tests/prog1.chalice
diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/general-tests/prog1.output.txt
index 630ecdfa..630ecdfa 100644
--- a/Chalice/tests/examples/prog1.output.txt
+++ b/Chalice/tests/general-tests/prog1.output.txt
diff --git a/Chalice/tests/examples/prog2.chalice b/Chalice/tests/general-tests/prog2.chalice
index 55fe8ff5..55fe8ff5 100644
--- a/Chalice/tests/examples/prog2.chalice
+++ b/Chalice/tests/general-tests/prog2.chalice
diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/general-tests/prog2.output.txt
index b9d88bbe..b9d88bbe 100644
--- a/Chalice/tests/examples/prog2.output.txt
+++ b/Chalice/tests/general-tests/prog2.output.txt
diff --git a/Chalice/tests/examples/prog3.chalice b/Chalice/tests/general-tests/prog3.chalice
index de5dfad7..de5dfad7 100644
--- a/Chalice/tests/examples/prog3.chalice
+++ b/Chalice/tests/general-tests/prog3.chalice
diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/general-tests/prog3.output.txt
index 18d05658..18d05658 100644
--- a/Chalice/tests/examples/prog3.output.txt
+++ b/Chalice/tests/general-tests/prog3.output.txt
diff --git a/Chalice/tests/examples/prog4.chalice b/Chalice/tests/general-tests/prog4.chalice
index 3c655c71..3c655c71 100644
--- a/Chalice/tests/examples/prog4.chalice
+++ b/Chalice/tests/general-tests/prog4.chalice
diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/general-tests/prog4.output.txt
index 9415df7c..9415df7c 100644
--- a/Chalice/tests/examples/prog4.output.txt
+++ b/Chalice/tests/general-tests/prog4.output.txt
diff --git a/Chalice/tests/examples/quantifiers.chalice b/Chalice/tests/general-tests/quantifiers.chalice
index 7377ca3f..7377ca3f 100644
--- a/Chalice/tests/examples/quantifiers.chalice
+++ b/Chalice/tests/general-tests/quantifiers.chalice
diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/general-tests/quantifiers.output.txt
index 4abb22e1..2f325c42 100644
--- a/Chalice/tests/examples/quantifiers.output.txt
+++ b/Chalice/tests/general-tests/quantifiers.output.txt
@@ -2,5 +2,4 @@ Verification of quantifiers.chalice using parameters=""
 

   57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/general-tests/reg_test.bat b/Chalice/tests/general-tests/reg_test.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/general-tests/reg_test.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/general-tests/reg_test_all.bat b/Chalice/tests/general-tests/reg_test_all.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/general-tests/reg_test_all.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/general-tests/test.bat b/Chalice/tests/general-tests/test.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/general-tests/test.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt
index acbef565..02e7acb7 100644
--- a/Chalice/tests/permission-model/basic.output.txt
+++ b/Chalice/tests/permission-model/basic.output.txt
@@ -5,5 +5,4 @@ Verification of basic.chalice using parameters=""
   97.3: The postcondition at 99.13 might not hold. Insufficient fraction at 99.13 for Cell.x.
   148.3: The postcondition at 150.13 might not hold. Insufficient fraction at 150.13 for Cell.x.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 4 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt
index f588bc0a..159e0ee6 100644
--- a/Chalice/tests/permission-model/channels.output.txt
+++ b/Chalice/tests/permission-model/channels.output.txt
@@ -3,5 +3,4 @@ Verification of channels.chalice using parameters=""
   8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.
   18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 2 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt
index 2cb8d25d..f557b8c7 100644
--- a/Chalice/tests/permission-model/sequences.output.txt
+++ b/Chalice/tests/permission-model/sequences.output.txt
@@ -3,5 +3,4 @@ Verification of sequences.chalice using parameters=""
   36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
   60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
 
-The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
 Boogie program verifier finished with 2 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt
index be0b6f91..d6875825 100644
--- a/Chalice/tests/readme.txt
+++ b/Chalice/tests/readme.txt
@@ -5,8 +5,13 @@ Chalice Test Suite
 Contents

 --------

 - examples: Various examples how Chalice can be used to verify concurrent

-  programs.

-- permission-model: Regression tests for the permission model of Chalice.

+  programs. These tests represent (the core of) real problems and are therefore

+  well suited for performance and comparison tests (e.g. with other tools).

+- general-tests: Regression tests for various aspects of Chalice.

+- regressions: Regression tests for fixed bugs to ensure they do not occur

+  again.

+- permission-model: Regression tests specifically for the permission model of

+  Chalice.

 - refinements: Regression tests for the refinement extension.

 - test-scripts: Some batch scripts that can be used to execute the tests in an

   easy and automated way. More information below.

@@ -19,6 +24,7 @@ tests in different ways. There are launchers in the test directories (e.g. in
 examples or permission-model) to access them.

 

 Commands (sorted by relevance):

+- runalltests.bat: Executes all tests in all test folders.

 - test.bat <file> [-params]: Execute a test and output the result of the

   verification. Note: <file> must not include the file extension.

 - reg_test.bat <file> [-params]: Execute a tests as a regression test, i.e., run

diff --git a/Chalice/tests/regressions/generate_reference.bat b/Chalice/tests/regressions/generate_reference.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/regressions/generate_reference.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/regressions/generate_reference_all.bat b/Chalice/tests/regressions/generate_reference_all.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/regressions/generate_reference_all.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/regressions/reg_test.bat b/Chalice/tests/regressions/reg_test.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/regressions/reg_test.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/regressions/reg_test_all.bat b/Chalice/tests/regressions/reg_test_all.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/regressions/reg_test_all.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/regressions/test.bat b/Chalice/tests/regressions/test.bat
new file mode 100644
index 00000000..6864843c
--- /dev/null
+++ b/Chalice/tests/regressions/test.bat
@@ -0,0 +1,2 @@
+@echo off

+call "..\test-scripts\%0" %*

diff --git a/Chalice/tests/regressions/workitem-10147.chalice b/Chalice/tests/regressions/workitem-10147.chalice
new file mode 100644
index 00000000..eb6f31c7
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10147.chalice
@@ -0,0 +1,22 @@
+class Cell {

+  

+  var x: int;

+  

+  // the declaration of a method with the same name for a parameter

+  // as well as a result alone does not yet cause a problem, but ...

+  method problematic_method(c: Cell) returns (c: Cell)

+    requires acc(c.x);

+  {

+  }

+  

+  // ... calling it leads to various 'undeclared identifier' errors

+  // in boogie. (previously. now fixed by not allowing c as both in and out parameter)

+  method error()

+  {

+    var a: Cell := new Cell;

+    var b: Cell;

+    

+    call b := problematic_method(a);

+  }

+  

+}

diff --git a/Chalice/tests/regressions/workitem-10147.output.txt b/Chalice/tests/regressions/workitem-10147.output.txt
new file mode 100644
index 00000000..63bb3c9c
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10147.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10147.chalice using parameters="" 

+

+The program did not typecheck.

+7.3: duplicate parameter c of method problematic_method in class Cell

diff --git a/Chalice/tests/regressions/workitem-10190.chalice b/Chalice/tests/regressions/workitem-10190.chalice
new file mode 100644
index 00000000..ad84553a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10190.chalice
@@ -0,0 +1,6 @@
+// previously resulted in a StackOverFlowError of the Chalice parser
+class Node { 
+/*
+Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed diam voluptua. At vero eos et accusam et justo duo dolores et ea rebum. Stet clita kasd gubergren, no sea takimata sanctus est Lorem ipsum dolor sit amet. Lorem ipsum dolor sit amet, consetetur sadipscing elitr, sed diam nonumy eirmod tempor invidunt ut labore et dolore magna aliquyam erat, sed diam voluptua.
+*/
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10190.output.txt b/Chalice/tests/regressions/workitem-10190.output.txt
new file mode 100644
index 00000000..e314cbd3
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10190.output.txt
@@ -0,0 +1,5 @@
+Verification of workitem-10190.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 verified, 1 error
+

diff --git a/Chalice/tests/regressions/workitem-10192.chalice b/Chalice/tests/regressions/workitem-10192.chalice
new file mode 100644
index 00000000..06ff5881
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10192.chalice
@@ -0,0 +1,19 @@
+class Sequences { 
+	var xs: seq<int>
+
+	method append(a: int) 
+		requires acc(xs) 
+		ensures acc(xs) 
+		ensures size() == old(size()) + 1  /* verifies */ 
+		ensures |xs| == old(|xs|) + 1      /* previously failed */ 
+	{ xs := xs ++ [a] }
+	 
+	/* this heap-independent version also verifies. */ 
+	method append0(ins: seq<int>, a: int) returns (outs: seq<int>) 
+		ensures |outs| == |ins| + 1 
+	{ outs := ins ++ [a] } 
+	 
+	function size(): int  
+		requires rd(xs)
+	{ |xs| }
+} 
diff --git a/Chalice/tests/regressions/workitem-10192.output.txt b/Chalice/tests/regressions/workitem-10192.output.txt
new file mode 100644
index 00000000..1f5fbeec
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10192.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10192.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10194.chalice b/Chalice/tests/regressions/workitem-10194.chalice
new file mode 100644
index 00000000..5828b0bf
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10194.chalice
@@ -0,0 +1,37 @@
+class Test {
+	var x: int
+	var tk: token<Test.incX>
+	
+	predicate V { acc(x) }
+	
+	method incX()
+		requires V
+		ensures V
+	{
+		unfold V
+		x := x + 1
+		fold V
+	}
+	
+	method joinTk()
+		requires acc(tk) && tk != null && acc(tk.joinable) && tk.joinable
+		requires eval(tk.fork this.incX(), true)
+		ensures V
+		ensures unfolding V in x == old(x) // ERROR: old(x) is not readable (no error here, previously)
+	{
+		join tk
+		assert V
+	}
+
+	method test()
+		requires acc(x) && x == 0
+		requires acc(tk)
+	{
+		fold V
+		fork tklocal := incX()
+		tk := tklocal
+		call joinTk()
+		unfold V
+		assert x == old(x) // this verified previously (without any errors anywhere in the file)
+	}
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10194.output.txt b/Chalice/tests/regressions/workitem-10194.output.txt
new file mode 100644
index 00000000..3ed31c08
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10194.output.txt
@@ -0,0 +1,5 @@
+Verification of workitem-10194.chalice using parameters="" 

+

+  20.35: Location might not be readable.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10195.chalice b/Chalice/tests/regressions/workitem-10195.chalice
new file mode 100644
index 00000000..99ea69f8
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10195.chalice
@@ -0,0 +1,38 @@
+class Test { 
+    method fails() 
+    { 
+      assert forall j in [10..5] :: true // ERROR: min > max
+      assert false // failed previously, now we get a smoke warning
+    }   
+   
+    method succeeds1() 
+    { 
+      assert forall j in [10..5] :: f(j) == 0 // ERROR: min > max
+      assert false // failed previously, now we get a smoke warning
+    } 
+     
+    method fails1() 
+    { 
+      assert forall j in [5..10] :: f(j) == 0
+    }
+        
+        method succeeds2(a: int, b: int)
+            requires 0 <= a && 0 <= b
+            requires f(a) < f(b)
+        {
+      assert forall j in [f(b)..f(a)] :: f(j) == 0 // ERROR: min > max
+            assert false // holds
+        }
+        
+        method fails2(a: int, b: int)
+            requires 0 <= a && 0 <= b
+            requires 0 < f(a)
+            requires f(a) < f(b)
+        {
+      assert forall j in [f(a)..f(b)] :: f(j) == 0
+        }
+     
+    function f(i: int): int 
+      requires 0 <= i
+    { 0 }        
+  } 
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10195.output.txt b/Chalice/tests/regressions/workitem-10195.output.txt
new file mode 100644
index 00000000..0636df17
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10195.output.txt
@@ -0,0 +1,12 @@
+Verification of workitem-10195.chalice using parameters="" 

+

+  4.14: Range minimum might not be smaller or equal to range maximum.
+  10.14: Range minimum might not be smaller or equal to range maximum.
+
+The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
+  2.5: The end of method fails is unreachable.
+  8.5: The end of method succeeds1 is unreachable.
+  19.9: Precondition of method succeeds2 is equivalent to false.
+  27.9: Precondition of method fails2 is equivalent to false.
+
+Boogie program verifier finished with 2 errors and 4 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10196.chalice b/Chalice/tests/regressions/workitem-10196.chalice
new file mode 100644
index 00000000..9257e5c2
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10196.chalice
@@ -0,0 +1,11 @@
+class C { 
+	method singleWarning() 
+	{ assert forall i in [] :: true } // previously, quantification over the empty list resulted in Boogie errors
+ 
+	method multipleWarnings() 
+	{ assert forall i in [] :: reqIGt0(i) == i } // previously, quantification over the empty list resulted in Boogie errors
+	 
+	function reqIGt0(i: int): int 
+		requires i >= 0 
+	{ i } 
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10196.output.txt b/Chalice/tests/regressions/workitem-10196.output.txt
new file mode 100644
index 00000000..013880cc
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10196.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10196.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10197.chalice b/Chalice/tests/regressions/workitem-10197.chalice
new file mode 100644
index 00000000..7212581c
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10197.chalice
@@ -0,0 +1,7 @@
+class Cell { var x: int } 
+
+class Test { 
+	method noop() 
+		ensures old(waitlevel) == waitlevel // previously resulted in Boogie errors
+	{} 
+} 
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10197.output.txt b/Chalice/tests/regressions/workitem-10197.output.txt
new file mode 100644
index 00000000..9cc1319a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10197.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10197.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10198.chalice b/Chalice/tests/regressions/workitem-10198.chalice
new file mode 100644
index 00000000..fd51977d
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10198.chalice
@@ -0,0 +1,17 @@
+class Cell { var x: int } 
+
+class Test { 
+	method get() returns (c: Cell) 
+		ensures c != null 
+		lockchange c /* previosly, this introduced errors */ 
+	{ 
+		c := new Cell 
+	} 
+	 
+	/* method was needed to get Boogie errors */ 
+	method testRd() // expected ERROR: method might lock/unlock more than allowed
+    {
+        var x: Cell
+		call x := get() 
+	} 
+} 
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10198.output.txt b/Chalice/tests/regressions/workitem-10198.output.txt
new file mode 100644
index 00000000..8e421059
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10198.output.txt
@@ -0,0 +1,5 @@
+Verification of workitem-10198.chalice using parameters="" 

+

+  12.2: Method might lock/unlock more than allowed.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10199.chalice b/Chalice/tests/regressions/workitem-10199.chalice
new file mode 100644
index 00000000..678ed078
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10199.chalice
@@ -0,0 +1,21 @@
+class Test { 
+	var z: int 
+
+	predicate Z { acc(z) } 
+	predicate ZZ { Z } // XXX
+
+	method useZZ() 
+		requires ZZ 
+	{
+			// (ZZ,100)
+		unfold acc(ZZ, 40)
+			// (ZZ, 60), (Z, 40)
+		unfold acc(Z, 20) 
+			// (ZZ, 60), (Z, 20), (z, 20)
+		fold acc(Z, 10)
+			// (ZZ, 60), (Z, 30), (z, 10)
+		fold acc(ZZ, 30)
+			// previoulsy: Fold might fail because the definition of Test.ZZ does not hold. Insufficient fraction at XXX for Test.Z. 
+			// Should be (ZZ, 90), (z, 10)
+	}
+} 
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10199.output.txt b/Chalice/tests/regressions/workitem-10199.output.txt
new file mode 100644
index 00000000..4fb873e7
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10199.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10199.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-10200.chalice b/Chalice/tests/regressions/workitem-10200.chalice
new file mode 100644
index 00000000..a7394793
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10200.chalice
@@ -0,0 +1,25 @@
+class Test {
+	var f: int;
+	
+	function fib(n: int): int
+		requires n >= 0
+	{
+		n < 2 ? n : fib(n - 1) + fib(n - 2) // incompletness: termination not atomatically proven
+	}
+
+	method fibSeq(n: int) returns (r: int)
+		requires n >= 0
+		requires acc(this.f)
+		ensures acc(this.f)
+		ensures r == fib(n) // previous error: the postcondition might not hold
+	{
+		if (n < 2) {
+			r := n
+		} else {
+			var f1: int; var f2: int
+			call f1 := fibSeq(n - 1)
+			call f2 := fibSeq(n - 2)
+			r := f1 + f2
+		}
+	}
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10200.output.txt b/Chalice/tests/regressions/workitem-10200.output.txt
new file mode 100644
index 00000000..cac4bb62
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10200.output.txt
@@ -0,0 +1,5 @@
+Verification of workitem-10200.chalice using parameters="" 

+

+  7.15: The heap of the callee might not be strictly smaller than the heap of the caller.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-8234.chalice b/Chalice/tests/regressions/workitem-8234.chalice
new file mode 100644
index 00000000..5fbcea02
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-8234.chalice
@@ -0,0 +1,26 @@
+class Test{

+	var tests : seq<Test>;

+	var total : int;

+	

+	invariant acc(tests, 100);

+	invariant acc(total, 50);

+	

+	function at(loc : int) : Test

+		requires acc(tests);

+		requires loc >= 0 && loc < size();

+	{

+		tests[loc]

+	}

+	

+	

+	function size() : int

+		requires acc(tests);

+		ensures result >= 0;

+		ensures result == |tests|; // previously, there was a nullpointer exception here

+	{

+		|tests|

+	}

+	

+	predicate pre

+	{ acc(total, 50) }

+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-8234.output.txt b/Chalice/tests/regressions/workitem-8234.output.txt
new file mode 100644
index 00000000..8d13e17a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-8234.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-8234.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-8236.chalice b/Chalice/tests/regressions/workitem-8236.chalice
new file mode 100644
index 00000000..819bdb74
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-8236.chalice
@@ -0,0 +1,16 @@
+class Bug{

+

+	method Main() // expected ERROR: method might lock/unlock more than allowed

+	{

+		var a : Bug;

+		call a:= m();

+	}

+

+	method m() returns (a : Bug)

+		lockchange a // resulted previously in Boogie errors

+	{

+		a := new Bug;

+		share a;

+		acquire a;

+	}

+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-8236.output.txt b/Chalice/tests/regressions/workitem-8236.output.txt
new file mode 100644
index 00000000..30b42ab1
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-8236.output.txt
@@ -0,0 +1,5 @@
+Verification of workitem-8236.chalice using parameters="" 

+

+  3.2: Method might lock/unlock more than allowed.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/regressions/workitem-9978.chalice b/Chalice/tests/regressions/workitem-9978.chalice
new file mode 100644
index 00000000..02cd2e66
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-9978.chalice
@@ -0,0 +1,9 @@
+class C {

+  method nullPointerException()

+  {

+    while (true)

+    {

+      fork nullPointerException(); // previously, fork without token inside a while loop introduced a nullpointer exception.

+    }

+  }

+}

diff --git a/Chalice/tests/regressions/workitem-9978.output.txt b/Chalice/tests/regressions/workitem-9978.output.txt
new file mode 100644
index 00000000..0e557a3b
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-9978.output.txt
@@ -0,0 +1,6 @@
+Verification of workitem-9978.chalice using parameters="" 

+

+
+  4.5: The statements after the while-loop are unreachable.
+
+Boogie program verifier finished with 0 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/runalltests.bat b/Chalice/tests/runalltests.bat
index 3b0df4a4..f391b1f9 100644
--- a/Chalice/tests/runalltests.bat
+++ b/Chalice/tests/runalltests.bat
@@ -11,7 +11,7 @@ if "%1"=="-no-summary" (
 

 set t=0

 set c=0

-for %%f in (examples permission-model) do (

+for %%f in (examples permission-model general-tests regressions) do (

   echo Running tests in %%f ...

   echo ------------------------------------------------------

   cd %%f

diff --git a/Chalice/tests/test-scripts/readme.txt b/Chalice/tests/test-scripts/readme.txt
new file mode 100644
index 00000000..d4f408e8
--- /dev/null
+++ b/Chalice/tests/test-scripts/readme.txt
@@ -0,0 +1,3 @@
+

+The scripts in this directory are NOT meant for direct execution, but rather

+provide the implementation of the same-named scripts in the actual test folders.

diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
index 4ae603e8..8a05d7b2 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
@@ -10,7 +10,8 @@ namespace Demo
     {

       public Grammar() {

         #region 1. Terminals

-        NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");        

+        NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");

+        StringLiteral s = new StringLiteral("String", "\"", StringFlags.AllowsAllEscapes);

         IdentifierTerminal ident = new IdentifierTerminal("Identifier");

 

         // Copy pasted directly from Parser.scala

@@ -51,7 +52,6 @@ namespace Demo
 

         #region Disabled for a simpler grammar

         /*

-        StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

         Terminal dot = ToTerm(".", "dot");

         Terminal less = ToTerm("<");

         Terminal greater = ToTerm(">");

@@ -384,7 +384,7 @@ namespace Demo
         NonTerminal Simple = new NonTerminal("SimpleProg");

         NonTerminal Anything = new NonTerminal("Token");

         Simple.Rule = Anything.Star() + Eof;

-        Anything.Rule = n;

+        Anything.Rule = n | s;

         foreach (string keyword in reserved) Anything.Rule = Anything.Rule | ToTerm(keyword);

         Anything.Rule = Anything.Rule | ident;

         foreach (string delimiter in delimiters) Anything.Rule = Anything.Rule | ToTerm(delimiter);