Merge

author: Unknown <afd@afd-THINK.doc.ic.ac.uk> 2012-04-10 09:30:38 +0100
committer: Unknown <afd@afd-THINK.doc.ic.ac.uk> 2012-04-10 09:30:38 +0100
commit: d9ac9b3975fb54cce4dec82316e1852ec9bb6e68 (patch)
tree: 29187ece9655aa93ce1a31d09b3f1f64e56a904d
parent: 388caecdf98ec17712ceb11467546c3ea20674a4 (diff)
parent: 5db02f7f6576b5d6814f8a5c4c7291f845ac557a (diff)
3 files changed, 831 insertions, 606 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 3b933e42..7a7e850b 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -105,22 +105,26 @@ namespace BytecodeTranslator
     /// <remarks>still a stub</remarks>
     public override void TraverseChildren(IAddressableExpression addressableExpression)
     {
-      ILocalDefinition/*?*/ local = addressableExpression.Definition as ILocalDefinition;
+      Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");
+    }
+
+    private void LoadAddressOf(object container, IExpression/*?*/ instance) {
+
+      ILocalDefinition/*?*/ local = container as ILocalDefinition;
       if (local != null)
       {
         TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local)));
         return;
       }
-      IParameterDefinition/*?*/ param = addressableExpression.Definition as IParameterDefinition;
+      IParameterDefinition/*?*/ param = container as IParameterDefinition;
       if (param != null)
       {
         this.LoadParameter(param);
         return;
       }
-      IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;
+      IFieldReference/*?*/ field = container as IFieldReference;
       if (field != null) {
         var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field.ResolvedField));
-        var instance = addressableExpression.Instance;
         if (instance == null) {
           TranslatedExpressions.Push(f);
         } else {
@@ -132,31 +136,46 @@ namespace BytecodeTranslator
         } 
         return;
       }
-      IArrayIndexer/*?*/ arrayIndexer = addressableExpression.Definition as IArrayIndexer;
+      IArrayIndexer/*?*/ arrayIndexer = container as IArrayIndexer;
       if (arrayIndexer != null)
       {
         this.Traverse(arrayIndexer);
         return;
       }
-      IAddressDereference/*?*/ addressDereference = addressableExpression.Definition as IAddressDereference;
+      IAddressDereference/*?*/ addressDereference = container as IAddressDereference;
       if (addressDereference != null)
       {
         this.Traverse(addressDereference);
         return;
       }
-      IBlockExpression block = addressableExpression.Definition as IBlockExpression;
+      IBlockExpression block = container as IBlockExpression;
       if (block != null) {
         this.Traverse(block);
         return;
       }
-      IMethodReference/*?*/ method = addressableExpression.Definition as IMethodReference;
+      IMethodReference/*?*/ method = container as IMethodReference;
       if (method != null)
       {
         Console.WriteLine(MemberHelper.GetMethodSignature(method, NameFormattingOptions.Signature));
         //TODO
         throw new NotImplementedException();
       }
-      Contract.Assert(addressableExpression.Definition is IThisReference);
+      IExpression/*?*/ expression = container as IExpression;
+      if (expression != null) {
+        
+        this.Traverse(expression);
+        var e = this.TranslatedExpressions.Pop();
+
+        var newLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(expression.Type));
+        var cmd = Bpl.Cmd.SimpleAssign(Bpl.Token.NoToken, newLocal, e);
+        this.StmtTraverser.StmtBuilder.Add(cmd);
+
+        this.TranslatedExpressions.Push(newLocal);
+
+        return;
+      }
+
+      Contract.Assume(false);
     }
 
     public override void TraverseChildren(IAddressDereference addressDereference)
@@ -352,7 +371,9 @@ namespace BytecodeTranslator
           this.Traverse(addressOf.Expression);
         }
       } else {
-        this.Traverse(addressOf.Expression);
+        object container = addressOf.Expression.Definition;
+        IExpression/*?*/ instance = addressOf.Expression.Instance;
+        this.LoadAddressOf(container, instance);
         return;
       }
     }
@@ -729,7 +750,7 @@ namespace BytecodeTranslator
         // the AddressOf node should be ignored.
         var addrOf = thisArg as IAddressOf;
         var boogieType = this.sink.CciTypeToBoogie(methodToCall.ContainingType);
-        if (addrOf != null && boogieType != this.sink.Heap.RefType) {
+        if (false && addrOf != null && boogieType != this.sink.Heap.RefType) {
           thisArg = addrOf.Expression;
         }
 
@@ -759,20 +780,20 @@ namespace BytecodeTranslator
         }
 
         var expressionToTraverse = exp;
-        Bpl.Type boogieTypeOfExpression;
-
-        // Special case! exp can be an AddressOf expression if it is a value type being passed by reference.
-        // But since we pass reference parameters by in-out value passing, need to short-circuit the
-        // AddressOf node if the underlying type is not a Ref.
-        var addrOf = exp as IAddressOf;
-        if (addrOf != null) {
-          boogieTypeOfExpression = this.sink.CciTypeToBoogie(addrOf.Expression.Type);
-          if (boogieTypeOfExpression != this.sink.Heap.RefType) {
-            expressionToTraverse = addrOf.Expression;
-          }
-        }
+        //Bpl.Type boogieTypeOfExpression;
+
+        //// Special case! exp can be an AddressOf expression if it is a value type being passed by reference.
+        //// But since we pass reference parameters by in-out value passing, need to short-circuit the
+        //// AddressOf node if the underlying type is not a Ref.
+        //var addrOf = exp as IAddressOf;
+        //if (addrOf != null) {
+        //  boogieTypeOfExpression = this.sink.CciTypeToBoogie(addrOf.Expression.Type);
+        //  if (boogieTypeOfExpression != this.sink.Heap.RefType) {
+        //    expressionToTraverse = addrOf.Expression;
+        //  }
+        //}
 
-        boogieTypeOfExpression = this.sink.CciTypeToBoogie(expressionToTraverse.Type);
+        //boogieTypeOfExpression = this.sink.CciTypeToBoogie(expressionToTraverse.Type);
         this.Traverse(expressionToTraverse);
 
         Bpl.Expr e = this.TranslatedExpressions.Pop();
