diff options
author | Rustan Leino <unknown> | 2014-01-08 18:43:35 -0800 |
---|---|---|
committer | Rustan Leino <unknown> | 2014-01-08 18:43:35 -0800 |
commit | dd82ee5e33d25f6a5570da2ad6ab650ce6dc3164 (patch) | |
tree | 2a8fac681bdee8de2db7303ad06c3ab3c354470a /Source/Dafny/DafnyAst.cs | |
parent | 709f460287dac7b6646fe770d3e01ed7cf26c9eb (diff) |
Fixed build break: two contract problems
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 5525e879..bcf1e48a 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3983,7 +3983,7 @@ namespace Microsoft.Dafny { public static Expression CreateNot(IToken tok, Expression e) {
Contract.Requires(tok != null);
- Contract.Requires(e.Type == Type.Bool);
+ Contract.Requires(e.Type is BoolType);
var un = new UnaryExpr(tok, UnaryExpr.Opcode.Not, e);
un.Type = Type.Bool; // resolve here
return un;
@@ -4074,8 +4074,8 @@ namespace Microsoft.Dafny { /// </summary>
public static MatchCaseExpr CreateMatchCase(MatchCaseExpr old_case, Expression new_body) {
Contract.Requires(old_case != null);
- Contract.Requires(new_body != null);
- Contract.Ensures(Contract.Result<Expression>() != null);
+ Contract.Requires(new_body != null);
+ Contract.Ensures(Contract.Result<MatchCaseExpr>() != null);
ResolvedCloner cloner = new ResolvedCloner();
var newVars = old_case.Arguments.ConvertAll(cloner.CloneBoundVar);
|