diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10189.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10189.chalice | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice deleted file mode 100644 index b37b83f2..00000000 --- a/Chalice/tests/regressions/workitem-10189.chalice +++ /dev/null @@ -1,23 +0,0 @@ -class Node { - var v: int - var next: Node - - predicate V { - acc(v) - && acc(next) - && (next != null ==> next.V) - } - - unlimited function length(): int - requires rd(V) - { 1 + unfolding rd(V) in next == null ? 0 : next.length() } - - unlimited function at(i: int): int - requires rd(V) - requires i >= 0 - requires i < length() // XXXX - { - unfolding rd(V) in i == 0 ? v : next.at(i - 1) - // Precondition at XXX might not hold - } -}
\ No newline at end of file |