Merge

1 files changed, 0 insertions, 11 deletions

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 87a984a3..7fca7199 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -240,14 +240,3 @@ method notQuiteSwap3(c: CC, d: CC)
   c.x, d.x := 4, c.y;

   c.x, c.y := 3, c.y;

 }

-

-method M() returns (a: int, b: int) {

-  return 4, 6;

-}

-method otherChecks()

-{

-  var x: int, y: int;

-  x, y :| x + y == 5; // fine

-  x, x :| x + y == 5; // BAD, must give different variables.

-  //x, x := M(); // <-- this is caught early, so it suppresses other errors.

-}
\ No newline at end of file