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