1 sort bitvec 32
2 input 1 P_3
3 sort bitvec 1
4 slice 3 2 15 15
5 sort bitvec 16
6 zero 5
7 ite 5 4 -6 6
8 slice 5 2 15 0
9 concat 1 7 8
10 input 1 P_2
11 slice 3 10 15 15
12 ite 5 11 -6 6
13 slice 5 10 15 0
14 concat 1 12 13
15 mul 1 9 14
16 sort bitvec 17
17 concat 16 -6 11
18 concat 16 6 11
19 ite 16 11 17 18
20 sort bitvec 33
21 concat 20 19 13
22 concat 16 -6 4
23 concat 16 6 4
24 ite 16 4 22 23
25 concat 20 24 8
26 mul 20 21 25
27 slice 1 26 31 0
28 eq 3 15 27
29 constraint -28