1 files changed, 0 insertions, 42 deletions
diff --git a/Test/dafny0/ReturnErrors.dfy b/Test/dafny0/ReturnErrors.dfy
deleted file mode 100644
index 7f1c2948..00000000
--- a/Test/dafny0/ReturnErrors.dfy
+++ /dev/null
@@ -1,42 +0,0 @@
-
-class N
-{
-   var i: int;
-   method newN(n: N)
-      requires n != null;
-      modifies this, n;
-   {
-      n.i := 1;
-      i := 1;
-   }
-   method safe(n: N)
-      requires n != null;
-      modifies this;
-   {
-      i := n.i;
-   }
-}
-
-method m(v: int, n: N) returns (r: int)
-   modifies n;
-   ensures r == v;
-{
-   r := v;
-}
-method testing1() returns (s: int)
-   ensures s == 3;
-{
-   var n := new N;
-   return m(3, n); // ERROR: methods disallowed.
-}
-method testing2() returns (s: int, b: int)
-   ensures s == 3;
-{
-   var n := new N;
-   return m(3, n), 2; // ERROR: methods disallowed.
-}
-
-method testing3() returns (n: N)
-{
-   return new N.newN(n); // ERROR: disallowed, as newN() modifies n
-}
-\ No newline at end of file