2 files changed, 30 insertions, 0 deletions
diff --git a/Chalice/tests/regressions/internal-bug-7.chalice b/Chalice/tests/regressions/internal-bug-7.chalice
new file mode 100644
index 00000000..9f7d474d
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-7.chalice
@@ -0,0 +1,26 @@
+class Node {
+  var n: Node
+  
+  predicate P { acc(n) && (n != null ==> acc(n.P)) }
+
+  function length(): int
+    requires rd(P)
+    ensures result >= 1
+  { unfolding rd(P) in 1 + (n == null ? 0 : n.length()) }
+  
+}
+
+class Test {
+  method test(node: Node)
+    requires node != null
+    requires acc(node.P)
+  {
+    assert node.length() >= 1
+    assert (unfolding rd(node.P) in node.n == null) ==> (node.length() == 1) /* Holds in Chalice and Syxc */
+    //assert (unfolding rd(node.P) in node.n != null) ==> (unfolding rd(node.P) in node.n.length() >= 1) /* Holds in Chalice and Syxc */
+    assert (unfolding rd(node.P) in node.n != null) ==> (node.length() > 1) /* Holds in Chalice and Syxc */
+    assert (node.length() == 1) ==> (unfolding rd(node.P) in node.n == null) /* Fails in Chalice and Syxc */
+    assert (node.length() == 1) <==> (unfolding rd(node.P) in node.n == null)
+    // assert n.length() > 1 <==> unfolding rd(n.P) in n.n != null /* Fails in Chalice and Syxc */
+  }
+}
+\ No newline at end of file
diff --git a/Chalice/tests/regressions/internal-bug-7.output.txt b/Chalice/tests/regressions/internal-bug-7.output.txt
new file mode 100644
index 00000000..78ae95fd
--- /dev/null
+++ b/Chalice/tests/regressions/internal-bug-7.output.txt
@@ -0,0 +1,4 @@
+Verification of internal-bug-7.chalice using parameters="" 
+
+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings