Separate out the concepts of boxing

(i.e., CLR's creating a heap cell and
putting a value into it) from the concept
of the "union" type that all Boogie types
are a subtype of.

1 files changed, 1 insertions, 1 deletions

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4499f11e..bc4e7524 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -144,7 +144,7 @@ namespace BytecodeTranslator {
           if (TypeHelper.TypesAreEquivalent(c, type.PlatformType.SystemValueType)) continue;

           return CciTypeToBoogie(c);

         }

-        return heap.BoxType;

+        return heap.UnionType;

       } else

         return heap.RefType;

     }