1 sort bitvec 4 2 input 1 @inp2 3 sort bitvec 1 4 sort bitvec 3 5 sort array 4 3 6 input 5 @arr6 7 input 3 @inp7 8 sort bitvec 2 9 input 8 @inp9 10 input 4 @inp10 11 input 8 @inp11 12 input 1 @inp12 13 sort array 4 8 14 input 13 @arr14 15 input 4 @inp15 16 sort array 8 1 17 input 16 @arr17 18 sort array 8 3 19 input 18 @arr19 20 input 8 @inp20 21 input 1 @inp21 22 input 3 @inp22 23 input 8 @inp23 24 input 3 @inp24 25 sort array 8 8 26 input 25 @arr26 27 input 8 @inp27 28 input 13 @arr28 29 sort array 3 3 30 input 29 @arr30 31 sort array 3 4 32 input 31 @arr32 33 uext 4 22 2 34 write 31 32 -22 33 35 usubo 3 -11 -27 36 write 25 26 23 -27 37 write 31 32 -35 33 38 zero 4 39 uext 1 11 2 40 redand 3 39 41 sext 8 -22 1 42 sort bitvec 5 43 concat 42 33 41 44 sub 4 15 10 45 umulo 3 -39 21 46 saddo 3 12 -21 47 sgt 3 -27 20 48 sgt 3 7 -46 49 sort array 8 4 50 input 49 @arr50 51 write 49 50 23 15 52 slice 3 15 2 2 53 xor 3 52 -22 54 and 3 52 47 55 sext 1 45 3 56 sext 8 54 1 57 uext 1 56 2 58 srl 1 55 57 59 slice 3 11 0 0 60 sext 4 23 1 61 write 31 37 59 60 62 ulte 3 2 -58 63 sort array 4 4 64 input 63 @arr64 65 slice 4 2 3 1 66 write 63 64 -65 44 67 or 3 35 52 68 slice 8 58 2 1 69 ugte 3 27 -68 70 sext 8 -46 1 71 uext 1 70 2 72 sll 1 21 71 73 uext 4 69 2 74 udiv 4 73 65 75 sext 1 -35 3 76 slte 3 75 55 77 write 31 37 -40 44 78 slice 8 -12 2 1 79 sext 8 62 1 80 write 25 36 78 79 81 zero 3 82 or 3 47 47 83 slice 8 -44 1 0 84 uext 8 22 1 85 mul 8 83 84 86 const 1 0001 87 sub 3 47 69 88 slice 8 -44 2 1 89 udiv 8 88 -23 90 slice 3 9 0 0 91 slice 3 38 0 0 92 smod 3 90 91 93 sext 8 40 1 94 sdiv 8 93 23 95 slice 8 58 1 0 96 sext 8 7 1 97 sgt 3 -95 96 98 uext 1 74 1 99 sgte 3 72 98 100 uext 8 76 1 101 srl 8 56 100 102 eq 3 6 6 103 sext 8 102 1 104 neq 3 -103 -68 105 neg 3 54 106 write 29 30 -81 -48 107 nand 3 48 67 108 sort array 3 1 109 input 108 @arr109 110 write 108 109 -87 -39 111 uext 8 105 1 112 rol 8 84 111 113 sext 1 40 3 114 uext 1 69 3 115 neq 3 113 114 116 slice 3 112 1 1 117 uext 1 27 2 118 write 108 110 -116 -117 119 slice 3 94 0 0 120 write 29 30 -105 -119 121 uext 8 48 1 122 add 8 112 121 123 uext 8 67 1 124 sext 8 69 1 125 eq 3 123 124 126 write 29 120 97 87 127 uext 1 -89 2 128 slte 3 75 127 129 udiv 1 98 86 130 sext 8 -67 1 131 udiv 8 -130 124 132 and 3 45 -62 133 write 31 37 81 15 134 sext 1 76 3 135 concat 42 134 87 136 write 108 118 62 114 137 uext 1 40 3 138 uext 1 103 2 139 rol 1 137 138 140 uext 8 -48 1 141 neq 3 140 20 142 uext 8 7 1 143 sra 8 -9 142 144 slice 4 139 3 1 145 umulo 3 -144 -38 146 write 25 80 83 23 147 sgte 3 134 129 148 uext 4 62 2 149 redor 3 148 150 sort array 1 1 151 input 150 @arr151 152 input 150 @arr152 153 ite 150 24 151 152 154 slice 3 9 1 1 155 and 3 128 -154 156 ugte 3 55 134 157 sext 4 -40 2 158 sdiv 4 -157 65 159 sext 1 24 3 160 usubo 3 159 98 161 uext 1 104 3 162 ulte 3 -161 -12 163 write 31 61 87 38 164 uext 8 -53 1 165 sort array 1 4 166 input 165 @arr166 167 write 165 166 137 148 168 sext 1 -105 3 169 write 150 152 168 21 170 umulo 3 137 127 171 input 49 @arr171 172 sext 8 -47 1 173 sext 1 -27 2 174 write 16 17 172 -173 175 uext 1 160 3 176 sext 8 54 1 177 uext 1 -176 2 178 ror 1 175 177 179 slice 3 -43 0 0 180 slice 3 -143 0 0 181 nor 3 179 180 182 uext 1 82 3 183 sext 1 125 3 184 ugt 3 -182 -183 185 write 29 106 82 87 186 uext 1 155 3 187 write 165 167 -186 -33 188 slice 8 86 3 2 189 xnor 3 -76 -47 190 concat 42 107 159 191 sext 1 62 3 192 uext 8 54 1 193 uext 1 -192 2 194 ror 1 191 193 195 sub 4 158 158 196 slt 3 -23 20 197 neg 3 46 198 ugt 3 -33 65 199 ugte 3 70 -122 200 neg 8 41 201 sext 4 200 1 202 sext 4 -69 2 203 add 4 201 202 204 input 1 @inp204 205 uext 1 155 3 206 sext 1 105 3 207 ssubo 3 205 206 208 or 3 155 149 209 neg 3 -179 210 sext 8 62 1 211 write 13 28 148 -210 212 neq 3 195 -74 213 input 1 @inp213 214 sort array 1 3 215 input 214 @arr215 216 write 214 215 191 196 217 redxor 3 94 218 slt 3 -204 -137 219 mul 1 72 178 220 slice 3 -139 2 2 221 implies 3 105 -220 222 smod 1 -191 114 223 redand 3 -88 224 zero 4 225 sext 8 217 1 226 sort bitvec 6 227 uext 226 225 4 228 input 8 @inp228 229 read 3 19 79 230 input 4 @inp230 231 input 4 @inp231 232 input 4 @inp232 233 input 4 @inp233 234 input 3 @inp234 235 input 4 @inp235 236 input 1 @inp236 237 input 8 @inp237 238 input 1 @inp238 239 input 4 @inp239 240 input 1 @inp240 241 input 4 @inp241 242 input 1 @inp242 243 input 3 @inp243 244 input 4 @inp244 245 input 8 @inp245 246 input 3 @inp246 247 redor 3 -85 248 redor 3 -101 249 redand 3 131 250 redxor 3 135 251 redxor 3 -164 252 redor 3 188 253 redand 3 190 254 redand 3 194 255 redand 3 203 256 redor 3 -213 257 redxor 3 219 258 redand 3 222 259 redxor 3 224 260 redxor 3 227 261 redand 3 228 262 redor 3 230 263 redor 3 231 264 redor 3 232 265 redxor 3 233 266 redand 3 235 267 redor 3 236 268 redxor 3 237 269 redand 3 -238 270 redand 3 -239 271 redand 3 240 272 redor 3 241 273 redxor 3 242 274 redor 3 244 275 redxor 3 245 276 implies 3 92 -99 277 nor 3 115 132 278 xnor 3 141 145 279 or 3 147 156 280 xnor 3 -162 170 281 xnor 3 181 184 282 or 3 189 197 283 nor 3 198 199 284 xor 3 -207 208 285 nand 3 -209 212 286 implies 3 218 221 287 or 3 223 229 288 or 3 234 243 289 xnor 3 246 247 290 implies 3 -248 249 291 or 3 -250 251 292 implies 3 252 -253 293 implies 3 254 255 294 or 3 256 257 295 iff 3 -258 259 296 nand 3 260 261 297 implies 3 -262 -263 298 xnor 3 264 265 299 nand 3 266 267 300 nor 3 -268 269 301 nand 3 270 271 302 xnor 3 272 273 303 or 3 -274 275 304 implies 3 -276 277 305 nand 3 278 -279 306 implies 3 -280 281 307 xor 3 282 283 308 and 3 -284 -285 309 nand 3 -286 -287 310 xor 3 288 289 311 implies 3 290 291 312 iff 3 292 293 313 xor 3 294 295 314 or 3 296 297 315 nand 3 298 299 316 iff 3 300 -301 317 implies 3 302 303 318 nand 3 304 305 319 iff 3 306 -307 320 and 3 308 -309 321 nor 3 310 311 322 iff 3 -312 -313 323 nor 3 314 315 324 implies 3 316 317 325 iff 3 318 319 326 implies 3 320 -321 327 nor 3 -322 -323 328 and 3 -326 327 329 nand 3 327 328 330 constraint -329