// Skip function: __VERIFIER_error

// Skip function: __VERIFIER_nondet_int

// Skip function: __VERIFIER_nondet_ulong

// Function: __compiletime_assert_1016
// with type: void __compiletime_assert_1016()
// with return type: void
void __compiletime_assert_1016() {
  // Void type
  return;
}

// Function: __compiletime_assert_1017
// with type: void __compiletime_assert_1017()
// with return type: void
void __compiletime_assert_1017() {
  // Void type
  return;
}

// Function: __compiletime_assert_1018
// with type: void __compiletime_assert_1018()
// with return type: void
void __compiletime_assert_1018() {
  // Void type
  return;
}

// Function: __compiletime_assert_1020
// with type: void __compiletime_assert_1020()
// with return type: void
void __compiletime_assert_1020() {
  // Void type
  return;
}

// Function: __compiletime_assert_1030
// with type: void __compiletime_assert_1030()
// with return type: void
void __compiletime_assert_1030() {
  // Void type
  return;
}

// Function: __compiletime_assert_1031
// with type: void __compiletime_assert_1031()
// with return type: void
void __compiletime_assert_1031() {
  // Void type
  return;
}

// Function: __compiletime_assert_1089
// with type: void __compiletime_assert_1089()
// with return type: void
void __compiletime_assert_1089() {
  // Void type
  return;
}

// Function: __compiletime_assert_1091
// with type: void __compiletime_assert_1091()
// with return type: void
void __compiletime_assert_1091() {
  // Void type
  return;
}

// Function: __compiletime_assert_1093
// with type: void __compiletime_assert_1093()
// with return type: void
void __compiletime_assert_1093() {
  // Void type
  return;
}

// Function: __compiletime_assert_1095
// with type: void __compiletime_assert_1095()
// with return type: void
void __compiletime_assert_1095() {
  // Void type
  return;
}

// Function: __compiletime_assert_1097
// with type: void __compiletime_assert_1097()
// with return type: void
void __compiletime_assert_1097() {
  // Void type
  return;
}

// Function: __compiletime_assert_1099
// with type: void __compiletime_assert_1099()
// with return type: void
void __compiletime_assert_1099() {
  // Void type
  return;
}

// Function: __compiletime_assert_1100
// with type: void __compiletime_assert_1100()
// with return type: void
void __compiletime_assert_1100() {
  // Void type
  return;
}

// Function: __compiletime_assert_1101
// with type: void __compiletime_assert_1101()
// with return type: void
void __compiletime_assert_1101() {
  // Void type
  return;
}

// Function: __compiletime_assert_1102
// with type: void __compiletime_assert_1102()
// with return type: void
void __compiletime_assert_1102() {
  // Void type
  return;
}

// Function: __compiletime_assert_1103
// with type: void __compiletime_assert_1103()
// with return type: void
void __compiletime_assert_1103() {
  // Void type
  return;
}

// Function: __compiletime_assert_1107
// with type: void __compiletime_assert_1107()
// with return type: void
void __compiletime_assert_1107() {
  // Void type
  return;
}

// Function: __compiletime_assert_1108
// with type: void __compiletime_assert_1108()
// with return type: void
void __compiletime_assert_1108() {
  // Void type
  return;
}

// Function: __compiletime_assert_1109
// with type: void __compiletime_assert_1109()
// with return type: void
void __compiletime_assert_1109() {
  // Void type
  return;
}

// Function: __compiletime_assert_1110
// with type: void __compiletime_assert_1110()
// with return type: void
void __compiletime_assert_1110() {
  // Void type
  return;
}

// Function: __compiletime_assert_1114
// with type: void __compiletime_assert_1114()
// with return type: void
void __compiletime_assert_1114() {
  // Void type
  return;
}

// Function: __compiletime_assert_1115
// with type: void __compiletime_assert_1115()
// with return type: void
void __compiletime_assert_1115() {
  // Void type
  return;
}

// Function: __compiletime_assert_1117
// with type: void __compiletime_assert_1117()
// with return type: void
void __compiletime_assert_1117() {
  // Void type
  return;
}

// Function: __compiletime_assert_1119
// with type: void __compiletime_assert_1119()
// with return type: void
void __compiletime_assert_1119() {
  // Void type
  return;
}

// Function: __compiletime_assert_1155
// with type: void __compiletime_assert_1155()
// with return type: void
void __compiletime_assert_1155() {
  // Void type
  return;
}

// Function: __compiletime_assert_1203
// with type: void __compiletime_assert_1203()
// with return type: void
void __compiletime_assert_1203() {
  // Void type
  return;
}

// Function: __compiletime_assert_1204
// with type: void __compiletime_assert_1204()
// with return type: void
void __compiletime_assert_1204() {
  // Void type
  return;
}

// Function: __compiletime_assert_1206
// with type: void __compiletime_assert_1206()
// with return type: void
void __compiletime_assert_1206() {
  // Void type
  return;
}

// Function: __compiletime_assert_1264
// with type: void __compiletime_assert_1264()
// with return type: void
void __compiletime_assert_1264() {
  // Void type
  return;
}

// Function: __compiletime_assert_1266
// with type: void __compiletime_assert_1266()
// with return type: void
void __compiletime_assert_1266() {
  // Void type
  return;
}

// Function: __compiletime_assert_1269
// with type: void __compiletime_assert_1269()
// with return type: void
void __compiletime_assert_1269() {
  // Void type
  return;
}

// Function: __compiletime_assert_1270
// with type: void __compiletime_assert_1270()
// with return type: void
void __compiletime_assert_1270() {
  // Void type
  return;
}

// Function: __compiletime_assert_1293
// with type: void __compiletime_assert_1293()
// with return type: void
void __compiletime_assert_1293() {
  // Void type
  return;
}

// Function: __compiletime_assert_1295
// with type: void __compiletime_assert_1295()
// with return type: void
void __compiletime_assert_1295() {
  // Void type
  return;
}

// Function: __compiletime_assert_1296
// with type: void __compiletime_assert_1296()
// with return type: void
void __compiletime_assert_1296() {
  // Void type
  return;
}

// Function: __compiletime_assert_1298
// with type: void __compiletime_assert_1298()
// with return type: void
void __compiletime_assert_1298() {
  // Void type
  return;
}

// Function: __compiletime_assert_130
// with type: void __compiletime_assert_130()
// with return type: void
void __compiletime_assert_130() {
  // Void type
  return;
}

// Function: __compiletime_assert_1302
// with type: void __compiletime_assert_1302()
// with return type: void
void __compiletime_assert_1302() {
  // Void type
  return;
}

// Function: __compiletime_assert_1358
// with type: void __compiletime_assert_1358()
// with return type: void
void __compiletime_assert_1358() {
  // Void type
  return;
}

// Function: __compiletime_assert_1360
// with type: void __compiletime_assert_1360()
// with return type: void
void __compiletime_assert_1360() {
  // Void type
  return;
}

// Function: __compiletime_assert_1362
// with type: void __compiletime_assert_1362()
// with return type: void
void __compiletime_assert_1362() {
  // Void type
  return;
}

// Function: __compiletime_assert_1364
// with type: void __compiletime_assert_1364()
// with return type: void
void __compiletime_assert_1364() {
  // Void type
  return;
}

// Function: __compiletime_assert_1365
// with type: void __compiletime_assert_1365()
// with return type: void
void __compiletime_assert_1365() {
  // Void type
  return;
}

// Function: __compiletime_assert_1366
// with type: void __compiletime_assert_1366()
// with return type: void
void __compiletime_assert_1366() {
  // Void type
  return;
}

// Function: __compiletime_assert_1367
// with type: void __compiletime_assert_1367()
// with return type: void
void __compiletime_assert_1367() {
  // Void type
  return;
}

// Function: __compiletime_assert_1374
// with type: void __compiletime_assert_1374()
// with return type: void
void __compiletime_assert_1374() {
  // Void type
  return;
}

// Function: __compiletime_assert_1375
// with type: void __compiletime_assert_1375()
// with return type: void
void __compiletime_assert_1375() {
  // Void type
  return;
}

// Function: __compiletime_assert_1376
// with type: void __compiletime_assert_1376()
// with return type: void
void __compiletime_assert_1376() {
  // Void type
  return;
}

// Function: __compiletime_assert_1384
// with type: void __compiletime_assert_1384()
// with return type: void
void __compiletime_assert_1384() {
  // Void type
  return;
}

// Function: __compiletime_assert_1392
// with type: void __compiletime_assert_1392()
// with return type: void
void __compiletime_assert_1392() {
  // Void type
  return;
}

// Function: __compiletime_assert_1406
// with type: void __compiletime_assert_1406()
// with return type: void
void __compiletime_assert_1406() {
  // Void type
  return;
}

// Function: __compiletime_assert_1407
// with type: void __compiletime_assert_1407()
// with return type: void
void __compiletime_assert_1407() {
  // Void type
  return;
}

// Function: __compiletime_assert_1411
// with type: void __compiletime_assert_1411()
// with return type: void
void __compiletime_assert_1411() {
  // Void type
  return;
}

// Function: __compiletime_assert_1417
// with type: void __compiletime_assert_1417()
// with return type: void
void __compiletime_assert_1417() {
  // Void type
  return;
}

// Function: __compiletime_assert_1418
// with type: void __compiletime_assert_1418()
// with return type: void
void __compiletime_assert_1418() {
  // Void type
  return;
}

// Function: __compiletime_assert_1425
// with type: void __compiletime_assert_1425()
// with return type: void
void __compiletime_assert_1425() {
  // Void type
  return;
}

// Function: __compiletime_assert_1426
// with type: void __compiletime_assert_1426()
// with return type: void
void __compiletime_assert_1426() {
  // Void type
  return;
}

// Function: __compiletime_assert_1433
// with type: void __compiletime_assert_1433()
// with return type: void
void __compiletime_assert_1433() {
  // Void type
  return;
}

// Function: __compiletime_assert_1434
// with type: void __compiletime_assert_1434()
// with return type: void
void __compiletime_assert_1434() {
  // Void type
  return;
}

// Function: __compiletime_assert_1441
// with type: void __compiletime_assert_1441()
// with return type: void
void __compiletime_assert_1441() {
  // Void type
  return;
}

// Function: __compiletime_assert_1442
// with type: void __compiletime_assert_1442()
// with return type: void
void __compiletime_assert_1442() {
  // Void type
  return;
}

// Function: __compiletime_assert_1464
// with type: void __compiletime_assert_1464()
// with return type: void
void __compiletime_assert_1464() {
  // Void type
  return;
}

// Function: __compiletime_assert_1487
// with type: void __compiletime_assert_1487()
// with return type: void
void __compiletime_assert_1487() {
  // Void type
  return;
}

// Function: __compiletime_assert_1489
// with type: void __compiletime_assert_1489()
// with return type: void
void __compiletime_assert_1489() {
  // Void type
  return;
}

