1 files changed, 0 insertions, 58 deletions
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
deleted file mode 100644
index f1fc7d48..00000000
--- a/Test/dafny0/AdvancedLHS.dfy
+++ /dev/null
@@ -1,58 +0,0 @@
-class C {
-  var x: C;
-
-  method M(S: set<C>, a: array<C>, b: array2<C>)
-    requires S != {};
-    modifies this, a, b;
-  {
-    x := new C;
-    x := new C.Init();
-    x := *;
-    x := choose S;
-
-    // test evaluation order
-    var c := x;
-    x := null;
-    x := new C.InitOther(x);  // since the parameter is evaluated before the LHS is set, the precondition is met
-    assert x != c;
-
-    // test evaluation order and modification
-    if (*) {
-      var k := this.x;
-      var kx := this.x.x;
-      this.x.x := new C.InitAndMutate(this);
-      assert this.x == null;
-      assert this.x != k;
-      assert k.x != kx;  // because it was set to a new object
-      assert fresh(k.x);
-    } else {
-      var k := this.x;
-      var kx := this.x.x;
-      this.x.x := new C.InitAndMutate(this);
-      var t := this.x.x;  // error: null dereference (because InitAndMutate set this.x to null)
-    }
-
-    if (a != null && 10 <= a.Length) {
-      a[2] := new C;
-      a[3] := *;
-    }
-    if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {
-      b[2,14] := new C;
-      b[3,11] := *;
-    }
-  }
-
-  method Init() { }
-  method InitOther(c: C)
-    requires c == null;
-  {
-    var d := new int[if c == null then 10 else -3];  // run-time error if c were non-null, but it ain't
-  }
-  method InitAndMutate(c: C)
-    requires c != null;
-    modifies c;
-    ensures c.x == null;
-  {
-    c.x := null;
-  }
-}