1 files changed, 0 insertions, 59 deletions
diff --git a/Chalice/tests/general-tests/quantifiers.chalice b/Chalice/tests/general-tests/quantifiers.chalice
deleted file mode 100644
index 7377ca3f..00000000
--- a/Chalice/tests/general-tests/quantifiers.chalice
+++ /dev/null
@@ -1,59 +0,0 @@
-class A {
-  var f: int;
-}
-
-class Quantifiers {  
-  var bamboo: seq<A>;
-
-  method test1(a: seq<int>, b: int) 
-    requires b in a;
-    requires b > 0;
-  {
-    assert exists j in a :: true && j > 0;
-    assert exists j:int :: 0 <= j && j < |a| && a[j] > 0;
-    assert forall j in a :: exists k in a :: k > 0;
-  }
-
-  method test2(a: seq<A>)
-    requires rd(a[*].*);
-    requires |a| > 0;
-    requires forall i in a :: i != null && i.f > 0;
-  {
-    assert a[0].f > 0;
-    assert forall j: A :: j in a && j != null ==> j.f > 0;
-    assert exists j: A :: j in a && j != null && j.f > 0;
-  }
-
-  method test3(a: seq<A>)
-    requires |a| > 0;
-    requires acc(a[*].f);
-  {
-    var c := new A;
-    assert c != a[0];
-  }
-}
-
-class Functions {
-  var x: int;
-  var y: int;
-
-  function test1(): int
-    requires acc(this.*);
-  {
-    x + y
-  }
-
-  function test2(): int
-    requires acc(x) && acc(y);
-  { 
-    x + y
-  }
-
-  function test3(a: seq<A>): int
-    requires acc(a[*].f);
-    requires forall x in a :: x != null;
-    requires forall i,j in [0..|a|] :: i != j ==> a[i] != a[j];
-  {
-    |a| == 0 ? 0 : a[0].f + test3(a[1..])
-  }
-}