
What am I missing?
// Sum of elements between indices b(egin and e(nd
function method sum(a: array<int>, b: int, e: int): int
requires a != null;
requires 0 <= b <= e < a.Length; // b and e are indices in a
reads a;
decreases e  b;
{
if (b == e) then a[b] // length 1
else sum(a, b, e  1) + a[e] // a[0] + sum(b + 1, e) preferable but failed Test()
}
method Test()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := 9, 6, 7, 8;
assert sum(a, 1, 2) == 13;
assert sum(a, 1, 3) == 21;
}
method Test1()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := 9, 6, 7, 8;
//assertion violation(?!) assert sum(a, 1, 3) == 21;
}



I suppose I am to use sequences here rather than arrays, because following is OK (supported in documentation?):
// Sum of elements between indices b(egin and e(nd
function sum(a: seq<int>, b: int, e: int): int
requires 0 <= b <= e < a; // b and e are indices in a
decreases e  b;
{
if (b == e) then a[b] // length 1
else sum(a, b, e  1) + a[e] // a[0] + sum(b + 1, e) preferable but failed Test()
}
method Test()
{
var a: seq<int> := [9, 6, 7, 8];
assert sum(a, 1, 2) == 13;
assert sum(a, 1, 3) == 21;
}
method Test1()
{
var a: seq<int> := [9, 6, 7, 8];
assert sum(a, 1, 3) == 21;
}



I don't know for sure, but it appears that there is some issue with verification of functions when the termination measure is hit. Here is another version of your code that exhibits the same type, but mirrored problem:
// Sum of elements between indices b(egin and e(nd
function method sum(a: array<int>, b: int, e: int): int
requires a != null;
requires 0 <= b <= e < a.Length; // b and e are indices in a
reads a;
decreases e  b;
{
if (b == e) then a[b] // length 1
else a[b] + sum(a, b + 1, e)
}
method Test()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := 9, 6, 7, 8;
assert sum(a, 2, 3) == 15;
assert sum(a, 1, 3) == 21;
}
method Test1()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := 9, 6, 7, 8;
assert sum(a, 1, 3) == 21;
}

