1 sort bitvec 32
2 input 1 @inp2
3 const 1 00000000000000000000000000001010
4 sort bitvec 1
5 slice 4 3 31 31
6 slice 4 2 31 31
7 sort bitvec 31
8 slice 7 3 30 0
9 slice 7 2 30 0
10 ult 4 8 9
11 and 4 5 -6
12 and 4 -5 -6
13 and 4 5 6
14 and 4 12 10
15 and 4 13 10
16 and 4 -14 -15
17 and 4 -11 16
18 constraint -17