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