1 sort bitvec 32
2 input 1 x0
3 input 1 x1
4 input 1 y0
5 input 1 y1
6 sort bitvec 1
7 eq 6 2 4
8 eq 6 3 5
9 constd 1 2
10 mul 1 3 9
11 ite 1 8 10 9
12 mul 1 2 11
13 ite 1 7 12 9
14 constd 1 1
15 ite 1 8 5 14
16 mul 1 4 15
17 ite 1 7 16 14
18 mul 1 9 17
19 eq 6 13 18
20 constraint -19