1 files changed, 57 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/setset.chalice b/Chalice/tests/predicates/setset.chalice
new file mode 100644
index 00000000..512c65c1
--- /dev/null
+++ b/Chalice/tests/predicates/setset.chalice
@@ -0,0 +1,57 @@
+class Node {
+  var value: int;
+
+  method init(v: int)
+    requires acc(value)
+    ensures valid
+  {
+    value := v
+    fold this.valid
+  }
+  
+  function get():int requires valid { unfolding valid in value }
+  
+  method set(v: int)
+    requires valid
+    ensures valid && get() == v
+  {
+    unfold valid
+    value := v
+    fold valid
+  }
+  
+  predicate valid {
+    acc(value)
+  }
+  
+  method main(x: Node, y: Node)
+    requires x != null && y != null
+    requires x.valid && y.valid
+  {
+    call x.set(3)
+    call y.set(3)
+    call x.set(3)
+    call y.set(3)
+    call x.set(3)
+    call y.set(3)
+    call x.set(3)
+    unfold x.valid
+    x.value := 3
+    fold x.valid
+    call y.set(3)
+    call x.set(3)
+    call y.set(3)
+    unfold x.valid
+    x.value := 3
+    fold x.valid
+    unfold x.valid
+    x.value := 3
+    fold x.valid
+    call x.set(3)
+    call y.set(3)
+    call x.set(4)
+    
+    assert y.get() == 3
+    assert x.get() == 3 // error: should fail
+  }
+}
+\ No newline at end of file