1 var 13 v0
2 var 5 v1
3 const 1 1
4 const 1 0
5 slice 4 2 3 0
6 slice 1 2 4 4
7 concat 5 5 6
8 slice 1 7 4 4
9 const 5 00001
10 add 5 -7 9
11 cond 5 8 10 7
12 urem 5 11 11
13 add 5 -12 9
14 cond 5 8 13 12
15 const 4 0000
16 concat 5 15 3
17 slice 1 16 4 4
18 slice 4 16 3 0
19 slice 4 7 3 0
20 ult 1 18 19
21 and 1 17 -8
22 and 1 -17 -8
23 and 1 17 8
24 and 1 22 20
25 and 1 23 20
26 and 1 -24 -25
27 and 1 -21 26
28 cond 1 27 3 4
29 concat 5 15 28
30 eq 1 2 29
31 add 1 -3 3
32 concat 5 15 31
33 udiv 5 10 32
34 const 8 00000000
35 concat 13 34 2
36 slice 9 1 12 4
37 slice 4 1 3 0
38 const 9 000000000
39 eq 1 36 38
40 slice 1 35 12 12
41 const 12 000000000000
42 const 12 111111111111
43 slice 1 40 0 0
44 cond 12 43 42 41
45 concat 13 44 40
46 const 3 000
47 const 3 111
48 cond 3 40 47 46
49 concat 16 48 35
50 slice 1 49 15 15
51 srl 16 49 37
52 srl 16 -49 37
53 cond 16 50 -52 51
54 slice 13 53 12 0
55 cond 13 -39 45 54
56 and 5 -14 -16
57 concat 13 41 3
58 and 13 -55 -57
59 and 13 55 57
60 and 13 -58 -59
61 add 5 -10 9
62 add 5 -56 10
63 ult 1 31 4
64 cond 1 63 3 4
65 slice 1 61 4 4
66 slice 1 33 4 4
67 slice 4 61 3 0
68 slice 4 33 3 0
69 ult 1 67 68
70 and 1 65 -66
71 and 1 -65 -66
72 and 1 65 66
73 and 1 71 69
74 and 1 72 69
75 and 1 -73 -74
76 and 1 -70 75
77 cond 1 76 3 4
78 concat 13 41 64
79 slice 1 78 12 12
80 slice 1 -60 12 12
81 slice 12 78 11 0
82 slice 12 -60 11 0
83 ult 1 81 82
84 and 1 79 -80
85 and 1 -79 -80
86 and 1 79 80
87 and 1 85 83
88 and 1 86 83
89 and 1 -87 -88
90 and 1 -84 89
91 cond 1 90 3 4
92 slice 1 -10 4 4
93 slice 4 -10 3 0
94 ult 1 93 93
95 and 1 92 -92
96 and 1 -92 -92
97 and 1 92 92
98 and 1 96 94
99 and 1 97 94
100 and 1 -98 -99
101 and 1 -95 100
102 cond 1 101 3 4
103 const 4 1111
104 slice 1 30 0 0
105 cond 4 104 103 15
106 concat 5 105 30
107 slice 1 62 4 4
108 slice 1 106 4 4
109 slice 4 62 3 0
110 slice 4 106 3 0
111 ult 1 109 110
112 and 1 107 -108
113 and 1 -107 -108
114 and 1 107 108
115 and 1 113 111
116 and 1 114 111
117 and 1 -115 -116
118 and 1 -112 117
119 cond 1 -118 3 4
120 eq 1 102 3
121 concat 5 15 119
122 eq 1 121 7
123 eq 1 91 3
124 eq 1 77 3
125 and 1 123 -124
126 and 1 120 122
127 and 1 -125 126
128 and 1 127 3
129 root 1 128
; error: -rwl3 /tmp/fuzztestboolector9736.btor -uali -uad -uac -m