1 files changed, 3 insertions, 9 deletions
diff --git a/float_test.bpl b/float_test.bpl
index 22e436a1..ebd0ab47 100644
--- a/float_test.bpl
+++ b/float_test.bpl
@@ -1,11 +1,5 @@
-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?
+procedure F(n: float) returns(r: float)
+	ensures r == n;
 {
-  if (100 < n) {
-    r := n - 10;
-  } else {
-    call r := F(n + 11);
-    call r := F(r);
-  }
+	r := n;
 }
 \ No newline at end of file