1 sort bitvec 32
2 input 1 x
3 input 1 y
4 add 1 -2 -3
5 add 1 2 3
6 add 1 4 5
7 const 1 11111111111111111111111111111110
8 sort bitvec 1
9 eq 8 6 7
10 constraint 9