blob: 10caeebb42d9e5fa245cc8981ed0bd8097a124ec (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
class Test {
var next: Test;
var elem: int;
predicate valid {
acc(elem) && acc(next) &&
(next != null ==> next.valid)
}
function get(index:int):int
requires valid
// on 2012-02-21, a bug was reported that caused Chalice to crash with an
// InternalError for the following precondition.
requires unfolding valid in true
{0}
}
|