// Function: __compiletime_assert_1506
// with type: void __compiletime_assert_1506()
// with return type: void
void __compiletime_assert_1506() {
  // Void type
  return;
}

// Function: __compiletime_assert_1519
// with type: void __compiletime_assert_1519()
// with return type: void
void __compiletime_assert_1519() {
  // Void type
  return;
}

// Function: __compiletime_assert_1527
// with type: void __compiletime_assert_1527()
// with return type: void
void __compiletime_assert_1527() {
  // Void type
  return;
}

// Function: __compiletime_assert_157
// with type: void __compiletime_assert_157()
// with return type: void
void __compiletime_assert_157() {
  // Void type
  return;
}

// Function: __compiletime_assert_159
// with type: void __compiletime_assert_159()
// with return type: void
void __compiletime_assert_159() {
  // Void type
  return;
}

// Function: __compiletime_assert_160
// with type: void __compiletime_assert_160()
// with return type: void
void __compiletime_assert_160() {
  // Void type
  return;
}

// Function: __compiletime_assert_161
// with type: void __compiletime_assert_161()
// with return type: void
void __compiletime_assert_161() {
  // Void type
  return;
}

// Function: __compiletime_assert_1792
// with type: void __compiletime_assert_1792()
// with return type: void
void __compiletime_assert_1792() {
  // Void type
  return;
}

// Function: __compiletime_assert_184
// with type: void __compiletime_assert_184()
// with return type: void
void __compiletime_assert_184() {
  // Void type
  return;
}

// Function: __compiletime_assert_186
// with type: void __compiletime_assert_186()
// with return type: void
void __compiletime_assert_186() {
  // Void type
  return;
}

// Function: __compiletime_assert_187
// with type: void __compiletime_assert_187()
// with return type: void
void __compiletime_assert_187() {
  // Void type
  return;
}

// Function: __compiletime_assert_191
// with type: void __compiletime_assert_191()
// with return type: void
void __compiletime_assert_191() {
  // Void type
  return;
}

// Function: __compiletime_assert_195
// with type: void __compiletime_assert_195()
// with return type: void
void __compiletime_assert_195() {
  // Void type
  return;
}

// Function: __compiletime_assert_211
// with type: void __compiletime_assert_211()
// with return type: void
void __compiletime_assert_211() {
  // Void type
  return;
}

// Function: __compiletime_assert_213
// with type: void __compiletime_assert_213()
// with return type: void
void __compiletime_assert_213() {
  // Void type
  return;
}

// Function: __compiletime_assert_217
// with type: void __compiletime_assert_217()
// with return type: void
void __compiletime_assert_217() {
  // Void type
  return;
}

// Function: __compiletime_assert_218
// with type: void __compiletime_assert_218()
// with return type: void
void __compiletime_assert_218() {
  // Void type
  return;
}

// Function: __compiletime_assert_219
// with type: void __compiletime_assert_219()
// with return type: void
void __compiletime_assert_219() {
  // Void type
  return;
}

// Function: __compiletime_assert_220
// with type: void __compiletime_assert_220()
// with return type: void
void __compiletime_assert_220() {
  // Void type
  return;
}

// Function: __compiletime_assert_283
// with type: void __compiletime_assert_283()
// with return type: void
void __compiletime_assert_283() {
  // Void type
  return;
}

// Function: __compiletime_assert_298
// with type: void __compiletime_assert_298()
// with return type: void
void __compiletime_assert_298() {
  // Void type
  return;
}

// Function: __compiletime_assert_300
// with type: void __compiletime_assert_300()
// with return type: void
void __compiletime_assert_300() {
  // Void type
  return;
}

// Function: __compiletime_assert_314
// with type: void __compiletime_assert_314()
// with return type: void
void __compiletime_assert_314() {
  // Void type
  return;
}

// Function: __compiletime_assert_315
// with type: void __compiletime_assert_315()
// with return type: void
void __compiletime_assert_315() {
  // Void type
  return;
}

// Function: __compiletime_assert_365
// with type: void __compiletime_assert_365()
// with return type: void
void __compiletime_assert_365() {
  // Void type
  return;
}

// Function: __compiletime_assert_368
// with type: void __compiletime_assert_368()
// with return type: void
void __compiletime_assert_368() {
  // Void type
  return;
}

// Function: __compiletime_assert_374
// with type: void __compiletime_assert_374()
// with return type: void
void __compiletime_assert_374() {
  // Void type
  return;
}

// Function: __compiletime_assert_407
// with type: void __compiletime_assert_407()
// with return type: void
void __compiletime_assert_407() {
  // Void type
  return;
}

// Function: __compiletime_assert_408
// with type: void __compiletime_assert_408()
// with return type: void
void __compiletime_assert_408() {
  // Void type
  return;
}

// Function: __compiletime_assert_410
// with type: void __compiletime_assert_410()
// with return type: void
void __compiletime_assert_410() {
  // Void type
  return;
}

// Function: __compiletime_assert_415
// with type: void __compiletime_assert_415()
// with return type: void
void __compiletime_assert_415() {
  // Void type
  return;
}

// Function: __compiletime_assert_434
// with type: void __compiletime_assert_434()
// with return type: void
void __compiletime_assert_434() {
  // Void type
  return;
}

// Function: __compiletime_assert_436
// with type: void __compiletime_assert_436()
// with return type: void
void __compiletime_assert_436() {
  // Void type
  return;
}

// Function: __compiletime_assert_438
// with type: void __compiletime_assert_438()
// with return type: void
void __compiletime_assert_438() {
  // Void type
  return;
}

