1 files changed, 0 insertions, 43 deletions
diff --git a/Chalice/tests/refinements/DuplicatesVideo.chalice b/Chalice/tests/refinements/DuplicatesVideo.chalice
deleted file mode 100644
index 3886cb78..00000000
--- a/Chalice/tests/refinements/DuplicatesVideo.chalice
+++ /dev/null
@@ -1,43 +0,0 @@
-class Duplicates0 {
-  method Find(s: seq<int>) returns (b: bool)
-    requires forall i in s :: i in [0..100];
-  {
-    b := exists i in [0..|s|] :: s[i] in s[..i];
-  }
-}
-
-class Duplicates1 refines Duplicates0 {
-  refines Find(s: seq<int>) returns (b: bool)
-  {
-    var n := 0;
-    b := false;
-    while (n < |s|)
-      invariant 0 <= n && n <= |s|;
-      invariant b <==> exists i in [0..n] :: s[i] in s[..i];
-    {
-      var c := s[n] in s[..n];
-      b := b || c;
-      n := n + 1;
-    }
-  }
-}
-
-class Duplicates2 refines Duplicates1 {
-  transforms Find(s: seq<int>) returns (b: bool)
-  {
-    _;
-    // bitset has length 100, initially all false
-    var bitset:seq<bool> [|bitset| == 100 && true !in bitset ];
-    while
-      invariant |bitset| == 100;
-      invariant forall i in [0..n] :: bitset[ s[i] ];
-      invariant forall j in [0..100] :: bitset[j] ==> j in s[..n];
-    {
-      replaces c by {
-        var c: bool := bitset[ s[n] ];
-      }
-      bitset := bitset[..s[n] ] ++ [true] ++ bitset[ s[n] + 1 ..];
-      _;
-    }
-  }
-}
-\ No newline at end of file