Chalice/tests/regressions/workitem-10200.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

class Test {
	var f: int;
	
	function fib(n: int): int
		requires n >= 0
	{
		n < 2 ? n : fib(n - 1) + fib(n - 2) // incompletness: termination not atomatically proven
	}

	method fibSeq(n: int) returns (r: int)
		requires n >= 0
		requires acc(this.f)
		ensures acc(this.f)
		ensures r == fib(n) // previous error: the postcondition might not hold
	{
		if (n < 2) {
			r := n
		} else {
			var f1: int; var f2: int
			call f1 := fibSeq(n - 1)
			call f2 := fibSeq(n - 2)
			r := f1 + f2
		}
	}
}