@@ -1312,39 +1333,54 @@ namespace BytecodeTranslator
       }
       IPropertyDefinition/*?*/ propertyDefinition = container as IPropertyDefinition;
       if (propertyDefinition != null) {
-        //Contract.Assume(propertyDefinition.Getter != null && propertyDefinition.Setter != null);
-        //if (!propertyDefinition.IsStatic) {
-        //  this.Traverse(target.Instance);
-        //}
-        //ILocalDefinition temp = null;
-        //if (pushTargetRValue) {
-        //  if (!propertyDefinition.IsStatic) {
-        //    this.generator.Emit(OperationCode.Dup);
-        //    this.generator.Emit(target.GetterIsVirtual ? OperationCode.Callvirt : OperationCode.Call, propertyDefinition.Getter);
-        //  } else {
-        //    this.generator.Emit(OperationCode.Call, propertyDefinition.Getter);
-        //  }
-        //  if (!treatAsStatement && resultIsInitialTargetRValue) {
-        //    this.generator.Emit(OperationCode.Dup);
-        //    this.StackSize++;
-        //    temp = new TemporaryVariable(source.Type, this.method);
-        //    this.VisitAssignmentTo(temp);
-        //  }
-        //}
-        //sourceTraverser(source);
-        //if (!treatAsStatement && !resultIsInitialTargetRValue) {
-        //  this.generator.Emit(OperationCode.Dup);
-        //  this.StackSize++;
-        //  temp = new TemporaryVariable(propertyDefinition.Type, this.method);
-        //  this.VisitAssignmentTo(temp);
-        //}
-        //if (!propertyDefinition.IsStatic) {
-        //  this.generator.Emit(target.SetterIsVirtual ? OperationCode.Callvirt : OperationCode.Call, propertyDefinition.Setter);
-        //} else {
-        //  this.generator.Emit(OperationCode.Call, propertyDefinition.Setter);
-        //}
-        //if (temp != null) this.LoadLocal(temp);
-        //return;
+        Contract.Assume(propertyDefinition.Getter != null && propertyDefinition.Setter != null);
+        if (!propertyDefinition.IsStatic) {
+          this.Traverse(target.Instance);
+        }
+        Bpl.IdentifierExpr temp = null;
+        var token = Bpl.Token.NoToken;
+        if (pushTargetRValue) {
+
+          List<Bpl.Expr> inexpr;
+          List<Bpl.IdentifierExpr> outvars;
+          Bpl.IdentifierExpr thisExpr;
+          Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr, bool>> toBoxed;
+          var proc2 = TranslateArgumentsAndReturnProcedure(token, propertyDefinition.Getter, propertyDefinition.Getter.ResolvedMethod, target.Instance, IteratorHelper.GetEmptyEnumerable<IExpression>(), out inexpr, out outvars, out thisExpr, out toBoxed);
+
+          EmitLineDirective(token);
+
+          this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc2.Name, inexpr, outvars));
+
+          if (!treatAsStatement && resultIsInitialTargetRValue) {
+            //var 
+            //this.generator.Emit(OperationCode.Dup);
+            //this.StackSize++;
+            //temp = new TemporaryVariable(source.Type, this.method);
+            //this.VisitAssignmentTo(temp);
+          }
+        }
+        sourceTraverser(source);
+        if (!treatAsStatement && !resultIsInitialTargetRValue) {
+          var e3 = this.TranslatedExpressions.Pop();
+          var loc = this.sink.CreateFreshLocal(source.Type);
+          temp = Bpl.Expr.Ident(loc);
+          var cmd = Bpl.Cmd.SimpleAssign(tok, temp, e3);
+          this.StmtTraverser.StmtBuilder.Add(cmd);
+          this.TranslatedExpressions.Push(temp);
+        }
+
+        var setterArgs = new List<Bpl.Expr>();
+        var setterArg = this.TranslatedExpressions.Pop();
+        if (!propertyDefinition.IsStatic)
+          setterArgs.Add(this.TranslatedExpressions.Pop());
+        setterArgs.Add(setterArg);
+
+        var setterProc = this.sink.FindOrCreateProcedure(propertyDefinition.Setter.ResolvedMethod);
+        EmitLineDirective(token);
+        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, setterProc.Decl.Name, setterArgs, new List<Bpl.IdentifierExpr>()));
+
+        if (temp != null) this.TranslatedExpressions.Push(temp);
+        return;
       }
       Contract.Assume(false);
     }
@@ -1519,7 +1555,23 @@ namespace BytecodeTranslator
 
 
     public override void TraverseChildren(IBitwiseAnd bitwiseAnd) {
-      base.TraverseChildren(bitwiseAnd);
+      var targetExpression = bitwiseAnd.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x &= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, bitwiseAnd, (IExpression e) => this.TraverseBitwiseAndRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: bitwiseAnd.ResultIsUnmodifiedLeftOperand);
+      } else { // x & e
+        this.Traverse(bitwiseAnd.LeftOperand);
+        this.TraverseBitwiseAndRightOperandAndDoOperation(bitwiseAnd);
+      }
+    }
+    private void TraverseBitwiseAndRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IBitwiseAnd);
+      var bitwiseAnd = (IBitwiseAnd)expression;
+
+      this.Traverse(bitwiseAnd.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1537,7 +1589,23 @@ namespace BytecodeTranslator
     }
 
     public override void TraverseChildren(IBitwiseOr bitwiseOr) {
-      base.TraverseChildren(bitwiseOr);
+      var targetExpression = bitwiseOr.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x |= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, bitwiseOr, (IExpression e) => this.TraverseBitwiseOrRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: bitwiseOr.ResultIsUnmodifiedLeftOperand);
+      } else { // x | e
+        this.Traverse(bitwiseOr.LeftOperand);
+        this.TraverseBitwiseOrRightOperandAndDoOperation(bitwiseOr);
+      }
+    }
+
+    private void TraverseBitwiseOrRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IBitwiseOr);
+      var bitwiseOr = (IBitwiseOr)expression;
+      this.Traverse(bitwiseOr.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1555,7 +1623,23 @@ namespace BytecodeTranslator
     }
 
     public override void TraverseChildren(IModulus modulus) {
-      base.TraverseChildren(modulus);
+      var targetExpression = modulus.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x %= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, modulus, (IExpression e) => this.TraverseModulusRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: modulus.ResultIsUnmodifiedLeftOperand);
+      } else { // x % e
+        this.Traverse(modulus.LeftOperand);
+        this.TraverseModulusRightOperandAndDoOperation(modulus);
+      }
+    }
+
+    private void TraverseModulusRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IModulus);
+      var modulus = (IModulus)expression;
+      this.Traverse(modulus.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1577,7 +1661,23 @@ namespace BytecodeTranslator
 
     public override void TraverseChildren(IDivision division)
     {
-      base.TraverseChildren(division);
+      var targetExpression = division.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x /= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, division, (IExpression e) => this.TraverseDivisionRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: division.ResultIsUnmodifiedLeftOperand);
+      } else { // x / e
+        this.Traverse(division.LeftOperand);
+        this.TraverseDivisionRightOperandAndDoOperation(division);
+      }
+    }
+
+    private void TraverseDivisionRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IDivision);
+      var division = (IDivision)expression;
+      this.Traverse(division.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1598,7 +1698,23 @@ namespace BytecodeTranslator
     }
 
     public override void TraverseChildren(IExclusiveOr exclusiveOr) {
-      base.TraverseChildren(exclusiveOr);
+      var targetExpression = exclusiveOr.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x ^= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, exclusiveOr, (IExpression e) => this.TraverseExclusiveOrRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: exclusiveOr.ResultIsUnmodifiedLeftOperand);
+      } else { // x ^ e
+        this.Traverse(exclusiveOr.LeftOperand);
+        this.TraverseExclusiveOrRightOperandAndDoOperation(exclusiveOr);
+      }
+    }
+
+    private void TraverseExclusiveOrRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IExclusiveOr);
+      var exclusiveOr = (IExclusiveOr)expression;
+      this.Traverse(exclusiveOr.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       var e = new Bpl.NAryExpr(
@@ -1611,7 +1727,22 @@ namespace BytecodeTranslator
 
     public override void TraverseChildren(ISubtraction subtraction)
     {
-      base.TraverseChildren(subtraction);
+      var targetExpression = subtraction.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x -= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, subtraction, (IExpression e) => this.TraverseSubtractionRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: subtraction.ResultIsUnmodifiedLeftOperand);
+      } else { // x - e
+        this.Traverse(subtraction.LeftOperand);
+        this.TraverseSubtractionRightOperandAndDoOperation(subtraction);
+      }
+    }
+    private void TraverseSubtractionRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is ISubtraction);
+      var subtraction = (ISubtraction)expression;
+
+      this.Traverse(subtraction.RightOperand);
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1633,7 +1764,23 @@ namespace BytecodeTranslator
 
     public override void TraverseChildren(IMultiplication multiplication)
     {
-      base.TraverseChildren(multiplication);
+      var targetExpression = multiplication.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x *= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, multiplication, (IExpression e) => this.TraverseMultiplicationRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: multiplication.ResultIsUnmodifiedLeftOperand);
+      } else { // x * e
+        this.Traverse(multiplication.LeftOperand);
+        this.TraverseMultiplicationRightOperandAndDoOperation(multiplication);
+      }
+    }
+
+    private void TraverseMultiplicationRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IMultiplication);
+      var multiplication = (IMultiplication)expression;
+      this.Traverse(multiplication.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e;
@@ -1751,6 +1898,15 @@ namespace BytecodeTranslator
 
     public override void TraverseChildren(IEquality equal)
     {
+      if ((equal.LeftOperand.Type.TypeCode != PrimitiveTypeCode.NotPrimitive || equal.LeftOperand.Type.TypeCode != PrimitiveTypeCode.NotPrimitive)
+        && !TypeHelper.TypesAreEquivalent(equal.LeftOperand.Type, equal.RightOperand.Type)) {
+        throw new TranslationException(
+          String.Format("Decompiler messed up: equality's left operand is of type '{0}' but right operand is of type '{1}'.",
+          TypeHelper.GetTypeName(equal.LeftOperand.Type),
+          TypeHelper.GetTypeName(equal.RightOperand.Type)
+          ));
+      }
+
       base.TraverseChildren(equal);
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1759,6 +1915,17 @@ namespace BytecodeTranslator
 
     public override void TraverseChildren(INotEquality nonEqual)
     {
+
+      if ((nonEqual.LeftOperand.Type.TypeCode != PrimitiveTypeCode.NotPrimitive || nonEqual.LeftOperand.Type.TypeCode != PrimitiveTypeCode.NotPrimitive)
+        &&
+        !TypeHelper.TypesAreEquivalent(nonEqual.LeftOperand.Type, nonEqual.RightOperand.Type)) {
+        throw new TranslationException(
+          String.Format("Decompiler messed up: inequality's left operand is of type '{0}' but right operand is of type '{1}'.",
+          TypeHelper.GetTypeName(nonEqual.LeftOperand.Type),
+          TypeHelper.GetTypeName(nonEqual.RightOperand.Type)
+          ));
+      }
+
       base.TraverseChildren(nonEqual);
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
@@ -1766,7 +1933,23 @@ namespace BytecodeTranslator
     }
 
     public override void TraverseChildren(IRightShift rightShift) {
-      base.TraverseChildren(rightShift);
+      var targetExpression = rightShift.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x >>= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, rightShift, (IExpression e) => this.TraverseRightShiftRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: rightShift.ResultIsUnmodifiedLeftOperand);
+      } else { // x >> e
+        this.Traverse(rightShift.LeftOperand);
+        this.TraverseRightShiftRightOperandAndDoOperation(rightShift);
+      }
+    }
+
+    private void TraverseRightShiftRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is IRightShift);
+      var rightShift = (IRightShift)expression;
+      this.Traverse(rightShift.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e = new Bpl.NAryExpr(
@@ -1778,7 +1961,23 @@ namespace BytecodeTranslator
     }
 
     public override void TraverseChildren(ILeftShift leftShift) {
-      base.TraverseChildren(leftShift);
+      var targetExpression = leftShift.LeftOperand as ITargetExpression;
+      if (targetExpression != null) { // x <<= e
+        bool statement = this.currentExpressionIsOpAssignStatement;
+        this.currentExpressionIsOpAssignStatement = false;
+        this.VisitAssignment(targetExpression, leftShift, (IExpression e) => this.TraverseLeftShiftRightOperandAndDoOperation(e),
+          treatAsStatement: statement, pushTargetRValue: true, resultIsInitialTargetRValue: leftShift.ResultIsUnmodifiedLeftOperand);
+      } else { // x << e
+        this.Traverse(leftShift.LeftOperand);
+        this.TraverseLeftShiftRightOperandAndDoOperation(leftShift);
+      }
+    }
+
+    private void TraverseLeftShiftRightOperandAndDoOperation(IExpression expression) {
+      Contract.Assume(expression is ILeftShift);
+      var leftShift = (ILeftShift)expression;
+      this.Traverse(leftShift.RightOperand);
+
       Bpl.Expr rexp = TranslatedExpressions.Pop();
       Bpl.Expr lexp = TranslatedExpressions.Pop();
       Bpl.Expr e = new Bpl.NAryExpr(
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 92438297..33f173ce 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -1,7 +1,7 @@
 // Copyright (c) 2010, Microsoft Corp.
 // Bytecode Translator prelude
 
-type HeapType = [Ref][Field]Box;
+type HeapType = [Ref][Field]Union;
 
 var $Alloc: [Ref]bool;
 
@@ -58,6 +58,18 @@ function {:builtin "MapImp"} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]
 
 axiom MultisetEmpty == mapconstint(0);
 
+function IsRef(u: Union) : bool;
+
+axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x)));
+
+axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x)));
+
+axiom (forall x: Real :: { Real2Union(x) } Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x)));
+
+axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x)));
+
+axiom (forall x: Ref :: { Struct2Union(x) } Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x)));
+
 function $TypeOfInv(Ref) : Type;
 
 axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);
