diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e977dbd5..a58d6e6c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6100,6 +6100,9 @@ namespace Microsoft.Dafny s.IsGhost = s.Lhss.TrueForAll(AssignStmt.LhsIsToGhost);
var ec = ErrorCount;
ResolveExpression(s.Expr, new ResolveOpts(codeContext, true, specContextOnly));
+ if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
+ Error(s.Expr, "type of RHS of assign-such-that statement must be boolean (got {0})", s.Expr.Type);
+ }
if (ec == ErrorCount && !s.IsGhost && s.AssumeToken == null && !specContextOnly) {
CheckIsNonGhost(s.Expr);
|