// Function: __compiletime_assert_440
// with type: void __compiletime_assert_440()
// with return type: void
void __compiletime_assert_440() {
  // Void type
  return;
}

// Function: __compiletime_assert_443
// with type: void __compiletime_assert_443()
// with return type: void
void __compiletime_assert_443() {
  // Void type
  return;
}

// Function: __compiletime_assert_444
// with type: void __compiletime_assert_444()
// with return type: void
void __compiletime_assert_444() {
  // Void type
  return;
}

// Function: __compiletime_assert_446
// with type: void __compiletime_assert_446()
// with return type: void
void __compiletime_assert_446() {
  // Void type
  return;
}

// Function: __compiletime_assert_447
// with type: void __compiletime_assert_447()
// with return type: void
void __compiletime_assert_447() {
  // Void type
  return;
}

// Function: __compiletime_assert_465
// with type: void __compiletime_assert_465()
// with return type: void
void __compiletime_assert_465() {
  // Void type
  return;
}

// Function: __compiletime_assert_467
// with type: void __compiletime_assert_467()
// with return type: void
void __compiletime_assert_467() {
  // Void type
  return;
}

// Function: __compiletime_assert_474
// with type: void __compiletime_assert_474()
// with return type: void
void __compiletime_assert_474() {
  // Void type
  return;
}

// Function: __compiletime_assert_478
// with type: void __compiletime_assert_478()
// with return type: void
void __compiletime_assert_478() {
  // Void type
  return;
}

// Function: __compiletime_assert_500
// with type: void __compiletime_assert_500()
// with return type: void
void __compiletime_assert_500() {
  // Void type
  return;
}

// Function: __compiletime_assert_511
// with type: void __compiletime_assert_511()
// with return type: void
void __compiletime_assert_511() {
  // Void type
  return;
}

// Function: __compiletime_assert_547
// with type: void __compiletime_assert_547()
// with return type: void
void __compiletime_assert_547() {
  // Void type
  return;
}

// Function: __compiletime_assert_548
// with type: void __compiletime_assert_548()
// with return type: void
void __compiletime_assert_548() {
  // Void type
  return;
}

// Function: __compiletime_assert_549
// with type: void __compiletime_assert_549()
// with return type: void
void __compiletime_assert_549() {
  // Void type
  return;
}

// Function: __compiletime_assert_552
// with type: void __compiletime_assert_552()
// with return type: void
void __compiletime_assert_552() {
  // Void type
  return;
}

// Function: __compiletime_assert_553
// with type: void __compiletime_assert_553()
// with return type: void
void __compiletime_assert_553() {
  // Void type
  return;
}

// Function: __compiletime_assert_554
// with type: void __compiletime_assert_554()
// with return type: void
void __compiletime_assert_554() {
  // Void type
  return;
}

// Function: __compiletime_assert_558
// with type: void __compiletime_assert_558()
// with return type: void
void __compiletime_assert_558() {
  // Void type
  return;
}

// Function: __compiletime_assert_559
// with type: void __compiletime_assert_559()
// with return type: void
void __compiletime_assert_559() {
  // Void type
  return;
}

// Function: __compiletime_assert_560
// with type: void __compiletime_assert_560()
// with return type: void
void __compiletime_assert_560() {
  // Void type
  return;
}

// Function: __compiletime_assert_569
// with type: void __compiletime_assert_569()
// with return type: void
void __compiletime_assert_569() {
  // Void type
  return;
}

// Function: __compiletime_assert_572
// with type: void __compiletime_assert_572()
// with return type: void
void __compiletime_assert_572() {
  // Void type
  return;
}

// Function: __compiletime_assert_576
// with type: void __compiletime_assert_576()
// with return type: void
void __compiletime_assert_576() {
  // Void type
  return;
}

// Function: __compiletime_assert_584
// with type: void __compiletime_assert_584()
// with return type: void
void __compiletime_assert_584() {
  // Void type
  return;
}

// Function: __compiletime_assert_585
// with type: void __compiletime_assert_585()
// with return type: void
void __compiletime_assert_585() {
  // Void type
  return;
}

// Function: __compiletime_assert_586
// with type: void __compiletime_assert_586()
// with return type: void
void __compiletime_assert_586() {
  // Void type
  return;
}

// Function: __compiletime_assert_592
// with type: void __compiletime_assert_592()
// with return type: void
void __compiletime_assert_592() {
  // Void type
  return;
}

// Function: __compiletime_assert_594
// with type: void __compiletime_assert_594()
// with return type: void
void __compiletime_assert_594() {
  // Void type
  return;
}

// Function: __compiletime_assert_595
// with type: void __compiletime_assert_595()
// with return type: void
void __compiletime_assert_595() {
  // Void type
  return;
}

// Function: __compiletime_assert_610
// with type: void __compiletime_assert_610()
// with return type: void
void __compiletime_assert_610() {
  // Void type
  return;
}

// Function: __compiletime_assert_641
// with type: void __compiletime_assert_641()
// with return type: void
void __compiletime_assert_641() {
  // Void type
  return;
}

// Function: __compiletime_assert_656
// with type: void __compiletime_assert_656()
// with return type: void
void __compiletime_assert_656() {
  // Void type
  return;
}

// Function: __compiletime_assert_658
// with type: void __compiletime_assert_658()
// with return type: void
void __compiletime_assert_658() {
  // Void type
  return;
}

// Function: __compiletime_assert_661
// with type: void __compiletime_assert_661()
// with return type: void
void __compiletime_assert_661() {
  // Void type
  return;
}

