1 files changed, 11 insertions, 0 deletions
diff --git a/float_test.bpl b/float_test.bpl
new file mode 100644
index 00000000..22e436a1
--- /dev/null
+++ b/float_test.bpl
@@ -0,0 +1,11 @@
+procedure F(n: int) returns (r: int)
+  ensures 100 < n ==> r == n - 10;  // This postcondition is easy to check by hand
+  ensures n <= 100 ==> r == 91;     // Do you believe this one is true?
+{
+  if (100 < n) {
+    r := n - 10;
+  } else {
+    call r := F(n + 11);
+    call r := F(r);
+  }
+}
+\ No newline at end of file