1 sort bitvec 8
2 input 1 x
3 input 1 y
4 sort bitvec 1
5 slt 4 2 3
6 sub 1 2 3
7 xor 1 2 3
8 xor 1 6 2
9 and 1 7 8
10 xor 1 6 9
11 slice 4 10 7 7
12 eq 4 5 11
13 and 1 2 -3
14 xnor 1 2 3
15 and 1 14 6
16 or 1 13 15
17 slice 4 16 7 7
18 eq 4 5 17
19 slte 4 2 3
20 or 1 2 -3
21 sub 1 3 2
22 or 1 7 -21
23 and 1 20 22
24 slice 4 23 7 7
25 eq 4 19 24
26 sort bitvec 3
27 one 26
28 uext 1 27 5
29 sra 1 14 28
30 add 1 29 13
31 slice 4 30 7 7
32 eq 4 19 31
33 or 4 -12 -18
34 or 4 -25 -32
35 or 4 33 34
36 constraint 35