1 files changed, 0 insertions, 97 deletions
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
deleted file mode 100644
index b6ef0d68..00000000
--- a/Test/dafny0/TypeAntecedents.dfy
+++ /dev/null
@@ -1,97 +0,0 @@
-// -------- This is an example of what was once logically (although not trigger-ly) unsound ---
-
-datatype Wrapper<T> = Wrap(T);
-datatype Unit = It;
-datatype Color = Yellow | Blue;
-
-function F(a: Wrapper<Unit>): bool
-  ensures a == Wrapper.Wrap(Unit.It);
-{
-  match a
-  case Wrap(u) => G(u)
-}
-
-function G(u: Unit): bool
-  ensures u == Unit.It;
-{
-  match u
-  case It => true
-}
-
-method BadLemma(c0: Color, c1: Color)
-  ensures c0 == c1;
-{
-  var w0 := Wrapper.Wrap(c0);
-  var w1 := Wrapper.Wrap(c1);
-
-  // Manually, add the following assertions in Boogie.  (These would
-  // be ill-typed in Dafny.)
-  //     assert _default.F($Heap, this, w#06);
-  //     assert _default.F($Heap, this, w#17);
-
-  assert w0 == w1;  // this would be bad news (it should be reported as an error)
-}
-
-method Main() {
-  BadLemma(Color.Yellow, Color.Blue);
-  assert false;  // this shows how things can really go wrong if BadLemma verified successfully
-}
-
-// ---------------
-
-class MyClass {
-  var x: int;
-  // The function axiom has "DType(this) == class.MyClass" in its antecedent.  Hence, it
-  // is possible to prove the various asserts below only if the receiver is known by the
-  // verifier to be of type MyClass.
-  function H(): int { 5 }
-}
-
-datatype List =  Nil | Cons(MyClass, List);
-
-method M(list: List, S: set<MyClass>) returns (ret: int)
-  modifies S;
-  ensures ret == 7;
-{  // error: postcondition violation (this postcondition tests that control does flow to the end)
-  match (list) {
-    case Nil =>
-    case Cons(r,tail) =>
-      if (r != null) {
-        ghost var h := r.H();
-        assert h == 5;
-      } else {
-        assert false;  // error
-      }
-  }
-  var k := N();
-  assert k.H() == 5;
-  ghost var l := NF();
-  assert l != null ==> l.H() == 5;
-
-  parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }
-  parallel (s | s != null && s in S) {
-    s.x := 0;
-  }
-
-  assert (forall t: MyClass :: t == null || t.H() == 5);
-  // note, the definedness problem in the next line sits inside an unreachable branch
-  assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));
-
-  assert TakesADatatype(List.Nil) == 12;
-  assert TakesADatatype(List.Cons(null, List.Nil)) == 12;
-  assert AlsoTakesADatatype(GenData.Pair(false, true)) == 17;
-}
-
-method N() returns (k: MyClass)
-  ensures k != null;
-{
-  k := new MyClass;
-}
-var a: MyClass;
-function NF(): MyClass reads this; { a }
-
-function TakesADatatype(a: List): int { 12 }
-
-datatype GenData<T> = Pair(T, T);
-
-function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }