1 files changed, 0 insertions, 13 deletions
diff --git a/Test/dafny0/BadFunction.dfy b/Test/dafny0/BadFunction.dfy
deleted file mode 100644
index 3affaa80..00000000
--- a/Test/dafny0/BadFunction.dfy
+++ /dev/null
@@ -1,13 +0,0 @@
-// The following function gives rise to an inconsistent axiom, except
-// for its CanUseFunctionDefs antecedent, which saves the day.
-function F(x: int): int
-  decreases x;
-{
-  F(x) + 1  // error: does not decrease termination metric
-}
-
-method M()
-{
-  assert F(5) == 0;  // no error is generated here, because of the inconsistent axiom
-  assert false;  // ditto
-}