summaryrefslogtreecommitdiff
path: root/Chalice/tests/regressions/workitem-10196.chalice
diff options
context:
space:
mode:
Diffstat (limited to 'Chalice/tests/regressions/workitem-10196.chalice')
-rw-r--r--Chalice/tests/regressions/workitem-10196.chalice11
1 files changed, 0 insertions, 11 deletions
diff --git a/Chalice/tests/regressions/workitem-10196.chalice b/Chalice/tests/regressions/workitem-10196.chalice
deleted file mode 100644
index 9257e5c2..00000000
--- a/Chalice/tests/regressions/workitem-10196.chalice
+++ /dev/null
@@ -1,11 +0,0 @@
-class C {
- method singleWarning()
- { assert forall i in [] :: true } // previously, quantification over the empty list resulted in Boogie errors
-
- method multipleWarnings()
- { assert forall i in [] :: reqIGt0(i) == i } // previously, quantification over the empty list resulted in Boogie errors
-
- function reqIGt0(i: int): int
- requires i >= 0
- { i }
-} \ No newline at end of file