// Function: __compiletime_assert_664
// with type: void __compiletime_assert_664()
// with return type: void
void __compiletime_assert_664() {
  // Void type
  return;
}

// Function: __compiletime_assert_668
// with type: void __compiletime_assert_668()
// with return type: void
void __compiletime_assert_668() {
  // Void type
  return;
}

// Function: __compiletime_assert_702
// with type: void __compiletime_assert_702()
// with return type: void
void __compiletime_assert_702() {
  // Void type
  return;
}

// Function: __compiletime_assert_708
// with type: void __compiletime_assert_708()
// with return type: void
void __compiletime_assert_708() {
  // Void type
  return;
}

// Function: __compiletime_assert_718
// with type: void __compiletime_assert_718()
// with return type: void
void __compiletime_assert_718() {
  // Void type
  return;
}

// Function: __compiletime_assert_722
// with type: void __compiletime_assert_722()
// with return type: void
void __compiletime_assert_722() {
  // Void type
  return;
}

// Function: __compiletime_assert_726
// with type: void __compiletime_assert_726()
// with return type: void
void __compiletime_assert_726() {
  // Void type
  return;
}

// Function: __compiletime_assert_730
// with type: void __compiletime_assert_730()
// with return type: void
void __compiletime_assert_730() {
  // Void type
  return;
}

// Function: __compiletime_assert_747
// with type: void __compiletime_assert_747()
// with return type: void
void __compiletime_assert_747() {
  // Void type
  return;
}

// Function: __compiletime_assert_752
// with type: void __compiletime_assert_752()
// with return type: void
void __compiletime_assert_752() {
  // Void type
  return;
}

// Function: __compiletime_assert_753
// with type: void __compiletime_assert_753()
// with return type: void
void __compiletime_assert_753() {
  // Void type
  return;
}

// Function: __compiletime_assert_754
// with type: void __compiletime_assert_754()
// with return type: void
void __compiletime_assert_754() {
  // Void type
  return;
}

// Function: __compiletime_assert_770
// with type: void __compiletime_assert_770()
// with return type: void
void __compiletime_assert_770() {
  // Void type
  return;
}

// Function: __compiletime_assert_775
// with type: void __compiletime_assert_775()
// with return type: void
void __compiletime_assert_775() {
  // Void type
  return;
}

// Function: __compiletime_assert_776
// with type: void __compiletime_assert_776()
// with return type: void
void __compiletime_assert_776() {
  // Void type
  return;
}

// Function: __compiletime_assert_777
// with type: void __compiletime_assert_777()
// with return type: void
void __compiletime_assert_777() {
  // Void type
  return;
}

// Function: __compiletime_assert_798
// with type: void __compiletime_assert_798()
// with return type: void
void __compiletime_assert_798() {
  // Void type
  return;
}

// Function: __compiletime_assert_805
// with type: void __compiletime_assert_805()
// with return type: void
void __compiletime_assert_805() {
  // Void type
  return;
}

// Function: __compiletime_assert_806
// with type: void __compiletime_assert_806()
// with return type: void
void __compiletime_assert_806() {
  // Void type
  return;
}

// Function: __compiletime_assert_807
// with type: void __compiletime_assert_807()
// with return type: void
void __compiletime_assert_807() {
  // Void type
  return;
}

// Function: __compiletime_assert_811
// with type: void __compiletime_assert_811()
// with return type: void
void __compiletime_assert_811() {
  // Void type
  return;
}

// Function: __compiletime_assert_812
// with type: void __compiletime_assert_812()
// with return type: void
void __compiletime_assert_812() {
  // Void type
  return;
}

// Function: __compiletime_assert_813
// with type: void __compiletime_assert_813()
// with return type: void
void __compiletime_assert_813() {
  // Void type
  return;
}

// Function: __compiletime_assert_817
// with type: void __compiletime_assert_817()
// with return type: void
void __compiletime_assert_817() {
  // Void type
  return;
}

// Function: __compiletime_assert_818
// with type: void __compiletime_assert_818()
// with return type: void
void __compiletime_assert_818() {
  // Void type
  return;
}

// Function: __compiletime_assert_819
// with type: void __compiletime_assert_819()
// with return type: void
void __compiletime_assert_819() {
  // Void type
  return;
}

// Function: __compiletime_assert_820
// with type: void __compiletime_assert_820()
// with return type: void
void __compiletime_assert_820() {
  // Void type
  return;
}

// Function: __compiletime_assert_824
// with type: void __compiletime_assert_824()
// with return type: void
void __compiletime_assert_824() {
  // Void type
  return;
}

// Function: __compiletime_assert_825
// with type: void __compiletime_assert_825()
// with return type: void
void __compiletime_assert_825() {
  // Void type
  return;
}

// Function: __compiletime_assert_826
// with type: void __compiletime_assert_826()
// with return type: void
void __compiletime_assert_826() {
  // Void type
  return;
}

// Function: __compiletime_assert_827
// with type: void __compiletime_assert_827()
// with return type: void
void __compiletime_assert_827() {
  // Void type
  return;
}

// Function: __compiletime_assert_831
// with type: void __compiletime_assert_831()
// with return type: void
void __compiletime_assert_831() {
  // Void type
  return;
}

// Function: __compiletime_assert_832
// with type: void __compiletime_assert_832()
// with return type: void
void __compiletime_assert_832() {
  // Void type
  return;
}

// Function: __compiletime_assert_833
// with type: void __compiletime_assert_833()
// with return type: void
void __compiletime_assert_833() {
  // Void type
  return;
}

// Function: __compiletime_assert_834
// with type: void __compiletime_assert_834()
// with return type: void
void __compiletime_assert_834() {
  // Void type
  return;
}

// Function: __compiletime_assert_838
// with type: void __compiletime_assert_838()
// with return type: void
void __compiletime_assert_838() {
  // Void type
  return;
}

// Function: __compiletime_assert_839
// with type: void __compiletime_assert_839()
// with return type: void
void __compiletime_assert_839() {
  // Void type
  return;
}

// Function: __compiletime_assert_840
// with type: void __compiletime_assert_840()
// with return type: void
void __compiletime_assert_840() {
  // Void type
  return;
}

// Function: __compiletime_assert_841
// with type: void __compiletime_assert_841()
// with return type: void
void __compiletime_assert_841() {
  // Void type
  return;
}

// Function: __compiletime_assert_845
// with type: void __compiletime_assert_845()
// with return type: void
void __compiletime_assert_845() {
  // Void type
  return;
}

// Function: __compiletime_assert_846
// with type: void __compiletime_assert_846()
// with return type: void
void __compiletime_assert_846() {
  // Void type
  return;
}

// Function: __compiletime_assert_847
// with type: void __compiletime_assert_847()
// with return type: void
void __compiletime_assert_847() {
  // Void type
  return;
}

// Function: __compiletime_assert_848
// with type: void __compiletime_assert_848()
// with return type: void
void __compiletime_assert_848() {
  // Void type
  return;
}

// Function: __compiletime_assert_858
// with type: void __compiletime_assert_858()
// with return type: void
void __compiletime_assert_858() {
  // Void type
  return;
}

// Function: __compiletime_assert_859
// with type: void __compiletime_assert_859()
// with return type: void
void __compiletime_assert_859() {
  // Void type
  return;
}

// Function: __compiletime_assert_860
// with type: void __compiletime_assert_860()
// with return type: void
void __compiletime_assert_860() {
  // Void type
  return;
}

// Function: __compiletime_assert_865
// with type: void __compiletime_assert_865()
// with return type: void
void __compiletime_assert_865() {
  // Void type
  return;
}

// Function: __compiletime_assert_868
// with type: void __compiletime_assert_868()
// with return type: void
void __compiletime_assert_868() {
  // Void type
  return;
}

// Function: __compiletime_assert_869
// with type: void __compiletime_assert_869()
// with return type: void
void __compiletime_assert_869() {
  // Void type
  return;
}

// Function: __compiletime_assert_880
// with type: void __compiletime_assert_880()
// with return type: void
void __compiletime_assert_880() {
  // Void type
  return;
}

// Function: __compiletime_assert_884
// with type: void __compiletime_assert_884()
// with return type: void
void __compiletime_assert_884() {
  // Void type
  return;
}

// Function: __compiletime_assert_885
// with type: void __compiletime_assert_885()
// with return type: void
void __compiletime_assert_885() {
  // Void type
  return;
}

// Function: __compiletime_assert_886
// with type: void __compiletime_assert_886()
// with return type: void
void __compiletime_assert_886() {
  // Void type
  return;
}

// Function: __compiletime_assert_890
// with type: void __compiletime_assert_890()
// with return type: void
void __compiletime_assert_890() {
  // Void type
  return;
}

// Function: __compiletime_assert_894
// with type: void __compiletime_assert_894()
// with return type: void
void __compiletime_assert_894() {
  // Void type
  return;
}

// Function: __compiletime_assert_898
// with type: void __compiletime_assert_898()
// with return type: void
void __compiletime_assert_898() {
  // Void type
  return;
}

// Function: __compiletime_assert_966
// with type: void __compiletime_assert_966()
// with return type: void
void __compiletime_assert_966() {
  // Void type
  return;
}

// Function: __compiletime_assert_967
// with type: void __compiletime_assert_967()
// with return type: void
void __compiletime_assert_967() {
  // Void type
  return;
}

// Function: __const_udelay
// with type: void __const_udelay(unsigned long)
// with return type: void
void __const_udelay(unsigned long arg0) {
  // Void type
  return;
}

// Function: __dynamic_dev_dbg
// with type: int __dynamic_dev_dbg(struct _ddebug *, const struct device *, const char *, ...)
// with return type: int
int __VERIFIER_nondet_int(void);
int __dynamic_dev_dbg(struct _ddebug *arg0, const struct device *arg1, const char *arg2, ...) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: _dev_info
// with type: int _dev_info(const struct device *, const char *, ...)
// with return type: int
int __VERIFIER_nondet_int(void);
int _dev_info(const struct device *arg0, const char *arg1, ...) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Skip function: calloc

// Function: consume_skb
// with type: void consume_skb(struct sk_buff *)
// with return type: void
void consume_skb(struct sk_buff *arg0) {
  // Void type
  return;
}

// Function: dev_err
// with type: int dev_err(const struct device *, const char *, ...)
// with return type: int
int __VERIFIER_nondet_int(void);
int dev_err(const struct device *arg0, const char *arg1, ...) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Skip function: free

// Function: get_random_bytes
// with type: void get_random_bytes(void *, int)
// with return type: void
void get_random_bytes(void *arg0, int arg1) {
  // Void type
  return;
}

// Function: ldv_after_alloc
// with type: void ldv_after_alloc(void *)
// with return type: void
void ldv_after_alloc(void *arg0) {
  // Void type
  return;
}

// Function: ldv_assert
// with type: void ldv_assert(const char *, int)
// with return type: void
void ldv_assert(const char *arg0, int arg1) {
  // Void type
  return;
}

