diff options
Diffstat (limited to 'Chalice/tests/regressions/internal-bug-7.chalice')
| -rw-r--r-- | Chalice/tests/regressions/internal-bug-7.chalice | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/Chalice/tests/regressions/internal-bug-7.chalice b/Chalice/tests/regressions/internal-bug-7.chalice deleted file mode 100644 index 9f7d474d..00000000 --- a/Chalice/tests/regressions/internal-bug-7.chalice +++ /dev/null @@ -1,26 +0,0 @@ -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 |