1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/BadFunction.dfy b/Test/dafny0/BadFunction.dfy
new file mode 100644
index 00000000..3affaa80
--- /dev/null
+++ b/Test/dafny0/BadFunction.dfy
@@ -0,0 +1,13 @@
+// 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
+}