// Function: ldv_check_alloc_flags
// with type: void ldv_check_alloc_flags(gfp_t )
// with return type: void
void ldv_check_alloc_flags(gfp_t arg0) {
  // Void type
  return;
}

// Function: ldv_pre_probe
// with type: void ldv_pre_probe()
// with return type: void
void ldv_pre_probe() {
  // Void type
  return;
}

// Function: ldv_pre_usb_register_driver
// with type: int ldv_pre_usb_register_driver()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_pre_usb_register_driver() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Skip function: malloc

// Skip function: memcpy

// Skip function: memset

// Function: msleep
// with type: void msleep(unsigned int)
// with return type: void
void msleep(unsigned int arg0) {
  // Void type
  return;
}

// Function: rt2x00debug_dump_frame
// with type: void rt2x00debug_dump_frame(struct rt2x00_dev *, enum rt2x00_dump_type , struct sk_buff *)
// with return type: void
void rt2x00debug_dump_frame(struct rt2x00_dev *arg0, enum rt2x00_dump_type arg1, struct sk_buff *arg2) {
  // Void type
  return;
}

// Function: rt2x00mac_add_interface
// with type: int rt2x00mac_add_interface(struct ieee80211_hw *, struct ieee80211_vif *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_add_interface(struct ieee80211_hw *arg0, struct ieee80211_vif *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_bss_info_changed
// with type: void rt2x00mac_bss_info_changed(struct ieee80211_hw *, struct ieee80211_vif *, struct ieee80211_bss_conf *, u32 )
// with return type: void
void rt2x00mac_bss_info_changed(struct ieee80211_hw *arg0, struct ieee80211_vif *arg1, struct ieee80211_bss_conf *arg2, u32 arg3) {
  // Void type
  return;
}

// Function: rt2x00mac_conf_tx
// with type: int rt2x00mac_conf_tx(struct ieee80211_hw *, struct ieee80211_vif *, u16 , const struct ieee80211_tx_queue_params *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_conf_tx(struct ieee80211_hw *arg0, struct ieee80211_vif *arg1, u16 arg2, const struct ieee80211_tx_queue_params *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_configure_filter
// with type: void rt2x00mac_configure_filter(struct ieee80211_hw *, unsigned int, unsigned int *, u64 )
// with return type: void
void rt2x00mac_configure_filter(struct ieee80211_hw *arg0, unsigned int arg1, unsigned int *arg2, u64 arg3) {
  // Void type
  return;
}

// Function: rt2x00mac_flush
// with type: void rt2x00mac_flush(struct ieee80211_hw *, u32 , bool )
// with return type: void
void rt2x00mac_flush(struct ieee80211_hw *arg0, u32 arg1, bool arg2) {
  // Void type
  return;
}

// Function: rt2x00mac_get_antenna
// with type: int rt2x00mac_get_antenna(struct ieee80211_hw *, u32 *, u32 *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_get_antenna(struct ieee80211_hw *arg0, u32 *arg1, u32 *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_get_ringparam
// with type: void rt2x00mac_get_ringparam(struct ieee80211_hw *, u32 *, u32 *, u32 *, u32 *)
// with return type: void
void rt2x00mac_get_ringparam(struct ieee80211_hw *arg0, u32 *arg1, u32 *arg2, u32 *arg3, u32 *arg4) {
  // Void type
  return;
}

// Function: rt2x00mac_get_stats
// with type: int rt2x00mac_get_stats(struct ieee80211_hw *, struct ieee80211_low_level_stats *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_get_stats(struct ieee80211_hw *arg0, struct ieee80211_low_level_stats *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_remove_interface
// with type: void rt2x00mac_remove_interface(struct ieee80211_hw *, struct ieee80211_vif *)
// with return type: void
void rt2x00mac_remove_interface(struct ieee80211_hw *arg0, struct ieee80211_vif *arg1) {
  // Void type
  return;
}

