Test/bitvectors/bv2.bpl


1
2
3
4
5
6
7
8
9
10
11

procedure foo2(x : bv32) returns(r : bv32)
{
  block1:
    r := x[-1:1];  // Error
//    r := x[x:1];  // Error
    r := x[1:x];  // Error
    r := x[1+1:3];  // Error
    return;
}