diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9f3f474b..4402e5b1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4082,7 +4082,6 @@ namespace Microsoft.Dafny { } else if(operandType is MapType) {
return BinaryExpr.ResolvedOpcode.MapDisjoint;
} else {
- Contract.Assert(operandType is SetType);
return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
@@ -4161,7 +4160,6 @@ namespace Microsoft.Dafny { } else if (operandType is MapType) {
return BinaryExpr.ResolvedOpcode.InMap;
} else {
- Contract.Assert(operandType is SeqType);
return BinaryExpr.ResolvedOpcode.InSeq;
}
case BinaryExpr.Opcode.NotIn:
@@ -4172,7 +4170,6 @@ namespace Microsoft.Dafny { } else if (operandType is MapType) {
return BinaryExpr.ResolvedOpcode.NotInMap;
} else {
- Contract.Assert(operandType is SeqType);
return BinaryExpr.ResolvedOpcode.NotInSeq;
}
case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
|