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