Negative Range Failure

[DavePearce]

Test 001115 includes the following:

function f(int[] ls) -> bool
requires all { i in -1..4 | (i < 0) || (i >= |ls|) || (ls[i] >= 0) }:
    return true

This does not generate a boogie violation, but does generate an interpreter violation. My feeling is that the interpreter is wrong here.