@@ -73,17 +85,11 @@ implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Re
 
 
 
-axiom Box2Int($DefaultBox) == 0;
-
-axiom Box2Bool($DefaultBox) == false;
-
-axiom Box2Ref($DefaultBox) == null;
-
-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
+axiom Union2Int($DefaultHeapValue) == 0;
 
-axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);
+axiom Union2Bool($DefaultHeapValue) == false;
 
-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x);
+axiom Union2Ref($DefaultHeapValue) == null;
 
 function $ThreadDelegate(Ref) : Ref;
 
@@ -109,11 +115,11 @@ implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref
 
 
 
-procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
 
 
 
-implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
 {
     $Exception := null;
     call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -147,11 +153,11 @@ implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
 
 
 
-procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
+procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 
 
 
-implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
 {
     $Exception := null;
     call System.Threading.ThreadStart.Invoke(this);
@@ -182,7 +188,8 @@ implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
     else
     {
         call c := Alloc();
-        assume $Delegate(c) == MultisetPlus($Delegate(a), $Delegate(b));
+        assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b);
+        assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
     }
 }
 
@@ -204,14 +211,15 @@ implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
     {
         c := a;
     }
-    else if (MultisetMinus($Delegate(a), $Delegate(b)) == MultisetEmpty)
+    else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty)
     {
         c := null;
     }
     else
     {
         call c := Alloc();
-        assume $Delegate(c) == MultisetMinus($Delegate(a), $Delegate(b));
+        assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
+        assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0;
     }
 }
 
@@ -224,7 +232,8 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
 {
     call c := Alloc();
-    assume $Delegate(c) == MultisetSingleton(d);
+    assume $RefToDelegate(c) == d;
+    assume $RefToDelegateMultiset(c) == MultisetSingleton(d);
 }
 
 
@@ -251,141 +260,176 @@ implementation System.String.op_Inequality$System.String$System.String(a$in: Ref
 
 
 
-var isControlEnabled: [Ref]bool;
+var $Heap: HeapType;
 
-var isControlChecked: [Ref]bool;
+function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Union
+{
+  H[o][f]
+}
 
-procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
+function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Union) : HeapType
+{
+  H[o := H[o][f := v]]
+}
 
+var $ArrayContents: [Ref][int]Union;
 
+function $ArrayLength(Ref) : int;
 
-implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool)
+type {:datatype} Delegate;
+
+type DelegateMultiset = [Delegate]int;
+
+const unique MultisetEmpty: DelegateMultiset;
+
+function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset
 {
-    $Exception := null;
-    isControlEnabled[$this] := value$in;
+  MultisetEmpty[x := 1]
 }
 
+function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+{
+  mapadd(x, y)
+}
 
+function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+{
+  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))
+}
 
-procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
+type Field;
 
+type Union;
 
+const unique $DefaultHeapValue: Union;
 
-implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref)
-{
-  var enabledness: bool;
+type Ref;
 
-    $Exception := null;
-    enabledness := isControlEnabled[$this];
-    $result := Box2Ref(Bool2Box(enabledness));
-}
+const unique null: Ref;
 
+type {:datatype} Type;
 
+type Real;
 
-procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
+const unique $DefaultReal: Real;
 
+procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref);
 
 
-implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref)
-{
-  var check: bool;
 
-    $Exception := null;
-    check := Box2Bool(Ref2Box(value$in));
-    isControlChecked[$this] := check;
+implementation {:inline 1} $BoxFromBool(b: bool) returns (r: Ref)
+{
+    call r := Alloc();
+    assume $BoxedValue(r) == Bool2Union(b);
 }
 
 
 
-procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
+procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref);
 
 
 
-implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref)
+implementation {:inline 1} $BoxFromInt(i: int) returns (r: Ref)
 {
-  var isChecked: bool;
-
-    $Exception := null;
-    isChecked := isControlChecked[$this];
-    $result := Box2Ref(Bool2Box(isChecked));
+    call r := Alloc();
+    assume $BoxedValue(r) == Int2Union(i);
 }
 
 
 
-const unique $BoxField: Field;
+procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref);
 
-var $Heap: HeapType;
 
-function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Box
+
+implementation {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref)
 {
-  H[o][f]
+    call rf := Alloc();
+    assume $BoxedValue(rf) == Real2Union(r);
 }
 
-function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Box) : HeapType
+
+
+procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref);
+
+
+
+implementation {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref)
 {
-  H[o := H[o][f := v]]
+    call r := Alloc();
+    assume $BoxedValue(r) == Struct2Union(s);
 }
 
-var $ArrayContents: [Ref][int]Box;
 
-function $ArrayLength(Ref) : int;
 
-type {:datatype} Delegate;
+procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref);
 
-type DelegateMultiset = [Delegate]int;
 
-const unique MultisetEmpty: DelegateMultiset;
 
-function {:inline} MultisetSingleton(x: Delegate) : DelegateMultiset
+implementation {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref)
 {
-  MultisetEmpty[x := 1]
+    if (IsRef(u))
+    {
+        r := Union2Ref(u);
+    }
+    else
+    {
+        call r := Alloc();
+        assume $BoxedValue(r) == u;
+    }
 }
 
-function {:inline} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+
+
+function $BoxedValue(r: Ref) : Union;
+
+function {:inline true} $Unbox2Bool(r: Ref) : bool
 {
-  mapadd(x, y)
+  Union2Bool($BoxedValue(r))
 }
 
-function {:inline} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+function {:inline true} $Unbox2Int(r: Ref) : int
 {
-  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))
+  Union2Int($BoxedValue(r))
 }
 
-type Field;
-
-type Box;
-
-const unique $DefaultBox: Box;
-
-type Ref;
+function {:inline true} $Unbox2Real(r: Ref) : Real
+{
+  Union2Real($BoxedValue(r))
+}
 
-const unique null: Ref;
+function {:inline true} $Unbox2Struct(r: Ref) : Ref
+{
+  Union2Struct($BoxedValue(r))
+}
 
-type {:datatype} Type;
+function {:inline true} $Unbox2Union(r: Ref) : Union
+{
+  $BoxedValue(r)
+}
 
-type Real;
+function Union2Bool(u: Union) : bool;
 
-const unique $DefaultReal: Real;
+function Union2Int(u: Union) : int;
 
-function Box2Bool(Box) : bool;
+function Union2Ref(u: Union) : Ref;
 
-function Box2Int(Box) : int;
+function Union2Real(u: Union) : Real;
 
-function Box2Ref(Box) : Ref;
+function Union2Struct(u: Union) : Ref;
 
-function Box2Real(Box) : Real;
+function Bool2Union(boolValue: bool) : Union;
 
-function Bool2Box(bool) : Box;
+function Int2Union(intValue: int) : Union;
 
-function Int2Box(int) : Box;
+function Ref2Union(refValue: Ref) : Union;
 
-function Ref2Box(Ref) : Box;
+function Real2Union(realValue: Real) : Union;
 
-function Real2Box(Real) : Box;
+function Struct2Union(structValue: Ref) : Union;
 
-function {:inline true} Box2Box(b: Box) : Box
+function {:inline true} Union2Union(u: Union) : Union
 {
-  b
+  u
 }
 
 function Int2Real(int) : Real;
@@ -432,9 +476,11 @@ function $Subtype(Type, Type) : bool;
 
 function $DisjointSubtree(Type, Type) : bool;
 
-function $Delegate(Ref) : DelegateMultiset;
+function $RefToDelegate(Ref) : Delegate;
+
+function $RefToDelegateMultiset(Ref) : DelegateMultiset;
 
-function {:constructor} $DelegateCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate;
+function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate;
 
 var {:thread_local} $Exception: Ref;
 
@@ -474,11 +520,11 @@ implementation {:inline 1} RegressionTestInput.StructContainingStruct.#default_c
 {
   var $tmp0: Ref;
 
-    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.d, Real2Box($DefaultReal));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.d, Real2Union($DefaultReal));
     call $tmp0 := Alloc();
     call RegressionTestInput.S.#default_ctor($tmp0);
     assume $DynamicType($tmp0) == T$RegressionTestInput.S();
-    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.s, Ref2Box($tmp0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp0));
 }
 
 
@@ -499,9 +545,9 @@ implementation {:inline 1} RegressionTestInput.StructContainingStruct.#copy_ctor
 
     call other := Alloc();
     assume $DynamicType(other) == T$RegressionTestInput.StructContainingStruct();
-    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.d, Real2Box(Box2Real(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.d))));
-    call $tmp1 := RegressionTestInput.S.#copy_ctor(Box2Ref(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.s)));
-    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.s, Ref2Box($tmp1));
+    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.d, Real2Union(Union2Real(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.d))));
+    call $tmp1 := RegressionTestInput.S.#copy_ctor(Union2Ref(Read($Heap, this, F$RegressionTestInput.StructContainingStruct.s)));
+    $Heap := Write($Heap, other, F$RegressionTestInput.StructContainingStruct.s, Ref2Union($tmp1));
 }
 
 
@@ -514,18 +560,12 @@ implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionT
 {
   var s: Ref;
   var t_Ref: Ref;
-  var $tmp0: Ref;
   var $localExc: Ref;
   var $label: int;
 
     s := s$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 206} true;
-    call $tmp0 := Alloc();
-    call RegressionTestInput.StructContainingStruct.#default_ctor($tmp0);
-    assume $DynamicType($tmp0) == T$RegressionTestInput.StructContainingStruct();
-    t_Ref := $tmp0;
+    assume {:breadcrumb 0} true;
     call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 208} true;
     $result := t_Ref;
     return;
 }
@@ -551,15 +591,14 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
   var $label: int;
 
     d := d$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+    assume {:breadcrumb 1} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
     call System.Console.WriteLine$System.Double(d);
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
-    return;
 }
 
 
@@ -575,15 +614,14 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
   var $label: int;
 
     o := o$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real(Read($Heap, o, $BoxField)));
+    assume {:breadcrumb 2} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o));
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
-    return;
 }
 
 
@@ -603,40 +641,40 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
+    assume {:breadcrumb 3} true;
     d_Real := $real_literal_3_0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
     d2_Real := $real_literal_4_0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
-    return;
 }
 
 
@@ -654,13 +692,12 @@ implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 4} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -692,10 +729,10 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this:
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
-    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
-    return;
+    assume {:breadcrumb 5} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(Union2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
 }
 
 
