2 files changed, 24 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 09936f86..06f4e9e9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2067,7 +2067,7 @@ Dafny program verifier finished with 1 verified, 4 errors
 
 -------------------- Computations.dfy --------------------
 
-Dafny program verifier finished with 49 verified, 0 errors
+Dafny program verifier finished with 58 verified, 0 errors
 
 -------------------- ComputationsNeg.dfy --------------------
 ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index d3c42af5..0481fe96 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -155,8 +155,29 @@ function power(b: int, n: nat): int
 {
   if (n==0) then 1 else b*power(b, n-1)
 }
-
 ghost method test_power()
   ensures power(power(2, 3), 1+power(2, 2))==32768;
 {
-}
-\ No newline at end of file
+}
+
+function fib(n: nat): nat
+{
+  if (n<2) then n else fib(n-1)+fib(n-2)
+}
+ghost method test_fib()
+  ensures fib(12)==144;
+{
+}
+ghost method test_fib1(k: nat)
+  ensures k==12 ==> fib(k)==144;
+{
+}
+ghost method test_fib2(k: nat)
+  ensures 12<=k && k<=12 ==> fib(k)==144;
+{
+}
+ghost method test_fib3(k: nat, m: nat)
+{
+  var y := 12;
+  assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
+}