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

1 files changed, 15 insertions, 0 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 900c7459..1354e533 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1373,3 +1373,18 @@ module NonTypeVariableNames {
     Y := k;  // error: module name used as variable

   }

 }

+

+// ------------------- assign-such-that and let-such-that -------------------

+

+module SuchThat {

+  method M() {

+    var x: int;

+    x :| 5 + 7;  // error: constraint should be boolean

+    x :| x;  // error: constraint should be boolean

+    var y :| 4;  // error: constraint should be boolean

+  }

+  function F(): int {

+    var w :| 6 + 8;  // error: constraint should be boolean

+    w

+  }

+}