Chalice: Add testcase for mutually recursive predicates (failed before the last commit).

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

+  {}

+  

+}