@@ -709,15 +746,14 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($th
   var $localExc: Ref;
   var $label: int;
 
-    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
-    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Union(0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Union(0));
+    assume {:breadcrumb 6} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -748,24 +784,18 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 {
   var s_Ref: Ref;
   var $tmp0: Ref;
-  var $tmp1: Ref;
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 7} true;
     call $tmp0 := Alloc();
     call RegressionTestInput.S.#default_ctor($tmp0);
     assume $DynamicType($tmp0) == T$RegressionTestInput.S();
     s_Ref := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
-    call $tmp1 := Alloc();
-    call RegressionTestInput.S.#default_ctor($tmp1);
-    assume $DynamicType($tmp1) == T$RegressionTestInput.S();
-    s_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
-    assert Box2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
-    assert !Box2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b));
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
+    assert Union2Int(Read($Heap, s_Ref, F$RegressionTestInput.S.x)) == 0;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
+    assert !Union2Bool(Read($Heap, s_Ref, F$RegressionTestInput.S.b));
     $result := s_Ref;
     return;
 }
@@ -783,11 +813,12 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
   var $label: int;
 
     s := s$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
-    $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
-    assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
+    assume {:breadcrumb 8} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+    $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Union(3));
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
+    assert Union2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
     $result := s;
     return;
 }
@@ -803,13 +834,12 @@ implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 9} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -845,26 +875,19 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
+    assume {:breadcrumb 10} true;
     call $tmp0 := Alloc();
     assume $ArrayLength($tmp0) == 1 * 5;
     s_Ref := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
-    $ArrayContents := $ArrayContents[s_Ref := $ArrayContents[s_Ref][0 := Int2Box(2)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
-    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
+    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
     call $tmp1 := Alloc();
     assume $ArrayLength($tmp1) == 1 * 4;
     t_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
-    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
-    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
-    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
-    return;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
+    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
+    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
 }
 
 
@@ -881,26 +904,24 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
+    assume {:breadcrumb 11} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
     call $tmp0 := Alloc();
     assume $ArrayLength($tmp0) == 1 * 5;
     F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
-    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
-    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
+    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
+    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
     call $tmp1 := Alloc();
     assume $ArrayLength($tmp1) == 1 * 4;
     t_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
-    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
-    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
-    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
-    return;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
+    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
+    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
 }
 
 
@@ -918,16 +939,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
-    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
-    $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
-    _loc0_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
-    _loc1_Ref := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
-    assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
-    return;
+    assume {:breadcrumb 12} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+    $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Union(42)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+    $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Union(43)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
+    _loc0_Ref := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+    _loc1_Ref := Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+    assert Union2Int($ArrayContents[_loc0_Ref][x + 1]) == Union2Int($ArrayContents[_loc1_Ref][x]) + 1;
 }
 
 
@@ -943,24 +965,23 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($
   var $label: int;
 
     xs := xs$in;
-    if (xs != null)
+    assume {:breadcrumb 13} true;
+    if (!(xs != null))
     {
     }
     else
     {
     }
 
-    if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
+    if ((if !(xs != null) then true else !($ArrayLength(xs) > 0)) == 0)
     {
-        assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+        $ArrayContents := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Union2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
     }
     else
     {
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
-    return;
 }
 
 
@@ -974,14 +995,13 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
-    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Union(null));
+    assume {:breadcrumb 14} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1012,14 +1032,13 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#
   var $localExc: Ref;
   var $label: int;
 
-    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Box(0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Union(0));
+    assume {:breadcrumb 15} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1051,7 +1070,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
+    assume {:breadcrumb 16} true;
     $result := BitwiseAnd(x, y);
     return;
 }
@@ -1071,7 +1090,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
+    assume {:breadcrumb 17} true;
     $result := BitwiseOr(x, y);
     return;
 }
@@ -1091,7 +1110,7 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
+    assume {:breadcrumb 18} true;
     $result := BitwiseExclusiveOr(x, y);
     return;
 }
@@ -1109,7 +1128,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
+    assume {:breadcrumb 19} true;
     $result := BitwiseNegation(x);
     return;
 }
@@ -1125,13 +1144,12 @@ implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 20} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1171,13 +1189,12 @@ implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 21} true;
     call System.Attribute.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1206,10 +1223,9 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
+    assume {:breadcrumb 22} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
     x$out := x$out + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
-    return;
 }
 
 
@@ -1223,13 +1239,12 @@ implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 23} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1257,13 +1272,12 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 24} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1281,13 +1295,12 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 25} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1300,55 +1313,51 @@ procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref,
 
 
 
-procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Box);
+procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union);
 
 
 
 implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)
 {
   var x: int;
-  var CS$0$0000_Box: Box;
-  var $tmp0: Ref;
-  var __temp_2_Box: Box;
-  var __temp_3_Box: Box;
-  var $tmp1: Box;
-  var $tmp2: Box;
-  var y_Box: Box;
+  var CS$0$0000_Union: Union;
+  var $tmp0: Union;
+  var $tmp1: Union;
+  var $tmp2: Ref;
+  var y_Union: Union;
   var $localExc: Ref;
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
+    assume {:breadcrumb 26} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
-    CS$0$0000_Box := $DefaultBox;
-    call $tmp0 := Alloc();
-    $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000_Box));
-    if ($tmp0 != null)
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    CS$0$0000_Union := $DefaultHeapValue;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    call $tmp2 := $BoxFromUnion(CS$0$0000_Union);
+    if ($tmp2 != null)
     {
-        CS$0$0000_Box := $DefaultBox;
-        __temp_2_Box := CS$0$0000_Box;
     }
     else
     {
-        call $tmp2 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
-        $tmp1 := Box2Box($tmp2);
+        call $tmp1 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
+        $tmp0 := Union2Union($tmp1);
         if ($Exception != null)
         {
             return;
         }
-
-        __temp_3_Box := $tmp1;
-        __temp_2_Box := __temp_3_Box;
     }
 
-    y_Box := __temp_2_Box;
-    return;
+    y_Union := (if $tmp2 != null then $DefaultHeapValue else $tmp0);
 }
 
 
@@ -1385,8 +1394,8 @@ implementation T$RegressionTestInput.NestedGeneric.#cctor()
 
 implementation {:inline 1} RegressionTestInput.S.#default_ctor($this: Ref)
 {
-    $Heap := Write($Heap, $this, F$RegressionTestInput.S.x, Int2Box(0));
-    $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Box(false));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.S.x, Int2Union(0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.S.b, Bool2Union(false));
 }
 
 
@@ -1395,8 +1404,8 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref) returns (
 {
     call other := Alloc();
     assume $DynamicType(other) == T$RegressionTestInput.S();
-    $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
-    $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, F$RegressionTestInput.S.b))));
+    $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Union(Union2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
+    $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Union(Union2Bool(Read($Heap, this, F$RegressionTestInput.S.b))));
 }
 
 
@@ -1416,14 +1425,13 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ct
   var $localExc: Ref;
   var $label: int;
 
-    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Box(0));
+    $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Union(0));
+    assume {:breadcrumb 27} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1455,7 +1463,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
+    assume {:breadcrumb 28} true;
     $result := x + 1;
     return;
 }
@@ -1469,30 +1477,31 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);
 implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 {
   var x: int;
-  var __temp_1_int: int;
   var y_int: int;
   var $localExc: Ref;
   var $label: int;
 
     x := x$in;
-    __temp_1_int := 5 / x;
+    assume {:breadcrumb 29} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
     x := 3;
-    y_int := __temp_1_int + 3;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
-    if (x == 3)
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
+    y_int := 3 + 5 / x;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
+    if (x != 3)
     {
     }
     else
     {
     }
 
-    assert (if x == 3 then y_int <= 8 else false);
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
+    assert (if x != 3 then false else !(y_int > 8));
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
     F$RegressionTestInput.Class0.StaticInt := y_int;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
     assert y_int == F$RegressionTestInput.Class0.StaticInt;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
-    return;
 }
 
 
@@ -1510,8 +1519,7 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
-    return;
+    assume {:breadcrumb 30} true;
 }
 
 
@@ -1527,8 +1535,7 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
   var $label: int;
 
     b := b$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
-    return;
+    assume {:breadcrumb 31} true;
 }
 
 
