Test/test21/Casts.bpl


1
2
3
4
5
6
7
8
9
10
11


procedure P() returns () {
  var m : [int]int, n : [int]int, x : int;

  assume m[x] == x;
  assume n[x] == 1;

  assert n[m[x]] == 1;
  assert m[n[x]] == 1;    // should not be provable
}