1 files changed, 0 insertions, 45 deletions
diff --git a/Chalice/tests/examples/ProdConsChannel.chalice b/Chalice/tests/examples/ProdConsChannel.chalice
deleted file mode 100644
index abac4f5c..00000000
--- a/Chalice/tests/examples/ProdConsChannel.chalice
+++ /dev/null
@@ -1,45 +0,0 @@
-class Cell {
-  var val: int
-}
-
-channel Ch(c: Cell) where
-  c != null ==> acc(c.val) && 0 <= c.val && credit(this)
-
-class Program {
-  method Main() {
-    var ch := new Ch
-    fork tk0 := Producer(ch)
-    fork tk1 := Consumer(ch)
-    join tk0
-    join tk1
-  }
-  method Producer(ch: Ch)
-    requires ch != null
-    ensures credit(ch)
-  {
-    var i := 0
-    while (i < 25)
-    {
-      var x := i*i
-      var c := new Cell { val := x }
-      send ch(c)
-      i := i + 1
-    }
-    send ch(null)
-  }
-  method Consumer(ch: Ch)
-    requires rd(ch.mu) && waitlevel << ch.mu
-    requires credit(ch)
-    ensures rd(ch.mu)
-  {
-    var c: Cell
-    receive c := ch
-    while (c != null)
-      invariant rd(ch.mu) && waitlevel << ch.mu
-      invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch)
-    {
-      var i := c.val
-      receive c := ch
-    }
-  }
-}