More thoroughly check for nested assume statements during compilation

1 files changed, 24 insertions, 0 deletions

diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy
index 7d21933a..205b2296 100644
--- a/Test/dafny0/CompilationErrors.dfy
+++ b/Test/dafny0/CompilationErrors.dfy
@@ -12,3 +12,27 @@ ghost var g: int;
 

 function F(): int  // compile error: body-less ghost function

 function method H(): int  // compile error: body-less function method

+

+lemma Lemma() {

+  assume false;  // compile error: assume

+}

+ghost method GMethod() {

+  assume false;  // compile error: assume

+}

+

+function MyFunction(): int

+{

+  assume false;  // compile error: assume

+  6

+}

+

+function MyCalcFunction(): int

+{

+  calc <= {

+    2;

+    6;

+    { assume true; }  // compile error: assume

+    10;

+  }

+  12

+}