1 sort bitvec 3
2 zero 1
3 sort bitvec 1
4 input 3 @inp4
5 input 3 @inp5
6 input 3 @inp6
7 ult 3 5 6
8 and 3 4 -7
9 sort bitvec 2
10 concat 9 -8 -8
11 sort bitvec 5
12 concat 11 2 10
13 zero 11
14 eq 3 12 13
15 concat 9 -4 -4
16 concat 9 -7 -7
17 const 9 10
18 add 9 -16 -17
19 add 9 -15 18
20 zero 9
21 eq 3 19 20
22 and 3 14 -21
23 constraint 22