diff options
Diffstat (limited to 'Chalice/tests/regressions/workitem-10195.chalice')
| -rw-r--r-- | Chalice/tests/regressions/workitem-10195.chalice | 38 |
1 files changed, 0 insertions, 38 deletions
diff --git a/Chalice/tests/regressions/workitem-10195.chalice b/Chalice/tests/regressions/workitem-10195.chalice deleted file mode 100644 index 99ea69f8..00000000 --- a/Chalice/tests/regressions/workitem-10195.chalice +++ /dev/null @@ -1,38 +0,0 @@ -class Test { - method fails() - { - assert forall j in [10..5] :: true // ERROR: min > max - assert false // failed previously, now we get a smoke warning - } - - method succeeds1() - { - assert forall j in [10..5] :: f(j) == 0 // ERROR: min > max - assert false // failed previously, now we get a smoke warning - } - - method fails1() - { - assert forall j in [5..10] :: f(j) == 0 - } - - method succeeds2(a: int, b: int) - requires 0 <= a && 0 <= b - requires f(a) < f(b) - { - assert forall j in [f(b)..f(a)] :: f(j) == 0 // ERROR: min > max - assert false // holds - } - - method fails2(a: int, b: int) - requires 0 <= a && 0 <= b - requires 0 < f(a) - requires f(a) < f(b) - { - assert forall j in [f(a)..f(b)] :: f(j) == 0 - } - - function f(i: int): int - requires 0 <= i - { 0 } - }
\ No newline at end of file |