diff options
| author |  wuestholz <unknown> | 2013-07-23 10:28:04 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-23 10:28:04 -0700 |
| commit | 34ff60de0ab0a05c85e6af50ed6d1a93805e040b (patch) | |
| tree | 5454c3e0fe828a456facba4e5a86607ee27ca9e7 /Source/VCExpr/TypeErasure.cs | |
| parent | 4be2ab852c127558c04119958fd0b462ff2e6493 (diff) | |
Did some refactoring.
Diffstat (limited to 'Source/VCExpr/TypeErasure.cs')
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 2 |
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));
|