Test/z3api/boog35.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

procedure foo1(x: int, y: int)
{
  var a: [int][int]int;

  a[x][y] := 42;

  assert a[x][y] == 42;
}

procedure foo2(x: int, y: int)
{
  var a: [int][int]int;

  a[x][y] := 42;

  assert a[x][y] == 43;
}