1 files changed, 32 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/FoldUnfoldExperiments.chalice b/Chalice/tests/predicates/FoldUnfoldExperiments.chalice
new file mode 100644
index 00000000..4bead442
--- /dev/null
+++ b/Chalice/tests/predicates/FoldUnfoldExperiments.chalice
@@ -0,0 +1,32 @@
+class FoldUnfoldExperiments
+{
+  var x:int;
+  var y:int;
+  predicate X { acc(x) }
+  predicate Y { acc(y) }
+  
+  function getX():int
+    requires X;
+  { unfolding X in x }
+  
+  function getY():int
+    requires Y;
+  { unfolding Y in y }
+  
+  method setX(v:int)
+    requires X;
+    ensures X && getX()==v;
+  {
+    unfold X; x:=v; fold X;
+  }
+  
+  method check()
+    requires acc(x) && acc(y);
+    ensures acc(y) && y==2 && X && getX()==3;
+  {
+    x:=1; y:=2;
+    fold X; fold Y;
+    call setX(3);
+    unfold Y;
+  }
+}
+\ No newline at end of file