1 sort bitvec 8
2 input 1 @inp2
3 sort bitvec 4
4 const 3 0010
5 const 3 0111
6 const 1 00100111
7 const 1 11010111
8 const 1 00101000
9 const 1 11011000
10 sort bitvec 12
11 concat 10 2 4
12 sort bitvec 16
13 concat 12 -11 5
14 concat 12 -2 7
15 sort bitvec 1
16 eq 15 13 14
17 concat 10 2 -4
18 concat 12 -17 5
19 concat 12 -2 6
20 eq 15 18 19
21 concat 10 2 4
22 concat 12 -21 -5
23 concat 12 -2 9
24 eq 15 22 23
25 concat 10 2 -4
26 concat 12 -25 -5
27 concat 12 -2 8
28 eq 15 26 27
29 or 15 -16 -20
30 or 15 -24 -28
31 or 15 29 30
32 constraint 31