blob: 9257e5c232015b9e29d52623d25f0122dde66606 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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 }
}
|
