1 sort bitvec 32
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 sort bitvec 1
6 input 5 @inp6
7 add 1 2 3
8 ite 1 6 2 4
9 eq 5 7 8
10 eq 5 7 4
11 and 5 10 -6
12 zero 1
13 eq 5 3 12
14 eq 5 9 11
15 implies 5 -13 14
16 constraint -15