1 files changed, 33 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/aux-info.chalice b/Chalice/tests/predicates/aux-info.chalice
new file mode 100644
index 00000000..f457c481
--- /dev/null
+++ b/Chalice/tests/predicates/aux-info.chalice
@@ -0,0 +1,33 @@
+class Cell {
+  var value: int;
+  
+  predicate p { acc(value,1) }
+  
+  method test()
+    requires p && acc(value,2)
+  {
+    // previously, the following sequence let to negative secondary permission
+    // to the field value.
+    fold p
+    fold p
+    call void()
+    call void()
+    call void2()
+    
+    unfold p
+    var tmp: int := value
+    fold p
+    // make sure that at this point we can retain information about the field value
+    assert tmp == unfolding p in value
+  }
+  
+  method void()
+    requires p
+  {}
+  
+  method void2()
+    requires p
+    ensures p
+  {}
+  
+}