Test/test20/TypeSynonyms2.bpl


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


type Set a = [a]bool;

function union<a>(x : Set a, y : Set a) returns (Set a);
axiom (forall<a> x : Set a, y : Set a, z : a :: (x[z] || y[z]) == union(x, y)[z]);


const intSet0 : Set int;
axiom (forall x:int :: intSet0[x] == (x == 0 || x == 2 || x == 3));

const intSet1 : Set int;
axiom (forall x:int :: intSet1[x] == (x == -5 || x == 3));


procedure P() returns () {
  assert (forall x:int :: union(intSet0, intSet1)[x] ==
                                     (x == -5 || x == 0 || x == 2 || x == 3));
}