diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10199.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10199.chalice | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/Chalice/tests/regressions/workitem-10199.chalice b/Chalice/tests/regressions/workitem-10199.chalice deleted file mode 100644 index 678ed078..00000000 --- a/Chalice/tests/regressions/workitem-10199.chalice +++ /dev/null @@ -1,21 +0,0 @@ -class Test { - var z: int - - predicate Z { acc(z) } - predicate ZZ { Z } // XXX - - method useZZ() - requires ZZ - { - // (ZZ,100) - unfold acc(ZZ, 40) - // (ZZ, 60), (Z, 40) - unfold acc(Z, 20) - // (ZZ, 60), (Z, 20), (z, 20) - fold acc(Z, 10) - // (ZZ, 60), (Z, 30), (z, 10) - fold acc(ZZ, 30) - // previoulsy: Fold might fail because the definition of Test.ZZ does not hold. Insufficient fraction at XXX for Test.Z. - // Should be (ZZ, 90), (z, 10) - } -}
\ No newline at end of file |