1 files changed, 10 insertions, 0 deletions
diff --git a/Chalice/tests/general-tests/FunctionPostcondition.chalice b/Chalice/tests/general-tests/FunctionPostcondition.chalice
new file mode 100644
index 00000000..7fd95b05
--- /dev/null
+++ b/Chalice/tests/general-tests/FunctionPostcondition.chalice
@@ -0,0 +1,10 @@
+// this test is for function postconditions
+
+class FunctionPostconditions
+{
+  predicate valid { true }
+  
+  function t1(): int
+    ensures unfolding valid in true;
+  { 1 }
+}