1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
new file mode 100644
index 00000000..72e249d8
--- /dev/null
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -0,0 +1,22 @@
+function bad(n: nat): nat
+  decreases n;
+{
+  bad(n+1)
+}
+ghost method go_bad()
+  ensures bad(0)==0;
+{
+}
+
+datatype Nat = Zero | Succ(tail: Nat)
+predicate ThProperty(step: nat, t: Nat, r: nat)
+{
+  match t
+  case Zero => true
+  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+}
+ghost method test_ThProperty()
+  ensures ThProperty(10, Succ(Zero), 0);
+{
+//  assert ThProperty(9, Zero, 0);
+}
+\ No newline at end of file