1 sort bitvec 1
2 zero 1
3 sort bitvec 2
4 zero 3
5 sort bitvec 3
6 input 5 @inp6
7 zero 5
8 eq 1 6 -7
9 ite 1 8 -2 2
10 concat 3 -2 -9
11 eq 1 -4 10
12 ite 1 11 -2 2
13 sort bitvec 4
14 sort array 1 13
15 input 14 @arr15
16 input 1 @inp16
17 input 1 @inp17
18 ite 3 17 4 -4
19 zero 13
20 concat 13 2 6
21 ult 1 19 20
22 ite 1 21 -2 2
23 eq 1 -2 22
24 ite 1 23 -2 2
25 concat 3 24 22
26 slice 1 25 1 1
27 concat 3 2 -26
28 slice 1 27 0 0
29 uext 3 28 1
30 sll 3 18 29
31 ite 3 16 4 30
32 ult 1 4 31
33 ite 1 32 -2 2
34 concat 13 -7 33
35 write 14 15 2 34
36 read 13 35 2
37 slice 1 36 0 0
38 and 1 12 37
39 sort bitvec 5
40 zero 39
41 concat 39 19 22
42 eq 1 40 41
43 ite 1 42 -2 2
44 sort array 3 1
45 input 44 @arr45
46 concat 5 4 9
47 input 5 @inp47
48 urem 5 46 47
49 slice 1 48 2 2
50 write 44 45 4 -49
51 read 1 50 4
52 and 1 43 51
53 and 1 38 -52
54 eq 1 2 53
55 constraint -54