1 files changed, 24 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/mutual-dependence.chalice b/Chalice/tests/predicates/mutual-dependence.chalice
new file mode 100644
index 00000000..a0939607
--- /dev/null
+++ b/Chalice/tests/predicates/mutual-dependence.chalice
@@ -0,0 +1,24 @@
+class Cell {
+  var value: int;
+  var next: Cell;
+  
+  predicate p { q }
+  predicate q { acc(value) && acc(next) && (next != null ==> next.p) }
+  
+  method test()
+    requires acc(this.*)
+  {
+    value := 1
+    next := null
+    fold q
+    fold p
+    call void()
+    assert unfolding p in unfolding q in value == 1 // ERROR: should not verify
+  }
+  
+  method void()
+    requires p
+    ensures p
+  {}
+  
+}