1 files changed, 0 insertions, 59 deletions
diff --git a/Test/dafny0/ReturnTests.dfy b/Test/dafny0/ReturnTests.dfy
deleted file mode 100644
index ee60bc72..00000000
--- a/Test/dafny0/ReturnTests.dfy
+++ /dev/null
@@ -1,59 +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; // implict return still works.
-}
-
-method testing1() returns (a: int, b: set<int>)
-{
-   return 1, {1, 2, 3}; // type checking
-}
-method testing2() returns (a: int, b: int)
-   ensures a == 1 && b == 2;
-{
-   a, b := 2, 1;
-   return b, a; // test of parallel assignment.
-}
-method testing3() returns (a: int, b: int)
-   ensures a == 1 && b == 2;
-{
-   a, b := 2, 1; // these are wrong
-   if (true)
-   {
-      var a, b := 3, 4;
-      return 1, 2;// return updates non-shadowed, formal parameters correctly
-   }
-}
-
-method testing4(nnn: N) returns (n: N)
-   requires nnn != null;
-{
-   return new N.safe(nnn); // only modifies 'this', which is the fresh N
-}
-
-method testing5() returns (r: int)
-   ensures r == 2;
-{
-   r := 2;
-   return; // sanity check.
-}
-\ No newline at end of file