@@ -1544,8 +1551,7 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
   var $label: int;
 
     c := c$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
-    return;
+    assume {:breadcrumb 32} true;
 }
 
 
@@ -1560,7 +1566,7 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
+    assume {:breadcrumb 33} true;
     call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
     if ($Exception != null)
     {
@@ -1583,9 +1589,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assume {:breadcrumb 34} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
     x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
     $result := x$out;
     return;
 }
@@ -1602,11 +1610,14 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assume {:breadcrumb 35} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
     x$out := x$out + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
     F$RegressionTestInput.Class0.StaticInt := x$out;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
     $result := x$out;
     return;
 }
@@ -1624,11 +1635,13 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
+    assume {:breadcrumb 36} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
     x := x + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
     F$RegressionTestInput.Class0.StaticInt := x;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
     $result := x;
     return;
 }
@@ -1646,7 +1659,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
+    assume {:breadcrumb 37} true;
     $result := x;
     return;
 }
@@ -1665,7 +1678,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
   var $label: int;
 
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
+    assume {:breadcrumb 38} true;
     call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);
     if ($Exception != null)
     {
@@ -1687,13 +1700,12 @@ implementation RegressionTestInput.Class0.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 39} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1730,7 +1742,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
+    assume {:breadcrumb 40} true;
     $result := x < y;
     return;
 }
@@ -1748,27 +1760,29 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
   var $label: int;
 
     z := z$in;
-    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
+    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(false));
+    assume {:breadcrumb 41} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
-    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
+    $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Union(z));
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
     if (z)
     {
-        assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
         F$RegressionTestInput.ClassWithBoolTypes.staticB := z;
     }
     else
     {
     }
-
-    return;
 }
 
 
@@ -1783,15 +1797,14 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+    assume {:breadcrumb 42} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
     call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
-    return;
 }
 
 
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index d7848c0c..3069f557 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -56,6 +56,18 @@ function {:builtin "MapImp"} mapimp([Delegate]bool, [Delegate]bool) : [Delegate]
 
 axiom MultisetEmpty == mapconstint(0);
 
+function IsRef(u: Union) : bool;
+
+axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x)));
+
+axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x)));
+
+axiom (forall x: Real :: { Real2Union(x) } Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x)));
+
+axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x)));
+
+axiom (forall x: Ref :: { Struct2Union(x) } Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x)));
+
 function $TypeOfInv(Ref) : Type;
 
 axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);
@@ -71,17 +83,11 @@ implementation {:inline 1} System.Object.GetType(this: Ref) returns ($result: Re
 
 
 
-axiom Box2Int($DefaultBox) == 0;
-
-axiom Box2Bool($DefaultBox) == false;
-
-axiom Box2Ref($DefaultBox) == null;
-
-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x);
+axiom Union2Int($DefaultHeapValue) == 0;
 
-axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x);
+axiom Union2Bool($DefaultHeapValue) == false;
 
-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x);
+axiom Union2Ref($DefaultHeapValue) == null;
 
 function $ThreadDelegate(Ref) : Ref;
 
@@ -107,11 +113,11 @@ implementation {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref
 
 
 
-procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
+procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
 
 
 
-implementation {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
+implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)
 {
     $Exception := null;
     call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
@@ -145,11 +151,11 @@ implementation {:inline 1} System.Threading.Thread.Start(this: Ref)
 
 
 
-procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
+procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 
 
 
-implementation {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
+implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)
 {
     $Exception := null;
     call System.Threading.ThreadStart.Invoke(this);
@@ -180,7 +186,8 @@ implementation {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
     else
     {
         call c := Alloc();
-        assume $Delegate(c) == MultisetPlus($Delegate(a), $Delegate(b));
+        assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b);
+        assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
     }
 }
 
@@ -202,14 +209,15 @@ implementation {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
     {
         c := a;
     }
-    else if (MultisetMinus($Delegate(a), $Delegate(b)) == MultisetEmpty)
+    else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty)
     {
         c := null;
     }
     else
     {
         call c := Alloc();
-        assume $Delegate(c) == MultisetMinus($Delegate(a), $Delegate(b));
+        assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
+        assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0;
     }
 }
 
@@ -222,7 +230,8 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 implementation {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
 {
     call c := Alloc();
-    assume $Delegate(c) == MultisetSingleton(d);
+    assume $RefToDelegate(c) == d;
+    assume $RefToDelegateMultiset(c) == MultisetSingleton(d);
 }
 
 
@@ -249,129 +258,164 @@ implementation System.String.op_Inequality$System.String$System.String(a$in: Ref
 
 
 
-var isControlEnabled: [Ref]bool;
+var $ArrayContents: [Ref][int]Union;
 
-var isControlChecked: [Ref]bool;
+function $ArrayLength(Ref) : int;
 
-procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);
+type {:datatype} Delegate;
 
+type DelegateMultiset = [Delegate]int;
 
+const unique MultisetEmpty: DelegateMultiset;
 
-implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool)
+function {:inline true} MultisetSingleton(x: Delegate) : DelegateMultiset
 {
-    $Exception := null;
-    isControlEnabled[$this] := value$in;
+  MultisetEmpty[x := 1]
 }
 
+function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+{
+  mapadd(x, y)
+}
 
+function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+{
+  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))
+}
 
-procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);
+type Field;
 
+type Union;
 
+const unique $DefaultHeapValue: Union;
 
-implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref)
-{
-  var enabledness: bool;
+type Ref;
 
-    $Exception := null;
-    enabledness := isControlEnabled[$this];
-    $result := Box2Ref(Bool2Box(enabledness));
-}
+const unique null: Ref;
+
+type {:datatype} Type;
 
+type Real;
 
+const unique $DefaultReal: Real;
 
-procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);
+procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref);
 
 
 
-implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref)
+implementation {:inline 1} $BoxFromBool(b: bool) returns (r: Ref)
 {
-  var check: bool;
-
-    $Exception := null;
-    check := Box2Bool(Ref2Box(value$in));
-    isControlChecked[$this] := check;
+    call r := Alloc();
+    assume $BoxedValue(r) == Bool2Union(b);
 }
 
 
 
-procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);
+procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref);
 
 
 
-implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref)
+implementation {:inline 1} $BoxFromInt(i: int) returns (r: Ref)
 {
-  var isChecked: bool;
-
-    $Exception := null;
-    isChecked := isControlChecked[$this];
-    $result := Box2Ref(Bool2Box(isChecked));
+    call r := Alloc();
+    assume $BoxedValue(r) == Int2Union(i);
 }
 
 
 
-var $BoxField: [Ref]Box;
+procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref);
 
-var $ArrayContents: [Ref][int]Box;
 
-function $ArrayLength(Ref) : int;
 
-type {:datatype} Delegate;
+implementation {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref)
+{
+    call rf := Alloc();
+    assume $BoxedValue(rf) == Real2Union(r);
+}
 
-type DelegateMultiset = [Delegate]int;
 
-const unique MultisetEmpty: DelegateMultiset;
 
-function {:inline} MultisetSingleton(x: Delegate) : DelegateMultiset
-{
-  MultisetEmpty[x := 1]
-}
+procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref);
+
 
-function {:inline} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+
+implementation {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref)
 {
-  mapadd(x, y)
+    call r := Alloc();
+    assume $BoxedValue(r) == Struct2Union(s);
 }
 
-function {:inline} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset) : DelegateMultiset
+
+
+procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref);
+
+
+
+implementation {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref)
 {
-  mapiteint(mapgt(x, y), mapsub(x, y), mapconstint(0))
+    if (IsRef(u))
+    {
+        r := Union2Ref(u);
+    }
+    else
+    {
+        call r := Alloc();
+        assume $BoxedValue(r) == u;
+    }
 }
 
-type Field;
 
