Bug fix: check that assign-such-that constraint is of type boolean

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);