// Function: rt2x00mac_set_antenna
// with type: int rt2x00mac_set_antenna(struct ieee80211_hw *, u32 , u32 )
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_set_antenna(struct ieee80211_hw *arg0, u32 arg1, u32 arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_set_key
// with type: int rt2x00mac_set_key(struct ieee80211_hw *, enum set_key_cmd , struct ieee80211_vif *, struct ieee80211_sta *, struct ieee80211_key_conf *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_set_key(struct ieee80211_hw *arg0, enum set_key_cmd arg1, struct ieee80211_vif *arg2, struct ieee80211_sta *arg3, struct ieee80211_key_conf *arg4) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_set_tim
// with type: int rt2x00mac_set_tim(struct ieee80211_hw *, struct ieee80211_sta *, bool )
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_set_tim(struct ieee80211_hw *arg0, struct ieee80211_sta *arg1, bool arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_start
// with type: int rt2x00mac_start(struct ieee80211_hw *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00mac_start(struct ieee80211_hw *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00mac_stop
// with type: void rt2x00mac_stop(struct ieee80211_hw *)
// with return type: void
void rt2x00mac_stop(struct ieee80211_hw *arg0) {
  // Void type
  return;
}

// Function: rt2x00mac_sw_scan_complete
// with type: void rt2x00mac_sw_scan_complete(struct ieee80211_hw *)
// with return type: void
void rt2x00mac_sw_scan_complete(struct ieee80211_hw *arg0) {
  // Void type
  return;
}

// Function: rt2x00mac_sw_scan_start
// with type: void rt2x00mac_sw_scan_start(struct ieee80211_hw *)
// with return type: void
void rt2x00mac_sw_scan_start(struct ieee80211_hw *arg0) {
  // Void type
  return;
}

// Function: rt2x00mac_tx
// with type: void rt2x00mac_tx(struct ieee80211_hw *, struct ieee80211_tx_control *, struct sk_buff *)
// with return type: void
void rt2x00mac_tx(struct ieee80211_hw *arg0, struct ieee80211_tx_control *arg1, struct sk_buff *arg2) {
  // Void type
  return;
}

// Function: rt2x00mac_tx_frames_pending
// with type: bool rt2x00mac_tx_frames_pending(struct ieee80211_hw *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool rt2x00mac_tx_frames_pending(struct ieee80211_hw *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: rt2x00usb_clear_entry
// with type: void rt2x00usb_clear_entry(struct queue_entry *)
// with return type: void
void rt2x00usb_clear_entry(struct queue_entry *arg0) {
  // Void type
  return;
}

// Function: rt2x00usb_disable_radio
// with type: void rt2x00usb_disable_radio(struct rt2x00_dev *)
// with return type: void
void rt2x00usb_disable_radio(struct rt2x00_dev *arg0) {
  // Void type
  return;
}

// Function: rt2x00usb_disconnect
// with type: void rt2x00usb_disconnect(struct usb_interface *)
// with return type: void
void rt2x00usb_disconnect(struct usb_interface *arg0) {
  // Void type
  return;
}

// Function: rt2x00usb_flush_queue
// with type: void rt2x00usb_flush_queue(struct data_queue *, bool )
// with return type: void
void rt2x00usb_flush_queue(struct data_queue *arg0, bool arg1) {
  // Void type
  return;
}

// Function: rt2x00usb_initialize
// with type: int rt2x00usb_initialize(struct rt2x00_dev *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_initialize(struct rt2x00_dev *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_kick_queue
// with type: void rt2x00usb_kick_queue(struct data_queue *)
// with return type: void
void rt2x00usb_kick_queue(struct data_queue *arg0) {
  // Void type
  return;
}

// Function: rt2x00usb_probe
// with type: int rt2x00usb_probe(struct usb_interface *, const struct rt2x00_ops *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_probe(struct usb_interface *arg0, const struct rt2x00_ops *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_resume
// with type: int rt2x00usb_resume(struct usb_interface *)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_resume(struct usb_interface *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_suspend
// with type: int rt2x00usb_suspend(struct usb_interface *, pm_message_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_suspend(struct usb_interface *arg0, pm_message_t arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_uninitialize
// with type: void rt2x00usb_uninitialize(struct rt2x00_dev *)
// with return type: void
void rt2x00usb_uninitialize(struct rt2x00_dev *arg0) {
  // Void type
  return;
}

// Function: rt2x00usb_vendor_req_buff_lock
// with type: int rt2x00usb_vendor_req_buff_lock(struct rt2x00_dev *, const u8 , const u8 , const u16 , void *, const u16 , const int)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_vendor_req_buff_lock(struct rt2x00_dev *arg0, const u8 arg1, const u8 arg2, const u16 arg3, void *arg4, const u16 arg5, const int arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_vendor_request
// with type: int rt2x00usb_vendor_request(struct rt2x00_dev *, const u8 , const u8 , const u16 , const u16 , void *, const u16 , const int)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_vendor_request(struct rt2x00_dev *arg0, const u8 arg1, const u8 arg2, const u16 arg3, const u16 arg4, void *arg5, const u16 arg6, const int arg7) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_vendor_request_buff
// with type: int rt2x00usb_vendor_request_buff(struct rt2x00_dev *, const u8 , const u8 , const u16 , void *, const u16 , const int)
// with return type: int
int __VERIFIER_nondet_int(void);
int rt2x00usb_vendor_request_buff(struct rt2x00_dev *arg0, const u8 arg1, const u8 arg2, const u16 arg3, void *arg4, const u16 arg5, const int arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: rt2x00usb_watchdog
// with type: void rt2x00usb_watchdog(struct rt2x00_dev *)
// with return type: void
void rt2x00usb_watchdog(struct rt2x00_dev *arg0) {
  // Void type
  return;
}

// Function: rtnl_lock
// with type: void rtnl_lock()
// with return type: void
void rtnl_lock() {
  // Void type
  return;
}

// Function: rtnl_unlock
// with type: void rtnl_unlock()
// with return type: void
void rtnl_unlock() {
  // Void type
  return;
}

// Function: skb_push
// with type: unsigned char *skb_push(struct sk_buff *, unsigned int)
// with return type: (unsigned char)*
unsigned char *skb_push(struct sk_buff *arg0, unsigned int arg1) {
  // Pointer type
  return ldv_malloc(sizeof(unsigned char));
}

// Function: skb_trim
// with type: void skb_trim(struct sk_buff *, unsigned int)
// with return type: void
void skb_trim(struct sk_buff *arg0, unsigned int arg1) {
  // Void type
  return;
}

// Function: usb_deregister
// with type: void usb_deregister(struct usb_driver *)
// with return type: void
void usb_deregister(struct usb_driver *arg0) {
  // Void type
  return;
}

// Function: usb_register_driver
// with type: int usb_register_driver(struct usb_driver *, struct module *, const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int usb_register_driver(struct usb_driver *arg0, struct module *arg1, const char *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: usb_submit_urb
// with type: int usb_submit_urb(struct urb *, gfp_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int usb_submit_urb(struct urb *arg0, gfp_t arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}