summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasure.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
-rw-r--r--Source/VCExpr/TypeErasure.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 9614f9f8..4111c9df 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1362,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure {
List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, newPolarity);
Type/*!*/ oldType = node[0].Type;
if (AxBuilder.UnchangedType(oldType) &&
- node.All(e => e.Type.Equals(oldType)))
+ node.Skip(1).All(e => e.Type.Equals(oldType)))
return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
else
return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));