-type Box;
 
-const unique $DefaultBox: Box;
+function $BoxedValue(r: Ref) : Union;
 
-type Ref;
+function {:inline true} $Unbox2Bool(r: Ref) : bool
+{
+  Union2Bool($BoxedValue(r))
+}
 
-const unique null: Ref;
+function {:inline true} $Unbox2Int(r: Ref) : int
+{
+  Union2Int($BoxedValue(r))
+}
 
-type {:datatype} Type;
+function {:inline true} $Unbox2Real(r: Ref) : Real
+{
+  Union2Real($BoxedValue(r))
+}
 
-type Real;
+function {:inline true} $Unbox2Struct(r: Ref) : Ref
+{
+  Union2Struct($BoxedValue(r))
+}
 
-const unique $DefaultReal: Real;
+function {:inline true} $Unbox2Union(r: Ref) : Union
+{
+  $BoxedValue(r)
+}
 
-function Box2Bool(Box) : bool;
+function Union2Bool(u: Union) : bool;
 
-function Box2Int(Box) : int;
+function Union2Int(u: Union) : int;
 
-function Box2Ref(Box) : Ref;
+function Union2Ref(u: Union) : Ref;
 
-function Box2Real(Box) : Real;
+function Union2Real(u: Union) : Real;
 
-function Bool2Box(bool) : Box;
+function Union2Struct(u: Union) : Ref;
 
-function Int2Box(int) : Box;
+function Bool2Union(boolValue: bool) : Union;
 
-function Ref2Box(Ref) : Box;
+function Int2Union(intValue: int) : Union;
 
-function Real2Box(Real) : Box;
+function Ref2Union(refValue: Ref) : Union;
 
-function {:inline true} Box2Box(b: Box) : Box
+function Real2Union(realValue: Real) : Union;
+
+function Struct2Union(structValue: Ref) : Union;
+
+function {:inline true} Union2Union(u: Union) : Union
 {
-  b
+  u
 }
 
 function Int2Real(int) : Real;
@@ -418,9 +462,11 @@ function $Subtype(Type, Type) : bool;
 
 function $DisjointSubtree(Type, Type) : bool;
 
-function $Delegate(Ref) : DelegateMultiset;
+function $RefToDelegate(Ref) : Delegate;
 
-function {:constructor} $DelegateCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate;
+function $RefToDelegateMultiset(Ref) : DelegateMultiset;
+
+function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type) : Delegate;
 
 var {:thread_local} $Exception: Ref;
 
@@ -500,18 +546,12 @@ implementation RegressionTestInput.StructContainingStruct.ReturnCopy$RegressionT
 {
   var s: Ref;
   var t_Ref: Ref;
-  var $tmp0: Ref;
   var $localExc: Ref;
   var $label: int;
 
     s := s$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 206} true;
-    call $tmp0 := Alloc();
-    call RegressionTestInput.StructContainingStruct.#default_ctor($tmp0);
-    assume $DynamicType($tmp0) == T$RegressionTestInput.StructContainingStruct();
-    t_Ref := $tmp0;
+    assume {:breadcrumb 43} true;
     call t_Ref := RegressionTestInput.StructContainingStruct.#copy_ctor(s);
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 208} true;
     $result := t_Ref;
     return;
 }
@@ -537,15 +577,14 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this:
   var $label: int;
 
     d := d$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+    assume {:breadcrumb 44} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
     call System.Console.WriteLine$System.Double(d);
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
-    return;
 }
 
 
@@ -561,15 +600,14 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi
   var $label: int;
 
     o := o$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
-    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real($BoxField[o]));
+    assume {:breadcrumb 45} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+    call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, $Unbox2Real(o));
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
-    return;
 }
 
 
@@ -589,40 +627,40 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
+    assume {:breadcrumb 46} true;
     d_Real := $real_literal_3_0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
     d2_Real := $real_literal_4_0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
     call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d_Real, d2_Real));
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
-    return;
 }
 
 
@@ -640,13 +678,12 @@ implementation RegressionTestInput.RealNumbers.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 47} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -678,10 +715,10 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this:
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+    assume {:breadcrumb 48} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
-    return;
 }
 
 
@@ -697,13 +734,12 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($th
 
     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;
     F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0;
+    assume {:breadcrumb 49} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -734,24 +770,18 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res
 {
   var s_Ref: Ref;
   var $tmp0: Ref;
-  var $tmp1: Ref;
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 50} true;
     call $tmp0 := Alloc();
     call RegressionTestInput.S.#default_ctor($tmp0);
     assume $DynamicType($tmp0) == T$RegressionTestInput.S();
     s_Ref := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
-    call $tmp1 := Alloc();
-    call RegressionTestInput.S.#default_ctor($tmp1);
-    assume $DynamicType($tmp1) == T$RegressionTestInput.S();
-    s_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
     assert F$RegressionTestInput.S.x[s_Ref] == 0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
     assert !F$RegressionTestInput.S.b[s_Ref];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
     $result := s_Ref;
     return;
 }
@@ -769,11 +799,12 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes
   var $label: int;
 
     s := s$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+    assume {:breadcrumb 51} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
     F$RegressionTestInput.S.x[s] := 3;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
     assert F$RegressionTestInput.S.x[s] == 3;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
     $result := s;
     return;
 }
@@ -789,13 +820,12 @@ implementation RegressionTestInput.CreateStruct.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 52} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -831,26 +861,19 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
+    assume {:breadcrumb 53} true;
     call $tmp0 := Alloc();
     assume $ArrayLength($tmp0) == 1 * 5;
     s_Ref := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
-    $ArrayContents := $ArrayContents[s_Ref := $ArrayContents[s_Ref][0 := Int2Box(2)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
-    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
+    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
     call $tmp1 := Alloc();
     assume $ArrayLength($tmp1) == 1 * 4;
     t_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
-    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
-    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
-    assert Box2Int($ArrayContents[s_Ref][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 95} true;
-    return;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
+    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 94} true;
+    assert Union2Int($ArrayContents[s_Ref][0]) == 2;
 }
 
 
@@ -867,26 +890,24 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
+    assume {:breadcrumb 54} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
     call $tmp0 := Alloc();
     assume $ArrayLength($tmp0) == 1 * 5;
     F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
-    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
-    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
+    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Union(2)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
+    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
     call $tmp1 := Alloc();
     assume $ArrayLength($tmp1) == 1 * 4;
     t_Ref := $tmp1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
-    $ArrayContents := $ArrayContents[t_Ref := $ArrayContents[t_Ref][0 := Int2Box(1)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
-    assert Box2Int($ArrayContents[t_Ref][0]) == 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
-    assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
-    return;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
+    assert Union2Int($ArrayContents[t_Ref][0]) == 1;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
+    assert Union2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
 }
 
 
@@ -904,16 +925,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this:
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
-    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x := Int2Box(42)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
-    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Box(43)]];
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
+    assume {:breadcrumb 55} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
+    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x := Int2Union(42)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
+    $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][x + 1 := Int2Union(43)]];
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
     _loc0_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
     _loc1_Ref := F$RegressionTestInput.ClassWithArrayTypes.a[$this];
-    assert Box2Int($ArrayContents[_loc0_Ref][x + 1]) == Box2Int($ArrayContents[_loc1_Ref][x]) + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
-    return;
+    assert Union2Int($ArrayContents[_loc0_Ref][x + 1]) == Union2Int($ArrayContents[_loc1_Ref][x]) + 1;
 }
 
 
@@ -929,24 +951,23 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($
   var $label: int;
 
     xs := xs$in;
-    if (xs != null)
+    assume {:breadcrumb 56} true;
+    if (!(xs != null))
     {
     }
     else
     {
     }
 
-    if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
+    if ((if !(xs != null) then true else !($ArrayLength(xs) > 0)) == 0)
     {
-        assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
-        $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
+        $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this] := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.a[$this]][0 := Int2Union(Union2Int($ArrayContents[xs][0]))]];
     }
     else
     {
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 123} true;
-    return;
 }
 
 
