summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--BCT/BytecodeTranslator/Sink.cs3
1 files changed, 1 insertions, 2 deletions
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 2bf3b7d3..74dd39c9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -114,10 +114,9 @@ namespace BytecodeTranslator {
else if (type.ResolvedType.IsStruct)
return heap.StructType;
else if (type.IsEnum) {
- return CciTypeToBoogie(type.ResolvedType.UnderlyingType);
+ return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
} else
return heap.RefType;
- //return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type
}
/// <summary>