Test/bitvectors/bv7.bpl


1
2
3
4
5
6
7
8
9
10
11

// RUN: %boogie -proverWarnings:1 %s > %t
// RUN: %diff %s.expect %t
procedure foo2(x : bv32) returns(r : bv32)
{
  block1:
    r := x[x:1];  // Error
    r := x[(1:13)];  // Error
    return;
}