summaryrefslogtreecommitdiff
path: root/Chalice/tests/predicates/unfolding.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/predicates/unfolding.chalice')
-rw-r--r--Chalice/tests/predicates/unfolding.chalice1
1 files changed, 1 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/unfolding.chalice b/Chalice/tests/predicates/unfolding.chalice
index f01b237d..6b276a04 100644
--- a/Chalice/tests/predicates/unfolding.chalice
+++ b/Chalice/tests/predicates/unfolding.chalice
@@ -14,6 +14,7 @@ class Cell {
method test2()
requires p
+ ensures p
{
var tmp: int := unfolding p in value;
var tmp2: int := unfolding p in value;