1 files changed, 0 insertions, 71 deletions
diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
deleted file mode 100644
index 3bd2bf43..00000000
--- a/Test/VSI-Benchmarks/b1.dfy
+++ /dev/null
@@ -1,71 +0,0 @@
-// Spec# and Boogie and Chalice:  The program will be
-// the same, except that these languages do not check
-// for any kind of termination.  Also, in Spec#, there
-// is an issue of potential overflows.
-
-// Benchmark1
-
-method Add(x: int, y: int) returns (r: int)
-  ensures r == x+y;
-{
-  r := x;
-  if (y < 0) {
-    var n := y;
-    while (n != 0)
-      invariant r == x+y-n && 0 <= -n;
-    {
-      r := r - 1;
-      n := n + 1;
-    }
-  } else {
-    var n := y;
-    while (n != 0)
-      invariant r == x+y-n && 0 <= n;
-    {
-      r := r + 1;
-      n := n - 1;
-    }
-  }
-}
-
-method Mul(x: int, y: int) returns (r: int)
-  ensures r == x*y;
-  decreases x < 0, x;
-{
-  if (x == 0) {
-    r := 0;
-  } else if (x < 0) {
-    r := Mul(-x, y);
-    r := -r;
-  } else {
-    r := Mul(x-1, y);
-    r := Add(r, y);
-  }
-}
-
-// ---------------------------
-
-method Main() {
-  TestAdd(3, 180);
-  TestAdd(3, -180);
-  TestAdd(0, 1);
-
-  TestMul(3, 180);
-  TestMul(3, -180);
-  TestMul(180, 3);
-  TestMul(-180, 3);
-  TestMul(0, 1);
-  TestMul(1, 0);
-}
-
-method TestAdd(x: int, y: int) {
-  print x, " + ", y, " = ";
-  var z := Add(x, y);
-  print z, "\n";
-}
-
-method TestMul(x: int, y: int) {
-  print x, " * ", y, " = ";
-  var z := Mul(x, y);
-  print z, "\n";
-}