1 sort bitvec 8
2 input 1 x
3 one 1
4 neg 1 2
5 add 1 -2 3
6 sort bitvec 1
7 neq 6 4 5
8 sub 1 2 3
9 neq 6 4 -8
10 sub 1 4 3
11 neq 6 -2 10
12 neg 1 -2
13 add 1 2 3
14 neq 6 12 13
15 neq 6 -4 8
16 or 6 7 9
17 or 6 11 14
18 or 6 16 17
19 or 6 18 15
20 constraint 19