@@ -961,13 +982,12 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref)
   var $label: int;
 
     F$RegressionTestInput.ClassWithArrayTypes.a[$this] := null;
+    assume {:breadcrumb 57} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -999,13 +1019,12 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#
   var $label: int;
 
     F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x[$this] := 0;
+    assume {:breadcrumb 58} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1037,7 +1056,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
+    assume {:breadcrumb 59} true;
     $result := BitwiseAnd(x, y);
     return;
 }
@@ -1057,7 +1076,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
+    assume {:breadcrumb 60} true;
     $result := BitwiseOr(x, y);
     return;
 }
@@ -1077,7 +1096,7 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
+    assume {:breadcrumb 61} true;
     $result := BitwiseExclusiveOr(x, y);
     return;
 }
@@ -1095,7 +1114,7 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
+    assume {:breadcrumb 62} true;
     $result := BitwiseNegation(x);
     return;
 }
@@ -1111,13 +1130,12 @@ implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 63} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1157,13 +1175,12 @@ implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 64} true;
     call System.Attribute.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1192,10 +1209,9 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
+    assume {:breadcrumb 65} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 156} true;
     x$out := x$out + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 157} true;
-    return;
 }
 
 
@@ -1209,13 +1225,12 @@ implementation RegressionTestInput.RefParameters.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 66} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1243,13 +1258,12 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 67} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1267,13 +1281,12 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 68} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1286,55 +1299,51 @@ procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref,
 
 
 
-procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Box);
+procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Union);
 
 
 
 implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int)
 {
   var x: int;
-  var CS$0$0000_Box: Box;
-  var $tmp0: Ref;
-  var __temp_2_Box: Box;
-  var __temp_3_Box: Box;
-  var $tmp1: Box;
-  var $tmp2: Box;
-  var y_Box: Box;
+  var CS$0$0000_Union: Union;
+  var $tmp0: Union;
+  var $tmp1: Union;
+  var $tmp2: Ref;
+  var y_Union: Union;
   var $localExc: Ref;
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
+    assume {:breadcrumb 69} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
-    CS$0$0000_Box := $DefaultBox;
-    call $tmp0 := Alloc();
-    $BoxField[$tmp0] := Box2Box(CS$0$0000_Box);
-    if ($tmp0 != null)
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    CS$0$0000_Union := $DefaultHeapValue;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;
+    call $tmp2 := $BoxFromUnion(CS$0$0000_Union);
+    if ($tmp2 != null)
     {
-        CS$0$0000_Box := $DefaultBox;
-        __temp_2_Box := CS$0$0000_Box;
     }
     else
     {
-        call $tmp2 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
-        $tmp1 := Box2Box($tmp2);
+        call $tmp1 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
+        $tmp0 := Union2Union($tmp1);
         if ($Exception != null)
         {
             return;
         }
-
-        __temp_3_Box := $tmp1;
-        __temp_2_Box := __temp_3_Box;
     }
 
-    y_Box := __temp_2_Box;
-    return;
+    y_Union := (if $tmp2 != null then $DefaultHeapValue else $tmp0);
 }
 
 
@@ -1403,13 +1412,12 @@ implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ct
   var $label: int;
 
     F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;
+    assume {:breadcrumb 70} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1441,7 +1449,7 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 18} true;
+    assume {:breadcrumb 71} true;
     $result := x + 1;
     return;
 }
@@ -1455,30 +1463,31 @@ procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int);
 implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int)
 {
   var x: int;
-  var __temp_1_int: int;
   var y_int: int;
   var $localExc: Ref;
   var $label: int;
 
     x := x$in;
-    __temp_1_int := 5 / x;
+    assume {:breadcrumb 72} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
     x := 3;
-    y_int := __temp_1_int + 3;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
-    if (x == 3)
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 21} true;
+    y_int := 3 + 5 / x;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
+    if (x != 3)
     {
     }
     else
     {
     }
 
-    assert (if x == 3 then y_int <= 8 else false);
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
+    assert (if x != 3 then false else !(y_int > 8));
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
     F$RegressionTestInput.Class0.StaticInt := y_int;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
     assert y_int == F$RegressionTestInput.Class0.StaticInt;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
-    return;
 }
 
 
@@ -1496,8 +1505,7 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 28} true;
-    return;
+    assume {:breadcrumb 73} true;
 }
 
 
@@ -1513,8 +1521,7 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo
   var $label: int;
 
     b := b$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 29} true;
-    return;
+    assume {:breadcrumb 74} true;
 }
 
 
@@ -1530,8 +1537,7 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re
   var $label: int;
 
     c := c$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 30} true;
-    return;
+    assume {:breadcrumb 75} true;
 }
 
 
@@ -1546,7 +1552,7 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result:
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
+    assume {:breadcrumb 76} true;
     call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
     if ($Exception != null)
     {
@@ -1569,9 +1575,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assume {:breadcrumb 77} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
     x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
     $result := x$out;
     return;
 }
@@ -1588,11 +1596,14 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i
   var $label: int;
 
     x$out := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assume {:breadcrumb 78} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
     x$out := x$out + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
     F$RegressionTestInput.Class0.StaticInt := x$out;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
     $result := x$out;
     return;
 }
@@ -1610,11 +1621,13 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
+    assume {:breadcrumb 79} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
     x := x + 1;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
     F$RegressionTestInput.Class0.StaticInt := x;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
     $result := x;
     return;
 }
@@ -1632,7 +1645,7 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho
   var $label: int;
 
     x := x$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 56} true;
+    assume {:breadcrumb 80} true;
     $result := x;
     return;
 }
@@ -1651,7 +1664,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re
   var $label: int;
 
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
+    assume {:breadcrumb 81} true;
     call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);
     if ($Exception != null)
     {
@@ -1673,13 +1686,12 @@ implementation RegressionTestInput.Class0.#ctor($this: Ref)
   var $localExc: Ref;
   var $label: int;
 
+    assume {:breadcrumb 82} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
-
-    return;
 }
 
 
@@ -1716,7 +1728,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3
 
     x := x$in;
     y := y$in;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 70} true;
+    assume {:breadcrumb 83} true;
     $result := x < y;
     return;
 }
@@ -1735,26 +1747,28 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this
 
     z := z$in;
     F$RegressionTestInput.ClassWithBoolTypes.b[$this] := false;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
+    assume {:breadcrumb 84} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
     call System.Object.#ctor($this);
     if ($Exception != null)
     {
         return;
     }
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
     F$RegressionTestInput.ClassWithBoolTypes.b[$this] := z;
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
     if (z)
     {
-        assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+        assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
+        assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
         F$RegressionTestInput.ClassWithBoolTypes.staticB := z;
     }
     else
     {
     }
-
-    return;
 }
 
 
@@ -1769,15 +1783,14 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main()
   var $localExc: Ref;
   var $label: int;
 
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+    assume {:breadcrumb 85} true;
+    assert {:first} {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
+    assert {:sourceFile "C:\dev\Boogie\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
     call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
     if ($Exception != null)
     {
         return;
     }
-
-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
-    return;
 }
author	Unknown <afd@afd-THINK.doc.ic.ac.uk>	2012-04-10 09:30:38 +0100
committer	Unknown <afd@afd-THINK.doc.ic.ac.uk>	2012-04-10 09:30:38 +0100
commit	d9ac9b3975fb54cce4dec82316e1852ec9bb6e68 (patch)
tree	29187ece9655aa93ce1a31d09b3f1f64e56a904d
parent	388caecdf98ec17712ceb11467546c3ea20674a4 (diff)
parent	5db02f7f6576b5d6814f8a5c4c7291f845ac557a (diff)