sbv-14.8: SBVTestSuite/GoldFiles/aes128Enc.gold
== BEGIN: "Makefile" ================
# Makefile for aes128Enc. Automatically generated by SBV. Do not edit!
# include any user-defined .mk file in the current directory.
-include *.mk
CC?=gcc
CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
all: aes128Enc_driver
aes128Enc.o: aes128Enc.c aes128Enc.h
${CC} ${CCFLAGS} -c $< -o $@
aes128Enc_driver.o: aes128Enc_driver.c aes128Enc.h
${CC} ${CCFLAGS} -c $< -o $@
aes128Enc_driver: aes128Enc.o aes128Enc_driver.o
${CC} ${CCFLAGS} $^ -o $@ ${LDFLAGS}
clean:
rm -f *.o
veryclean: clean
rm -f aes128Enc_driver
== END: "Makefile" ==================
== BEGIN: "aes128Enc.h" ================
/* Header file for aes128Enc. Automatically generated by SBV. Do not edit! */
#ifndef SBV_GENERATED_aes128Enc_HEADER_INCLUDED
#define SBV_GENERATED_aes128Enc_HEADER_INCLUDED
#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <math.h>
/* Floating-point calling convention:
* Enter generated code in FE_TONEAREST (round-to-nearest, ties-to-even).
* Callbacks must preserve this mode before returning or re-entering.
* Generated code does not check or change the hardware rounding mode.
* Custom builds must disable implicit FP contraction, including at LTO link time.
*/
/* The boolean type */
typedef bool SBool;
/* The float type */
typedef float SFloat;
/* The double type */
typedef double SDouble;
/* Unsigned bit-vectors */
typedef uint8_t SWord8;
typedef uint16_t SWord16;
typedef uint32_t SWord32;
typedef uint64_t SWord64;
/* Signed bit-vectors */
typedef int8_t SInt8;
typedef int16_t SInt16;
typedef int32_t SInt32;
typedef int64_t SInt64;
/* Entry point prototype: */
void aes128Enc(const SWord32 *pt, const SWord32 *key, SWord32 *ct);
#endif /* SBV_GENERATED_aes128Enc_HEADER_INCLUDED */
== END: "aes128Enc.h" ==================
== BEGIN: "aes128Enc_driver.c" ================
/* Example driver program for aes128Enc. */
/* Automatically generated by SBV. Edit as you see fit! */
#include <stdio.h>
#include "aes128Enc.h"
int main(void)
{
const SWord32 sbv_driver_input_0[4] = {
0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
};
printf("Contents of input array pt:\n");
int sbv_driver_input_0_ctr;
for(sbv_driver_input_0_ctr = 0; sbv_driver_input_0_ctr < 4 ; ++sbv_driver_input_0_ctr)
{ printf(" pt[%1d] = ", sbv_driver_input_0_ctr);
printf("0x%08"PRIx32"UL", sbv_driver_input_0[sbv_driver_input_0_ctr]);
printf("\n");
}
const SWord32 sbv_driver_input_1[4] = {
0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
};
printf("Contents of input array key:\n");
int sbv_driver_input_1_ctr;
for(sbv_driver_input_1_ctr = 0; sbv_driver_input_1_ctr < 4 ; ++sbv_driver_input_1_ctr)
{ printf(" key[%1d] = ", sbv_driver_input_1_ctr);
printf("0x%08"PRIx32"UL", sbv_driver_input_1[sbv_driver_input_1_ctr]);
printf("\n");
}
SWord32 sbv_driver_output_0[4];
aes128Enc(sbv_driver_input_0, sbv_driver_input_1,
sbv_driver_output_0);
printf("aes128Enc(pt, key, ct) ->\n");
int sbv_driver_output_0_ctr;
for(sbv_driver_output_0_ctr = 0; sbv_driver_output_0_ctr < 4 ; ++sbv_driver_output_0_ctr)
{ printf(" ct[%1d] = ", sbv_driver_output_0_ctr);
printf("0x%08"PRIx32"UL", sbv_driver_output_0[sbv_driver_output_0_ctr]);
printf("\n");
}
return 0;
}
== END: "aes128Enc_driver.c" ==================
== BEGIN: "aes128Enc.c" ================
/* File: "aes128Enc.c". Automatically generated by SBV. Do not edit! */
#include "aes128Enc.h"
/* Exact bit-vector runtime. All arithmetic is modulo the declared width. */
#ifndef SBV_CGEN_UNUSED
#if defined(__GNUC__) || defined(__clang__)
#define SBV_CGEN_UNUSED __attribute__((unused))
#else
#define SBV_CGEN_UNUSED
#endif
#endif
static inline SBV_CGEN_UNUSED SWord8 sbv_bv_extract_u32_31_24_u8(SWord32 a)
{
SWord8 r = (SWord8) 0;
uint64_t i;
for (i = 0; i < 8; ++i) { r = (SWord8) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 24)) & UINT64_C(1)) != 0) << (i))); }
return r;
}
static inline SBV_CGEN_UNUSED SWord8 sbv_bv_extract_u32_23_16_u8(SWord32 a)
{
SWord8 r = (SWord8) 0;
uint64_t i;
for (i = 0; i < 8; ++i) { r = (SWord8) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 16)) & UINT64_C(1)) != 0) << (i))); }
return r;
}
static inline SBV_CGEN_UNUSED SWord8 sbv_bv_extract_u32_15_8_u8(SWord32 a)
{
SWord8 r = (SWord8) 0;
uint64_t i;
for (i = 0; i < 8; ++i) { r = (SWord8) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i + 8)) & UINT64_C(1)) != 0) << (i))); }
return r;
}
static inline SBV_CGEN_UNUSED SWord8 sbv_bv_extract_u32_7_0_u8(SWord32 a)
{
SWord8 r = (SWord8) 0;
uint64_t i;
for (i = 0; i < 8; ++i) { r = (SWord8) ((uint64_t) r | ((uint64_t) (((((uint64_t) a) >> (i)) & UINT64_C(1)) != 0) << (i))); }
return r;
}
static inline SBV_CGEN_UNUSED SWord32 sbv_bv_u32_rotl(SWord32 a, uint64_t amount)
{
amount %= 32;
if (amount == 0) return a;
return (SWord32) ((((uint64_t) (SWord32) a) << amount) | (((uint64_t) (SWord32) a) >> (32 - amount)));
}
static inline SBV_CGEN_UNUSED SWord32 sbv_bv_u32_rotr(SWord32 a, uint64_t amount)
{
amount %= 32;
if (amount == 0) return a;
return (SWord32) ((((uint64_t) (SWord32) a) >> amount) | (((uint64_t) (SWord32) a) << (32 - amount)));
}
static inline SBV_CGEN_UNUSED SWord16 sbv_bv_join_u8_u8_u16(SWord8 high, SWord8 low)
{
SWord16 r = (SWord16) 0; uint64_t i;
for (i = 0; i < 8; ++i) { r = (SWord16) ((uint64_t) r | ((uint64_t) (((((uint64_t) low) >> (i)) & UINT64_C(1)) != 0) << (i))); }
for (i = 0; i < 8; ++i) { r = (SWord16) ((uint64_t) r | ((uint64_t) (((((uint64_t) high) >> (i)) & UINT64_C(1)) != 0) << (i + 8))); }
return r;
}
static inline SBV_CGEN_UNUSED SWord32 sbv_bv_join_u16_u16_u32(SWord16 high, SWord16 low)
{
SWord32 r = (SWord32) 0; uint64_t i;
for (i = 0; i < 16; ++i) { r = (SWord32) ((uint64_t) r | ((uint64_t) (((((uint64_t) low) >> (i)) & UINT64_C(1)) != 0) << (i))); }
for (i = 0; i < 16; ++i) { r = (SWord32) ((uint64_t) r | ((uint64_t) (((((uint64_t) high) >> (i)) & UINT64_C(1)) != 0) << (i + 16))); }
return r;
}
void aes128Enc(const SWord32 *sbv_input_0,
const SWord32 *sbv_input_1, SWord32 *sbv_output_0)
{
const SWord32 s0 = sbv_input_0[0];
const SWord32 s1 = sbv_input_0[1];
const SWord32 s2 = sbv_input_0[2];
const SWord32 s3 = sbv_input_0[3];
const SWord32 s4 = sbv_input_1[0];
const SWord32 s5 = sbv_input_1[1];
const SWord32 s6 = sbv_input_1[2];
const SWord32 s7 = sbv_input_1[3];
const SWord32 s520 = s0 ^ s4;
const SWord8 s521 = sbv_bv_extract_u32_31_24_u8(s520);
const SWord32 s778 = s1 ^ s5;
const SWord8 s779 = sbv_bv_extract_u32_23_16_u8(s778);
const SWord32 s1037 = s2 ^ s6;
const SWord8 s1038 = sbv_bv_extract_u32_15_8_u8(s1037);
const SWord32 s1296 = s3 ^ s7;
const SWord8 s1297 = sbv_bv_extract_u32_7_0_u8(s1296);
const SWord32 s1300 = sbv_bv_u32_rotl(s7, 8);
const SWord8 s1301 = sbv_bv_extract_u32_31_24_u8(s1300);
const SWord8 s1304 = sbv_bv_extract_u32_23_16_u8(s1300);
const SWord8 s1307 = sbv_bv_extract_u32_15_8_u8(s1300);
const SWord8 s1309 = sbv_bv_extract_u32_7_0_u8(s1300);
const SWord8 s1317 = sbv_bv_extract_u32_31_24_u8(s778);
const SWord8 s1319 = sbv_bv_extract_u32_23_16_u8(s1037);
const SWord8 s1322 = sbv_bv_extract_u32_15_8_u8(s1296);
const SWord8 s1325 = sbv_bv_extract_u32_7_0_u8(s520);
const SWord8 s1333 = sbv_bv_extract_u32_31_24_u8(s1037);
const SWord8 s1335 = sbv_bv_extract_u32_23_16_u8(s1296);
const SWord8 s1338 = sbv_bv_extract_u32_15_8_u8(s520);
const SWord8 s1341 = sbv_bv_extract_u32_7_0_u8(s778);
const SWord8 s1349 = sbv_bv_extract_u32_31_24_u8(s1296);
const SWord8 s1351 = sbv_bv_extract_u32_23_16_u8(s520);
const SWord8 s1354 = sbv_bv_extract_u32_15_8_u8(s778);
const SWord8 s1357 = sbv_bv_extract_u32_7_0_u8(s1037);
SWord32 s522;
SWord32 s780;
SWord32 s781;
SWord32 s1039;
SWord32 s1040;
SWord32 s1298;
SWord32 s1299;
SWord8 s1302;
SWord8 s1303;
SWord8 s1305;
SWord16 s1306;
SWord8 s1308;
SWord8 s1310;
SWord16 s1311;
SWord32 s1312;
SWord32 s1313;
SWord32 s1314;
SWord8 s1315;
SWord32 s1316;
SWord32 s1318;
SWord32 s1320;
SWord32 s1321;
SWord32 s1323;
SWord32 s1324;
SWord32 s1326;
SWord32 s1327;
SWord32 s1328;
SWord32 s1329;
SWord8 s1330;
SWord32 s1331;
SWord32 s1332;
SWord32 s1334;
SWord32 s1336;
SWord32 s1337;
SWord32 s1339;
SWord32 s1340;
SWord32 s1342;
SWord32 s1343;
SWord32 s1344;
SWord32 s1345;
SWord8 s1346;
SWord32 s1347;
SWord32 s1348;
SWord32 s1350;
SWord32 s1352;
SWord32 s1353;
SWord32 s1355;
SWord32 s1356;
SWord32 s1358;
SWord32 s1359;
SWord32 s1360;
SWord32 s1361;
SWord8 s1362;
SWord32 s1363;
SWord32 s1364;
SWord32 s1365;
SWord8 s1366;
SWord8 s1367;
SWord8 s1368;
SWord8 s1369;
SWord8 s1370;
SWord16 s1371;
SWord8 s1372;
SWord8 s1373;
SWord8 s1374;
SWord8 s1375;
SWord16 s1376;
SWord32 s1377;
SWord32 s1378;
SWord32 s1379;
SWord8 s1380;
SWord32 s1381;
SWord8 s1382;
SWord32 s1383;
SWord8 s1384;
SWord32 s1385;
SWord32 s1386;
SWord8 s1387;
SWord32 s1388;
SWord32 s1389;
SWord8 s1390;
SWord32 s1391;
SWord32 s1392;
SWord32 s1393;
SWord32 s1394;
SWord8 s1395;
SWord32 s1396;
SWord32 s1397;
SWord8 s1398;
SWord32 s1399;
SWord8 s1400;
SWord32 s1401;
SWord32 s1402;
SWord8 s1403;
SWord32 s1404;
SWord32 s1405;
SWord8 s1406;
SWord32 s1407;
SWord32 s1408;
SWord32 s1409;
SWord32 s1410;
SWord8 s1411;
SWord32 s1412;
SWord32 s1413;
SWord8 s1414;
SWord32 s1415;
SWord8 s1416;
SWord32 s1417;
SWord32 s1418;
SWord8 s1419;
SWord32 s1420;
SWord32 s1421;
SWord8 s1422;
SWord32 s1423;
SWord32 s1424;
SWord32 s1425;
SWord32 s1426;
SWord8 s1427;
SWord32 s1428;
SWord32 s1429;
SWord32 s1430;
SWord8 s1431;
SWord8 s1432;
SWord8 s1433;
SWord8 s1434;
SWord8 s1435;
SWord16 s1436;
SWord8 s1437;
SWord8 s1438;
SWord8 s1439;
SWord8 s1440;
SWord16 s1441;
SWord32 s1442;
SWord32 s1443;
SWord32 s1444;
SWord8 s1445;
SWord32 s1446;
SWord8 s1447;
SWord32 s1448;
SWord8 s1449;
SWord32 s1450;
SWord32 s1451;
SWord8 s1452;
SWord32 s1453;
SWord32 s1454;
SWord8 s1455;
SWord32 s1456;
SWord32 s1457;
SWord32 s1458;
SWord32 s1459;
SWord8 s1460;
SWord32 s1461;
SWord32 s1462;
SWord8 s1463;
SWord32 s1464;
SWord8 s1465;
SWord32 s1466;
SWord32 s1467;
SWord8 s1468;
SWord32 s1469;
SWord32 s1470;
SWord8 s1471;
SWord32 s1472;
SWord32 s1473;
SWord32 s1474;
SWord32 s1475;
SWord8 s1476;
SWord32 s1477;
SWord32 s1478;
SWord8 s1479;
SWord32 s1480;
SWord8 s1481;
SWord32 s1482;
SWord32 s1483;
SWord8 s1484;
SWord32 s1485;
SWord32 s1486;
SWord8 s1487;
SWord32 s1488;
SWord32 s1489;
SWord32 s1490;
SWord32 s1491;
SWord8 s1492;
SWord32 s1493;
SWord32 s1494;
SWord32 s1495;
SWord8 s1496;
SWord8 s1497;
SWord8 s1498;
SWord8 s1499;
SWord8 s1500;
SWord16 s1501;
SWord8 s1502;
SWord8 s1503;
SWord8 s1504;
SWord8 s1505;
SWord16 s1506;
SWord32 s1507;
SWord32 s1508;
SWord32 s1509;
SWord8 s1510;
SWord32 s1511;
SWord8 s1512;
SWord32 s1513;
SWord8 s1514;
SWord32 s1515;
SWord32 s1516;
SWord8 s1517;
SWord32 s1518;
SWord32 s1519;
SWord8 s1520;
SWord32 s1521;
SWord32 s1522;
SWord32 s1523;
SWord32 s1524;
SWord8 s1525;
SWord32 s1526;
SWord32 s1527;
SWord8 s1528;
SWord32 s1529;
SWord8 s1530;
SWord32 s1531;
SWord32 s1532;
SWord8 s1533;
SWord32 s1534;
SWord32 s1535;
SWord8 s1536;
SWord32 s1537;
SWord32 s1538;
SWord32 s1539;
SWord32 s1540;
SWord8 s1541;
SWord32 s1542;
SWord32 s1543;
SWord8 s1544;
SWord32 s1545;
SWord8 s1546;
SWord32 s1547;
SWord32 s1548;
SWord8 s1549;
SWord32 s1550;
SWord32 s1551;
SWord8 s1552;
SWord32 s1553;
SWord32 s1554;
SWord32 s1555;
SWord32 s1556;
SWord8 s1557;
SWord32 s1558;
SWord32 s1559;
SWord32 s1560;
SWord8 s1561;
SWord8 s1562;
SWord8 s1563;
SWord8 s1564;
SWord8 s1565;
SWord16 s1566;
SWord8 s1567;
SWord8 s1568;
SWord8 s1569;
SWord8 s1570;
SWord16 s1571;
SWord32 s1572;
SWord32 s1573;
SWord32 s1574;
SWord8 s1575;
SWord32 s1576;
SWord8 s1577;
SWord32 s1578;
SWord8 s1579;
SWord32 s1580;
SWord32 s1581;
SWord8 s1582;
SWord32 s1583;
SWord32 s1584;
SWord8 s1585;
SWord32 s1586;
SWord32 s1587;
SWord32 s1588;
SWord32 s1589;
SWord8 s1590;
SWord32 s1591;
SWord32 s1592;
SWord8 s1593;
SWord32 s1594;
SWord8 s1595;
SWord32 s1596;
SWord32 s1597;
SWord8 s1598;
SWord32 s1599;
SWord32 s1600;
SWord8 s1601;
SWord32 s1602;
SWord32 s1603;
SWord32 s1604;
SWord32 s1605;
SWord8 s1606;
SWord32 s1607;
SWord32 s1608;
SWord8 s1609;
SWord32 s1610;
SWord8 s1611;
SWord32 s1612;
SWord32 s1613;
SWord8 s1614;
SWord32 s1615;
SWord32 s1616;
SWord8 s1617;
SWord32 s1618;
SWord32 s1619;
SWord32 s1620;
SWord32 s1621;
SWord8 s1622;
SWord32 s1623;
SWord32 s1624;
SWord32 s1625;
SWord8 s1626;
SWord8 s1627;
SWord8 s1628;
SWord8 s1629;
SWord8 s1630;
SWord16 s1631;
SWord8 s1632;
SWord8 s1633;
SWord8 s1634;
SWord8 s1635;
SWord16 s1636;
SWord32 s1637;
SWord32 s1638;
SWord32 s1639;
SWord8 s1640;
SWord32 s1641;
SWord8 s1642;
SWord32 s1643;
SWord8 s1644;
SWord32 s1645;
SWord32 s1646;
SWord8 s1647;
SWord32 s1648;
SWord32 s1649;
SWord8 s1650;
SWord32 s1651;
SWord32 s1652;
SWord32 s1653;
SWord32 s1654;
SWord8 s1655;
SWord32 s1656;
SWord32 s1657;
SWord8 s1658;
SWord32 s1659;
SWord8 s1660;
SWord32 s1661;
SWord32 s1662;
SWord8 s1663;
SWord32 s1664;
SWord32 s1665;
SWord8 s1666;
SWord32 s1667;
SWord32 s1668;
SWord32 s1669;
SWord32 s1670;
SWord8 s1671;
SWord32 s1672;
SWord32 s1673;
SWord8 s1674;
SWord32 s1675;
SWord8 s1676;
SWord32 s1677;
SWord32 s1678;
SWord8 s1679;
SWord32 s1680;
SWord32 s1681;
SWord8 s1682;
SWord32 s1683;
SWord32 s1684;
SWord32 s1685;
SWord32 s1686;
SWord8 s1687;
SWord32 s1688;
SWord32 s1689;
SWord32 s1690;
SWord8 s1691;
SWord8 s1692;
SWord8 s1693;
SWord8 s1694;
SWord8 s1695;
SWord16 s1696;
SWord8 s1697;
SWord8 s1698;
SWord8 s1699;
SWord8 s1700;
SWord16 s1701;
SWord32 s1702;
SWord32 s1703;
SWord32 s1704;
SWord8 s1705;
SWord32 s1706;
SWord8 s1707;
SWord32 s1708;
SWord8 s1709;
SWord32 s1710;
SWord32 s1711;
SWord8 s1712;
SWord32 s1713;
SWord32 s1714;
SWord8 s1715;
SWord32 s1716;
SWord32 s1717;
SWord32 s1718;
SWord32 s1719;
SWord8 s1720;
SWord32 s1721;
SWord32 s1722;
SWord8 s1723;
SWord32 s1724;
SWord8 s1725;
SWord32 s1726;
SWord32 s1727;
SWord8 s1728;
SWord32 s1729;
SWord32 s1730;
SWord8 s1731;
SWord32 s1732;
SWord32 s1733;
SWord32 s1734;
SWord32 s1735;
SWord8 s1736;
SWord32 s1737;
SWord32 s1738;
SWord8 s1739;
SWord32 s1740;
SWord8 s1741;
SWord32 s1742;
SWord32 s1743;
SWord8 s1744;
SWord32 s1745;
SWord32 s1746;
SWord8 s1747;
SWord32 s1748;
SWord32 s1749;
SWord32 s1750;
SWord32 s1751;
SWord8 s1752;
SWord32 s1753;
SWord32 s1754;
SWord32 s1755;
SWord8 s1756;
SWord8 s1757;
SWord8 s1758;
SWord8 s1759;
SWord8 s1760;
SWord16 s1761;
SWord8 s1762;
SWord8 s1763;
SWord8 s1764;
SWord8 s1765;
SWord16 s1766;
SWord32 s1767;
SWord32 s1768;
SWord32 s1769;
SWord8 s1770;
SWord32 s1771;
SWord8 s1772;
SWord32 s1773;
SWord8 s1774;
SWord32 s1775;
SWord32 s1776;
SWord8 s1777;
SWord32 s1778;
SWord32 s1779;
SWord8 s1780;
SWord32 s1781;
SWord32 s1782;
SWord32 s1783;
SWord32 s1784;
SWord8 s1785;
SWord32 s1786;
SWord32 s1787;
SWord8 s1788;
SWord32 s1789;
SWord8 s1790;
SWord32 s1791;
SWord32 s1792;
SWord8 s1793;
SWord32 s1794;
SWord32 s1795;
SWord8 s1796;
SWord32 s1797;
SWord32 s1798;
SWord32 s1799;
SWord32 s1800;
SWord8 s1801;
SWord32 s1802;
SWord32 s1803;
SWord8 s1804;
SWord32 s1805;
SWord8 s1806;
SWord32 s1807;
SWord32 s1808;
SWord8 s1809;
SWord32 s1810;
SWord32 s1811;
SWord8 s1812;
SWord32 s1813;
SWord32 s1814;
SWord32 s1815;
SWord32 s1816;
SWord8 s1817;
SWord32 s1818;
SWord32 s1819;
SWord32 s1820;
SWord8 s1821;
SWord8 s1822;
SWord8 s1823;
SWord8 s1824;
SWord8 s1825;
SWord16 s1826;
SWord8 s1827;
SWord8 s1828;
SWord8 s1829;
SWord8 s1830;
SWord16 s1831;
SWord32 s1832;
SWord32 s1833;
SWord32 s1834;
SWord8 s1835;
SWord8 s1836;
SWord8 s1837;
SWord32 s1838;
SWord8 s1839;
SWord32 s1840;
SWord32 s1841;
SWord8 s1842;
SWord32 s1843;
SWord32 s1844;
SWord8 s1845;
SWord32 s1846;
SWord32 s1847;
SWord32 s1848;
SWord32 s1849;
SWord8 s1850;
SWord8 s1851;
SWord16 s1852;
SWord8 s1853;
SWord32 s1854;
SWord8 s1855;
SWord32 s1856;
SWord32 s1857;
SWord8 s1858;
SWord32 s1859;
SWord32 s1860;
SWord8 s1861;
SWord32 s1862;
SWord32 s1863;
SWord32 s1864;
SWord32 s1865;
SWord8 s1866;
SWord8 s1867;
SWord8 s1868;
SWord32 s1869;
SWord8 s1870;
SWord32 s1871;
SWord32 s1872;
SWord8 s1873;
SWord32 s1874;
SWord32 s1875;
SWord8 s1876;
SWord32 s1877;
SWord32 s1878;
SWord32 s1879;
SWord32 s1880;
SWord8 s1881;
SWord8 s1882;
SWord16 s1883;
SWord32 s1884;
SWord32 s1885;
SWord8 s1886;
SWord8 s1887;
SWord8 s1888;
SWord8 s1889;
SWord8 s1890;
SWord16 s1891;
SWord8 s1892;
SWord8 s1893;
SWord8 s1894;
SWord8 s1895;
SWord16 s1896;
SWord32 s1897;
SWord32 s1898;
SWord32 s1899;
SWord8 s1900;
SWord8 s1901;
SWord8 s1902;
SWord8 s1903;
SWord16 s1904;
SWord8 s1905;
SWord8 s1906;
SWord8 s1907;
SWord8 s1908;
SWord16 s1909;
SWord32 s1910;
SWord32 s1911;
SWord32 s1912;
SWord8 s1913;
SWord8 s1914;
SWord8 s1915;
SWord8 s1916;
SWord16 s1917;
SWord8 s1918;
SWord8 s1919;
SWord8 s1920;
SWord8 s1921;
SWord16 s1922;
SWord32 s1923;
SWord32 s1924;
SWord32 s1925;
SWord8 s1926;
SWord8 s1927;
SWord8 s1928;
SWord8 s1929;
SWord16 s1930;
SWord8 s1931;
SWord8 s1932;
SWord8 s1933;
SWord8 s1934;
SWord16 s1935;
SWord32 s1936;
SWord32 s1937;
SWord32 s1938;
static const SWord32 table1[] = {
0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL,
0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL,
0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL,
0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,
0x8fcaca45UL, 0x1f82829dUL, 0x89c9c940UL, 0xfa7d7d87UL,
0xeffafa15UL, 0xb25959ebUL, 0x8e4747c9UL, 0xfbf0f00bUL,
0x41adadecUL, 0xb3d4d467UL, 0x5fa2a2fdUL, 0x45afafeaUL,
0x239c9cbfUL, 0x53a4a4f7UL, 0xe4727296UL, 0x9bc0c05bUL,
0x75b7b7c2UL, 0xe1fdfd1cUL, 0x3d9393aeUL, 0x4c26266aUL,
0x6c36365aUL, 0x7e3f3f41UL, 0xf5f7f702UL, 0x83cccc4fUL,
0x6834345cUL, 0x51a5a5f4UL, 0xd1e5e534UL, 0xf9f1f108UL,
0xe2717193UL, 0xabd8d873UL, 0x62313153UL, 0x2a15153fUL,
0x0804040cUL, 0x95c7c752UL, 0x46232365UL, 0x9dc3c35eUL,
0x30181828UL, 0x379696a1UL, 0x0a05050fUL, 0x2f9a9ab5UL,
0x0e070709UL, 0x24121236UL, 0x1b80809bUL, 0xdfe2e23dUL,
0xcdebeb26UL, 0x4e272769UL, 0x7fb2b2cdUL, 0xea75759fUL,
0x1209091bUL, 0x1d83839eUL, 0x582c2c74UL, 0x341a1a2eUL,
0x361b1b2dUL, 0xdc6e6eb2UL, 0xb45a5aeeUL, 0x5ba0a0fbUL,
0xa45252f6UL, 0x763b3b4dUL, 0xb7d6d661UL, 0x7db3b3ceUL,
0x5229297bUL, 0xdde3e33eUL, 0x5e2f2f71UL, 0x13848497UL,
0xa65353f5UL, 0xb9d1d168UL, 0x00000000UL, 0xc1eded2cUL,
0x40202060UL, 0xe3fcfc1fUL, 0x79b1b1c8UL, 0xb65b5bedUL,
0xd46a6abeUL, 0x8dcbcb46UL, 0x67bebed9UL, 0x7239394bUL,
0x944a4adeUL, 0x984c4cd4UL, 0xb05858e8UL, 0x85cfcf4aUL,
0xbbd0d06bUL, 0xc5efef2aUL, 0x4faaaae5UL, 0xedfbfb16UL,
0x864343c5UL, 0x9a4d4dd7UL, 0x66333355UL, 0x11858594UL,
0x8a4545cfUL, 0xe9f9f910UL, 0x04020206UL, 0xfe7f7f81UL,
0xa05050f0UL, 0x783c3c44UL, 0x259f9fbaUL, 0x4ba8a8e3UL,
0xa25151f3UL, 0x5da3a3feUL, 0x804040c0UL, 0x058f8f8aUL,
0x3f9292adUL, 0x219d9dbcUL, 0x70383848UL, 0xf1f5f504UL,
0x63bcbcdfUL, 0x77b6b6c1UL, 0xafdada75UL, 0x42212163UL,
0x20101030UL, 0xe5ffff1aUL, 0xfdf3f30eUL, 0xbfd2d26dUL,
0x81cdcd4cUL, 0x180c0c14UL, 0x26131335UL, 0xc3ecec2fUL,
0xbe5f5fe1UL, 0x359797a2UL, 0x884444ccUL, 0x2e171739UL,
0x93c4c457UL, 0x55a7a7f2UL, 0xfc7e7e82UL, 0x7a3d3d47UL,
0xc86464acUL, 0xba5d5de7UL, 0x3219192bUL, 0xe6737395UL,
0xc06060a0UL, 0x19818198UL, 0x9e4f4fd1UL, 0xa3dcdc7fUL,
0x44222266UL, 0x542a2a7eUL, 0x3b9090abUL, 0x0b888883UL,
0x8c4646caUL, 0xc7eeee29UL, 0x6bb8b8d3UL, 0x2814143cUL,
0xa7dede79UL, 0xbc5e5ee2UL, 0x160b0b1dUL, 0xaddbdb76UL,
0xdbe0e03bUL, 0x64323256UL, 0x743a3a4eUL, 0x140a0a1eUL,
0x924949dbUL, 0x0c06060aUL, 0x4824246cUL, 0xb85c5ce4UL,
0x9fc2c25dUL, 0xbdd3d36eUL, 0x43acacefUL, 0xc46262a6UL,
0x399191a8UL, 0x319595a4UL, 0xd3e4e437UL, 0xf279798bUL,
0xd5e7e732UL, 0x8bc8c843UL, 0x6e373759UL, 0xda6d6db7UL,
0x018d8d8cUL, 0xb1d5d564UL, 0x9c4e4ed2UL, 0x49a9a9e0UL,
0xd86c6cb4UL, 0xac5656faUL, 0xf3f4f407UL, 0xcfeaea25UL,
0xca6565afUL, 0xf47a7a8eUL, 0x47aeaee9UL, 0x10080818UL,
0x6fbabad5UL, 0xf0787888UL, 0x4a25256fUL, 0x5c2e2e72UL,
0x381c1c24UL, 0x57a6a6f1UL, 0x73b4b4c7UL, 0x97c6c651UL,
0xcbe8e823UL, 0xa1dddd7cUL, 0xe874749cUL, 0x3e1f1f21UL,
0x964b4bddUL, 0x61bdbddcUL, 0x0d8b8b86UL, 0x0f8a8a85UL,
0xe0707090UL, 0x7c3e3e42UL, 0x71b5b5c4UL, 0xcc6666aaUL,
0x904848d8UL, 0x06030305UL, 0xf7f6f601UL, 0x1c0e0e12UL,
0xc26161a3UL, 0x6a35355fUL, 0xae5757f9UL, 0x69b9b9d0UL,
0x17868691UL, 0x99c1c158UL, 0x3a1d1d27UL, 0x279e9eb9UL,
0xd9e1e138UL, 0xebf8f813UL, 0x2b9898b3UL, 0x22111133UL,
0xd26969bbUL, 0xa9d9d970UL, 0x078e8e89UL, 0x339494a7UL,
0x2d9b9bb6UL, 0x3c1e1e22UL, 0x15878792UL, 0xc9e9e920UL,
0x87cece49UL, 0xaa5555ffUL, 0x50282878UL, 0xa5dfdf7aUL,
0x038c8c8fUL, 0x59a1a1f8UL, 0x09898980UL, 0x1a0d0d17UL,
0x65bfbfdaUL, 0xd7e6e631UL, 0x844242c6UL, 0xd06868b8UL,
0x824141c3UL, 0x299999b0UL, 0x5a2d2d77UL, 0x1e0f0f11UL,
0x7bb0b0cbUL, 0xa85454fcUL, 0x6dbbbbd6UL, 0x2c16163aUL
};
s522 = table1[s521];
static const SWord32 table2[] = {
0xa5c66363UL, 0x84f87c7cUL, 0x99ee7777UL, 0x8df67b7bUL,
0x0dfff2f2UL, 0xbdd66b6bUL, 0xb1de6f6fUL, 0x5491c5c5UL,
0x50603030UL, 0x03020101UL, 0xa9ce6767UL, 0x7d562b2bUL,
0x19e7fefeUL, 0x62b5d7d7UL, 0xe64dababUL, 0x9aec7676UL,
0x458fcacaUL, 0x9d1f8282UL, 0x4089c9c9UL, 0x87fa7d7dUL,
0x15effafaUL, 0xebb25959UL, 0xc98e4747UL, 0x0bfbf0f0UL,
0xec41adadUL, 0x67b3d4d4UL, 0xfd5fa2a2UL, 0xea45afafUL,
0xbf239c9cUL, 0xf753a4a4UL, 0x96e47272UL, 0x5b9bc0c0UL,
0xc275b7b7UL, 0x1ce1fdfdUL, 0xae3d9393UL, 0x6a4c2626UL,
0x5a6c3636UL, 0x417e3f3fUL, 0x02f5f7f7UL, 0x4f83ccccUL,
0x5c683434UL, 0xf451a5a5UL, 0x34d1e5e5UL, 0x08f9f1f1UL,
0x93e27171UL, 0x73abd8d8UL, 0x53623131UL, 0x3f2a1515UL,
0x0c080404UL, 0x5295c7c7UL, 0x65462323UL, 0x5e9dc3c3UL,
0x28301818UL, 0xa1379696UL, 0x0f0a0505UL, 0xb52f9a9aUL,
0x090e0707UL, 0x36241212UL, 0x9b1b8080UL, 0x3ddfe2e2UL,
0x26cdebebUL, 0x694e2727UL, 0xcd7fb2b2UL, 0x9fea7575UL,
0x1b120909UL, 0x9e1d8383UL, 0x74582c2cUL, 0x2e341a1aUL,
0x2d361b1bUL, 0xb2dc6e6eUL, 0xeeb45a5aUL, 0xfb5ba0a0UL,
0xf6a45252UL, 0x4d763b3bUL, 0x61b7d6d6UL, 0xce7db3b3UL,
0x7b522929UL, 0x3edde3e3UL, 0x715e2f2fUL, 0x97138484UL,
0xf5a65353UL, 0x68b9d1d1UL, 0x00000000UL, 0x2cc1ededUL,
0x60402020UL, 0x1fe3fcfcUL, 0xc879b1b1UL, 0xedb65b5bUL,
0xbed46a6aUL, 0x468dcbcbUL, 0xd967bebeUL, 0x4b723939UL,
0xde944a4aUL, 0xd4984c4cUL, 0xe8b05858UL, 0x4a85cfcfUL,
0x6bbbd0d0UL, 0x2ac5efefUL, 0xe54faaaaUL, 0x16edfbfbUL,
0xc5864343UL, 0xd79a4d4dUL, 0x55663333UL, 0x94118585UL,
0xcf8a4545UL, 0x10e9f9f9UL, 0x06040202UL, 0x81fe7f7fUL,
0xf0a05050UL, 0x44783c3cUL, 0xba259f9fUL, 0xe34ba8a8UL,
0xf3a25151UL, 0xfe5da3a3UL, 0xc0804040UL, 0x8a058f8fUL,
0xad3f9292UL, 0xbc219d9dUL, 0x48703838UL, 0x04f1f5f5UL,
0xdf63bcbcUL, 0xc177b6b6UL, 0x75afdadaUL, 0x63422121UL,
0x30201010UL, 0x1ae5ffffUL, 0x0efdf3f3UL, 0x6dbfd2d2UL,
0x4c81cdcdUL, 0x14180c0cUL, 0x35261313UL, 0x2fc3ececUL,
0xe1be5f5fUL, 0xa2359797UL, 0xcc884444UL, 0x392e1717UL,
0x5793c4c4UL, 0xf255a7a7UL, 0x82fc7e7eUL, 0x477a3d3dUL,
0xacc86464UL, 0xe7ba5d5dUL, 0x2b321919UL, 0x95e67373UL,
0xa0c06060UL, 0x98198181UL, 0xd19e4f4fUL, 0x7fa3dcdcUL,
0x66442222UL, 0x7e542a2aUL, 0xab3b9090UL, 0x830b8888UL,
0xca8c4646UL, 0x29c7eeeeUL, 0xd36bb8b8UL, 0x3c281414UL,
0x79a7dedeUL, 0xe2bc5e5eUL, 0x1d160b0bUL, 0x76addbdbUL,
0x3bdbe0e0UL, 0x56643232UL, 0x4e743a3aUL, 0x1e140a0aUL,
0xdb924949UL, 0x0a0c0606UL, 0x6c482424UL, 0xe4b85c5cUL,
0x5d9fc2c2UL, 0x6ebdd3d3UL, 0xef43acacUL, 0xa6c46262UL,
0xa8399191UL, 0xa4319595UL, 0x37d3e4e4UL, 0x8bf27979UL,
0x32d5e7e7UL, 0x438bc8c8UL, 0x596e3737UL, 0xb7da6d6dUL,
0x8c018d8dUL, 0x64b1d5d5UL, 0xd29c4e4eUL, 0xe049a9a9UL,
0xb4d86c6cUL, 0xfaac5656UL, 0x07f3f4f4UL, 0x25cfeaeaUL,
0xafca6565UL, 0x8ef47a7aUL, 0xe947aeaeUL, 0x18100808UL,
0xd56fbabaUL, 0x88f07878UL, 0x6f4a2525UL, 0x725c2e2eUL,
0x24381c1cUL, 0xf157a6a6UL, 0xc773b4b4UL, 0x5197c6c6UL,
0x23cbe8e8UL, 0x7ca1ddddUL, 0x9ce87474UL, 0x213e1f1fUL,
0xdd964b4bUL, 0xdc61bdbdUL, 0x860d8b8bUL, 0x850f8a8aUL,
0x90e07070UL, 0x427c3e3eUL, 0xc471b5b5UL, 0xaacc6666UL,
0xd8904848UL, 0x05060303UL, 0x01f7f6f6UL, 0x121c0e0eUL,
0xa3c26161UL, 0x5f6a3535UL, 0xf9ae5757UL, 0xd069b9b9UL,
0x91178686UL, 0x5899c1c1UL, 0x273a1d1dUL, 0xb9279e9eUL,
0x38d9e1e1UL, 0x13ebf8f8UL, 0xb32b9898UL, 0x33221111UL,
0xbbd26969UL, 0x70a9d9d9UL, 0x89078e8eUL, 0xa7339494UL,
0xb62d9b9bUL, 0x223c1e1eUL, 0x92158787UL, 0x20c9e9e9UL,
0x4987ceceUL, 0xffaa5555UL, 0x78502828UL, 0x7aa5dfdfUL,
0x8f038c8cUL, 0xf859a1a1UL, 0x80098989UL, 0x171a0d0dUL,
0xda65bfbfUL, 0x31d7e6e6UL, 0xc6844242UL, 0xb8d06868UL,
0xc3824141UL, 0xb0299999UL, 0x775a2d2dUL, 0x111e0f0fUL,
0xcb7bb0b0UL, 0xfca85454UL, 0xd66dbbbbUL, 0x3a2c1616UL
};
s780 = table2[s779];
s781 = s522 ^ s780;
static const SWord32 table3[] = {
0x63a5c663UL, 0x7c84f87cUL, 0x7799ee77UL, 0x7b8df67bUL,
0xf20dfff2UL, 0x6bbdd66bUL, 0x6fb1de6fUL, 0xc55491c5UL,
0x30506030UL, 0x01030201UL, 0x67a9ce67UL, 0x2b7d562bUL,
0xfe19e7feUL, 0xd762b5d7UL, 0xabe64dabUL, 0x769aec76UL,
0xca458fcaUL, 0x829d1f82UL, 0xc94089c9UL, 0x7d87fa7dUL,
0xfa15effaUL, 0x59ebb259UL, 0x47c98e47UL, 0xf00bfbf0UL,
0xadec41adUL, 0xd467b3d4UL, 0xa2fd5fa2UL, 0xafea45afUL,
0x9cbf239cUL, 0xa4f753a4UL, 0x7296e472UL, 0xc05b9bc0UL,
0xb7c275b7UL, 0xfd1ce1fdUL, 0x93ae3d93UL, 0x266a4c26UL,
0x365a6c36UL, 0x3f417e3fUL, 0xf702f5f7UL, 0xcc4f83ccUL,
0x345c6834UL, 0xa5f451a5UL, 0xe534d1e5UL, 0xf108f9f1UL,
0x7193e271UL, 0xd873abd8UL, 0x31536231UL, 0x153f2a15UL,
0x040c0804UL, 0xc75295c7UL, 0x23654623UL, 0xc35e9dc3UL,
0x18283018UL, 0x96a13796UL, 0x050f0a05UL, 0x9ab52f9aUL,
0x07090e07UL, 0x12362412UL, 0x809b1b80UL, 0xe23ddfe2UL,
0xeb26cdebUL, 0x27694e27UL, 0xb2cd7fb2UL, 0x759fea75UL,
0x091b1209UL, 0x839e1d83UL, 0x2c74582cUL, 0x1a2e341aUL,
0x1b2d361bUL, 0x6eb2dc6eUL, 0x5aeeb45aUL, 0xa0fb5ba0UL,
0x52f6a452UL, 0x3b4d763bUL, 0xd661b7d6UL, 0xb3ce7db3UL,
0x297b5229UL, 0xe33edde3UL, 0x2f715e2fUL, 0x84971384UL,
0x53f5a653UL, 0xd168b9d1UL, 0x00000000UL, 0xed2cc1edUL,
0x20604020UL, 0xfc1fe3fcUL, 0xb1c879b1UL, 0x5bedb65bUL,
0x6abed46aUL, 0xcb468dcbUL, 0xbed967beUL, 0x394b7239UL,
0x4ade944aUL, 0x4cd4984cUL, 0x58e8b058UL, 0xcf4a85cfUL,
0xd06bbbd0UL, 0xef2ac5efUL, 0xaae54faaUL, 0xfb16edfbUL,
0x43c58643UL, 0x4dd79a4dUL, 0x33556633UL, 0x85941185UL,
0x45cf8a45UL, 0xf910e9f9UL, 0x02060402UL, 0x7f81fe7fUL,
0x50f0a050UL, 0x3c44783cUL, 0x9fba259fUL, 0xa8e34ba8UL,
0x51f3a251UL, 0xa3fe5da3UL, 0x40c08040UL, 0x8f8a058fUL,
0x92ad3f92UL, 0x9dbc219dUL, 0x38487038UL, 0xf504f1f5UL,
0xbcdf63bcUL, 0xb6c177b6UL, 0xda75afdaUL, 0x21634221UL,
0x10302010UL, 0xff1ae5ffUL, 0xf30efdf3UL, 0xd26dbfd2UL,
0xcd4c81cdUL, 0x0c14180cUL, 0x13352613UL, 0xec2fc3ecUL,
0x5fe1be5fUL, 0x97a23597UL, 0x44cc8844UL, 0x17392e17UL,
0xc45793c4UL, 0xa7f255a7UL, 0x7e82fc7eUL, 0x3d477a3dUL,
0x64acc864UL, 0x5de7ba5dUL, 0x192b3219UL, 0x7395e673UL,
0x60a0c060UL, 0x81981981UL, 0x4fd19e4fUL, 0xdc7fa3dcUL,
0x22664422UL, 0x2a7e542aUL, 0x90ab3b90UL, 0x88830b88UL,
0x46ca8c46UL, 0xee29c7eeUL, 0xb8d36bb8UL, 0x143c2814UL,
0xde79a7deUL, 0x5ee2bc5eUL, 0x0b1d160bUL, 0xdb76addbUL,
0xe03bdbe0UL, 0x32566432UL, 0x3a4e743aUL, 0x0a1e140aUL,
0x49db9249UL, 0x060a0c06UL, 0x246c4824UL, 0x5ce4b85cUL,
0xc25d9fc2UL, 0xd36ebdd3UL, 0xacef43acUL, 0x62a6c462UL,
0x91a83991UL, 0x95a43195UL, 0xe437d3e4UL, 0x798bf279UL,
0xe732d5e7UL, 0xc8438bc8UL, 0x37596e37UL, 0x6db7da6dUL,
0x8d8c018dUL, 0xd564b1d5UL, 0x4ed29c4eUL, 0xa9e049a9UL,
0x6cb4d86cUL, 0x56faac56UL, 0xf407f3f4UL, 0xea25cfeaUL,
0x65afca65UL, 0x7a8ef47aUL, 0xaee947aeUL, 0x08181008UL,
0xbad56fbaUL, 0x7888f078UL, 0x256f4a25UL, 0x2e725c2eUL,
0x1c24381cUL, 0xa6f157a6UL, 0xb4c773b4UL, 0xc65197c6UL,
0xe823cbe8UL, 0xdd7ca1ddUL, 0x749ce874UL, 0x1f213e1fUL,
0x4bdd964bUL, 0xbddc61bdUL, 0x8b860d8bUL, 0x8a850f8aUL,
0x7090e070UL, 0x3e427c3eUL, 0xb5c471b5UL, 0x66aacc66UL,
0x48d89048UL, 0x03050603UL, 0xf601f7f6UL, 0x0e121c0eUL,
0x61a3c261UL, 0x355f6a35UL, 0x57f9ae57UL, 0xb9d069b9UL,
0x86911786UL, 0xc15899c1UL, 0x1d273a1dUL, 0x9eb9279eUL,
0xe138d9e1UL, 0xf813ebf8UL, 0x98b32b98UL, 0x11332211UL,
0x69bbd269UL, 0xd970a9d9UL, 0x8e89078eUL, 0x94a73394UL,
0x9bb62d9bUL, 0x1e223c1eUL, 0x87921587UL, 0xe920c9e9UL,
0xce4987ceUL, 0x55ffaa55UL, 0x28785028UL, 0xdf7aa5dfUL,
0x8c8f038cUL, 0xa1f859a1UL, 0x89800989UL, 0x0d171a0dUL,
0xbfda65bfUL, 0xe631d7e6UL, 0x42c68442UL, 0x68b8d068UL,
0x41c38241UL, 0x99b02999UL, 0x2d775a2dUL, 0x0f111e0fUL,
0xb0cb7bb0UL, 0x54fca854UL, 0xbbd66dbbUL, 0x163a2c16UL
};
s1039 = table3[s1038];
s1040 = s781 ^ s1039;
static const SWord32 table4[] = {
0x6363a5c6UL, 0x7c7c84f8UL, 0x777799eeUL, 0x7b7b8df6UL,
0xf2f20dffUL, 0x6b6bbdd6UL, 0x6f6fb1deUL, 0xc5c55491UL,
0x30305060UL, 0x01010302UL, 0x6767a9ceUL, 0x2b2b7d56UL,
0xfefe19e7UL, 0xd7d762b5UL, 0xababe64dUL, 0x76769aecUL,
0xcaca458fUL, 0x82829d1fUL, 0xc9c94089UL, 0x7d7d87faUL,
0xfafa15efUL, 0x5959ebb2UL, 0x4747c98eUL, 0xf0f00bfbUL,
0xadadec41UL, 0xd4d467b3UL, 0xa2a2fd5fUL, 0xafafea45UL,
0x9c9cbf23UL, 0xa4a4f753UL, 0x727296e4UL, 0xc0c05b9bUL,
0xb7b7c275UL, 0xfdfd1ce1UL, 0x9393ae3dUL, 0x26266a4cUL,
0x36365a6cUL, 0x3f3f417eUL, 0xf7f702f5UL, 0xcccc4f83UL,
0x34345c68UL, 0xa5a5f451UL, 0xe5e534d1UL, 0xf1f108f9UL,
0x717193e2UL, 0xd8d873abUL, 0x31315362UL, 0x15153f2aUL,
0x04040c08UL, 0xc7c75295UL, 0x23236546UL, 0xc3c35e9dUL,
0x18182830UL, 0x9696a137UL, 0x05050f0aUL, 0x9a9ab52fUL,
0x0707090eUL, 0x12123624UL, 0x80809b1bUL, 0xe2e23ddfUL,
0xebeb26cdUL, 0x2727694eUL, 0xb2b2cd7fUL, 0x75759feaUL,
0x09091b12UL, 0x83839e1dUL, 0x2c2c7458UL, 0x1a1a2e34UL,
0x1b1b2d36UL, 0x6e6eb2dcUL, 0x5a5aeeb4UL, 0xa0a0fb5bUL,
0x5252f6a4UL, 0x3b3b4d76UL, 0xd6d661b7UL, 0xb3b3ce7dUL,
0x29297b52UL, 0xe3e33eddUL, 0x2f2f715eUL, 0x84849713UL,
0x5353f5a6UL, 0xd1d168b9UL, 0x00000000UL, 0xeded2cc1UL,
0x20206040UL, 0xfcfc1fe3UL, 0xb1b1c879UL, 0x5b5bedb6UL,
0x6a6abed4UL, 0xcbcb468dUL, 0xbebed967UL, 0x39394b72UL,
0x4a4ade94UL, 0x4c4cd498UL, 0x5858e8b0UL, 0xcfcf4a85UL,
0xd0d06bbbUL, 0xefef2ac5UL, 0xaaaae54fUL, 0xfbfb16edUL,
0x4343c586UL, 0x4d4dd79aUL, 0x33335566UL, 0x85859411UL,
0x4545cf8aUL, 0xf9f910e9UL, 0x02020604UL, 0x7f7f81feUL,
0x5050f0a0UL, 0x3c3c4478UL, 0x9f9fba25UL, 0xa8a8e34bUL,
0x5151f3a2UL, 0xa3a3fe5dUL, 0x4040c080UL, 0x8f8f8a05UL,
0x9292ad3fUL, 0x9d9dbc21UL, 0x38384870UL, 0xf5f504f1UL,
0xbcbcdf63UL, 0xb6b6c177UL, 0xdada75afUL, 0x21216342UL,
0x10103020UL, 0xffff1ae5UL, 0xf3f30efdUL, 0xd2d26dbfUL,
0xcdcd4c81UL, 0x0c0c1418UL, 0x13133526UL, 0xecec2fc3UL,
0x5f5fe1beUL, 0x9797a235UL, 0x4444cc88UL, 0x1717392eUL,
0xc4c45793UL, 0xa7a7f255UL, 0x7e7e82fcUL, 0x3d3d477aUL,
0x6464acc8UL, 0x5d5de7baUL, 0x19192b32UL, 0x737395e6UL,
0x6060a0c0UL, 0x81819819UL, 0x4f4fd19eUL, 0xdcdc7fa3UL,
0x22226644UL, 0x2a2a7e54UL, 0x9090ab3bUL, 0x8888830bUL,
0x4646ca8cUL, 0xeeee29c7UL, 0xb8b8d36bUL, 0x14143c28UL,
0xdede79a7UL, 0x5e5ee2bcUL, 0x0b0b1d16UL, 0xdbdb76adUL,
0xe0e03bdbUL, 0x32325664UL, 0x3a3a4e74UL, 0x0a0a1e14UL,
0x4949db92UL, 0x06060a0cUL, 0x24246c48UL, 0x5c5ce4b8UL,
0xc2c25d9fUL, 0xd3d36ebdUL, 0xacacef43UL, 0x6262a6c4UL,
0x9191a839UL, 0x9595a431UL, 0xe4e437d3UL, 0x79798bf2UL,
0xe7e732d5UL, 0xc8c8438bUL, 0x3737596eUL, 0x6d6db7daUL,
0x8d8d8c01UL, 0xd5d564b1UL, 0x4e4ed29cUL, 0xa9a9e049UL,
0x6c6cb4d8UL, 0x5656faacUL, 0xf4f407f3UL, 0xeaea25cfUL,
0x6565afcaUL, 0x7a7a8ef4UL, 0xaeaee947UL, 0x08081810UL,
0xbabad56fUL, 0x787888f0UL, 0x25256f4aUL, 0x2e2e725cUL,
0x1c1c2438UL, 0xa6a6f157UL, 0xb4b4c773UL, 0xc6c65197UL,
0xe8e823cbUL, 0xdddd7ca1UL, 0x74749ce8UL, 0x1f1f213eUL,
0x4b4bdd96UL, 0xbdbddc61UL, 0x8b8b860dUL, 0x8a8a850fUL,
0x707090e0UL, 0x3e3e427cUL, 0xb5b5c471UL, 0x6666aaccUL,
0x4848d890UL, 0x03030506UL, 0xf6f601f7UL, 0x0e0e121cUL,
0x6161a3c2UL, 0x35355f6aUL, 0x5757f9aeUL, 0xb9b9d069UL,
0x86869117UL, 0xc1c15899UL, 0x1d1d273aUL, 0x9e9eb927UL,
0xe1e138d9UL, 0xf8f813ebUL, 0x9898b32bUL, 0x11113322UL,
0x6969bbd2UL, 0xd9d970a9UL, 0x8e8e8907UL, 0x9494a733UL,
0x9b9bb62dUL, 0x1e1e223cUL, 0x87879215UL, 0xe9e920c9UL,
0xcece4987UL, 0x5555ffaaUL, 0x28287850UL, 0xdfdf7aa5UL,
0x8c8c8f03UL, 0xa1a1f859UL, 0x89898009UL, 0x0d0d171aUL,
0xbfbfda65UL, 0xe6e631d7UL, 0x4242c684UL, 0x6868b8d0UL,
0x4141c382UL, 0x9999b029UL, 0x2d2d775aUL, 0x0f0f111eUL,
0xb0b0cb7bUL, 0x5454fca8UL, 0xbbbbd66dUL, 0x16163a2cUL
};
s1298 = table4[s1297];
s1299 = s1040 ^ s1298;
static const SWord8 table0[] = {
99, 124, 119, 123, 242, 107, 111, 197, 48, 1, 103, 43, 254,
215, 171, 118, 202, 130, 201, 125, 250, 89, 71, 240, 173, 212,
162, 175, 156, 164, 114, 192, 183, 253, 147, 38, 54, 63, 247,
204, 52, 165, 229, 241, 113, 216, 49, 21, 4, 199, 35, 195,
24, 150, 5, 154, 7, 18, 128, 226, 235, 39, 178, 117, 9,
131, 44, 26, 27, 110, 90, 160, 82, 59, 214, 179, 41, 227,
47, 132, 83, 209, 0, 237, 32, 252, 177, 91, 106, 203, 190,
57, 74, 76, 88, 207, 208, 239, 170, 251, 67, 77, 51, 133,
69, 249, 2, 127, 80, 60, 159, 168, 81, 163, 64, 143, 146,
157, 56, 245, 188, 182, 218, 33, 16, 255, 243, 210, 205, 12,
19, 236, 95, 151, 68, 23, 196, 167, 126, 61, 100, 93, 25,
115, 96, 129, 79, 220, 34, 42, 144, 136, 70, 238, 184, 20,
222, 94, 11, 219, 224, 50, 58, 10, 73, 6, 36, 92, 194,
211, 172, 98, 145, 149, 228, 121, 231, 200, 55, 109, 141, 213,
78, 169, 108, 86, 244, 234, 101, 122, 174, 8, 186, 120, 37,
46, 28, 166, 180, 198, 232, 221, 116, 31, 75, 189, 139, 138,
112, 62, 181, 102, 72, 3, 246, 14, 97, 53, 87, 185, 134,
193, 29, 158, 225, 248, 152, 17, 105, 217, 142, 148, 155, 30,
135, 233, 206, 85, 40, 223, 140, 161, 137, 13, 191, 230, 66,
104, 65, 153, 45, 15, 176, 84, 187, 22
};
s1302 = table0[s1301];
s1303 = 1 ^ s1302;
s1305 = table0[s1304];
s1306 = sbv_bv_join_u8_u8_u16(s1303, s1305);
s1308 = table0[s1307];
s1310 = table0[s1309];
s1311 = sbv_bv_join_u8_u8_u16(s1308, s1310);
s1312 = sbv_bv_join_u16_u16_u32(s1306, s1311);
s1313 = s4 ^ s1312;
s1314 = s1299 ^ s1313;
s1315 = sbv_bv_extract_u32_31_24_u8(s1314);
s1316 = table1[s1315];
s1318 = table1[s1317];
s1320 = table2[s1319];
s1321 = s1318 ^ s1320;
s1323 = table3[s1322];
s1324 = s1321 ^ s1323;
s1326 = table4[s1325];
s1327 = s1324 ^ s1326;
s1328 = s5 ^ s1313;
s1329 = s1327 ^ s1328;
s1330 = sbv_bv_extract_u32_23_16_u8(s1329);
s1331 = table2[s1330];
s1332 = s1316 ^ s1331;
s1334 = table1[s1333];
s1336 = table2[s1335];
s1337 = s1334 ^ s1336;
s1339 = table3[s1338];
s1340 = s1337 ^ s1339;
s1342 = table4[s1341];
s1343 = s1340 ^ s1342;
s1344 = s6 ^ s1328;
s1345 = s1343 ^ s1344;
s1346 = sbv_bv_extract_u32_15_8_u8(s1345);
s1347 = table3[s1346];
s1348 = s1332 ^ s1347;
s1350 = table1[s1349];
s1352 = table2[s1351];
s1353 = s1350 ^ s1352;
s1355 = table3[s1354];
s1356 = s1353 ^ s1355;
s1358 = table4[s1357];
s1359 = s1356 ^ s1358;
s1360 = s7 ^ s1344;
s1361 = s1359 ^ s1360;
s1362 = sbv_bv_extract_u32_7_0_u8(s1361);
s1363 = table4[s1362];
s1364 = s1348 ^ s1363;
s1365 = sbv_bv_u32_rotl(s1360, 8);
s1366 = sbv_bv_extract_u32_31_24_u8(s1365);
s1367 = table0[s1366];
s1368 = 2 ^ s1367;
s1369 = sbv_bv_extract_u32_23_16_u8(s1365);
s1370 = table0[s1369];
s1371 = sbv_bv_join_u8_u8_u16(s1368, s1370);
s1372 = sbv_bv_extract_u32_15_8_u8(s1365);
s1373 = table0[s1372];
s1374 = sbv_bv_extract_u32_7_0_u8(s1365);
s1375 = table0[s1374];
s1376 = sbv_bv_join_u8_u8_u16(s1373, s1375);
s1377 = sbv_bv_join_u16_u16_u32(s1371, s1376);
s1378 = s1313 ^ s1377;
s1379 = s1364 ^ s1378;
s1380 = sbv_bv_extract_u32_31_24_u8(s1379);
s1381 = table1[s1380];
s1382 = sbv_bv_extract_u32_31_24_u8(s1329);
s1383 = table1[s1382];
s1384 = sbv_bv_extract_u32_23_16_u8(s1345);
s1385 = table2[s1384];
s1386 = s1383 ^ s1385;
s1387 = sbv_bv_extract_u32_15_8_u8(s1361);
s1388 = table3[s1387];
s1389 = s1386 ^ s1388;
s1390 = sbv_bv_extract_u32_7_0_u8(s1314);
s1391 = table4[s1390];
s1392 = s1389 ^ s1391;
s1393 = s1328 ^ s1378;
s1394 = s1392 ^ s1393;
s1395 = sbv_bv_extract_u32_23_16_u8(s1394);
s1396 = table2[s1395];
s1397 = s1381 ^ s1396;
s1398 = sbv_bv_extract_u32_31_24_u8(s1345);
s1399 = table1[s1398];
s1400 = sbv_bv_extract_u32_23_16_u8(s1361);
s1401 = table2[s1400];
s1402 = s1399 ^ s1401;
s1403 = sbv_bv_extract_u32_15_8_u8(s1314);
s1404 = table3[s1403];
s1405 = s1402 ^ s1404;
s1406 = sbv_bv_extract_u32_7_0_u8(s1329);
s1407 = table4[s1406];
s1408 = s1405 ^ s1407;
s1409 = s1344 ^ s1393;
s1410 = s1408 ^ s1409;
s1411 = sbv_bv_extract_u32_15_8_u8(s1410);
s1412 = table3[s1411];
s1413 = s1397 ^ s1412;
s1414 = sbv_bv_extract_u32_31_24_u8(s1361);
s1415 = table1[s1414];
s1416 = sbv_bv_extract_u32_23_16_u8(s1314);
s1417 = table2[s1416];
s1418 = s1415 ^ s1417;
s1419 = sbv_bv_extract_u32_15_8_u8(s1329);
s1420 = table3[s1419];
s1421 = s1418 ^ s1420;
s1422 = sbv_bv_extract_u32_7_0_u8(s1345);
s1423 = table4[s1422];
s1424 = s1421 ^ s1423;
s1425 = s1360 ^ s1409;
s1426 = s1424 ^ s1425;
s1427 = sbv_bv_extract_u32_7_0_u8(s1426);
s1428 = table4[s1427];
s1429 = s1413 ^ s1428;
s1430 = sbv_bv_u32_rotl(s1425, 8);
s1431 = sbv_bv_extract_u32_31_24_u8(s1430);
s1432 = table0[s1431];
s1433 = 4 ^ s1432;
s1434 = sbv_bv_extract_u32_23_16_u8(s1430);
s1435 = table0[s1434];
s1436 = sbv_bv_join_u8_u8_u16(s1433, s1435);
s1437 = sbv_bv_extract_u32_15_8_u8(s1430);
s1438 = table0[s1437];
s1439 = sbv_bv_extract_u32_7_0_u8(s1430);
s1440 = table0[s1439];
s1441 = sbv_bv_join_u8_u8_u16(s1438, s1440);
s1442 = sbv_bv_join_u16_u16_u32(s1436, s1441);
s1443 = s1378 ^ s1442;
s1444 = s1429 ^ s1443;
s1445 = sbv_bv_extract_u32_31_24_u8(s1444);
s1446 = table1[s1445];
s1447 = sbv_bv_extract_u32_31_24_u8(s1394);
s1448 = table1[s1447];
s1449 = sbv_bv_extract_u32_23_16_u8(s1410);
s1450 = table2[s1449];
s1451 = s1448 ^ s1450;
s1452 = sbv_bv_extract_u32_15_8_u8(s1426);
s1453 = table3[s1452];
s1454 = s1451 ^ s1453;
s1455 = sbv_bv_extract_u32_7_0_u8(s1379);
s1456 = table4[s1455];
s1457 = s1454 ^ s1456;
s1458 = s1393 ^ s1443;
s1459 = s1457 ^ s1458;
s1460 = sbv_bv_extract_u32_23_16_u8(s1459);
s1461 = table2[s1460];
s1462 = s1446 ^ s1461;
s1463 = sbv_bv_extract_u32_31_24_u8(s1410);
s1464 = table1[s1463];
s1465 = sbv_bv_extract_u32_23_16_u8(s1426);
s1466 = table2[s1465];
s1467 = s1464 ^ s1466;
s1468 = sbv_bv_extract_u32_15_8_u8(s1379);
s1469 = table3[s1468];
s1470 = s1467 ^ s1469;
s1471 = sbv_bv_extract_u32_7_0_u8(s1394);
s1472 = table4[s1471];
s1473 = s1470 ^ s1472;
s1474 = s1409 ^ s1458;
s1475 = s1473 ^ s1474;
s1476 = sbv_bv_extract_u32_15_8_u8(s1475);
s1477 = table3[s1476];
s1478 = s1462 ^ s1477;
s1479 = sbv_bv_extract_u32_31_24_u8(s1426);
s1480 = table1[s1479];
s1481 = sbv_bv_extract_u32_23_16_u8(s1379);
s1482 = table2[s1481];
s1483 = s1480 ^ s1482;
s1484 = sbv_bv_extract_u32_15_8_u8(s1394);
s1485 = table3[s1484];
s1486 = s1483 ^ s1485;
s1487 = sbv_bv_extract_u32_7_0_u8(s1410);
s1488 = table4[s1487];
s1489 = s1486 ^ s1488;
s1490 = s1425 ^ s1474;
s1491 = s1489 ^ s1490;
s1492 = sbv_bv_extract_u32_7_0_u8(s1491);
s1493 = table4[s1492];
s1494 = s1478 ^ s1493;
s1495 = sbv_bv_u32_rotl(s1490, 8);
s1496 = sbv_bv_extract_u32_31_24_u8(s1495);
s1497 = table0[s1496];
s1498 = 8 ^ s1497;
s1499 = sbv_bv_extract_u32_23_16_u8(s1495);
s1500 = table0[s1499];
s1501 = sbv_bv_join_u8_u8_u16(s1498, s1500);
s1502 = sbv_bv_extract_u32_15_8_u8(s1495);
s1503 = table0[s1502];
s1504 = sbv_bv_extract_u32_7_0_u8(s1495);
s1505 = table0[s1504];
s1506 = sbv_bv_join_u8_u8_u16(s1503, s1505);
s1507 = sbv_bv_join_u16_u16_u32(s1501, s1506);
s1508 = s1443 ^ s1507;
s1509 = s1494 ^ s1508;
s1510 = sbv_bv_extract_u32_31_24_u8(s1509);
s1511 = table1[s1510];
s1512 = sbv_bv_extract_u32_31_24_u8(s1459);
s1513 = table1[s1512];
s1514 = sbv_bv_extract_u32_23_16_u8(s1475);
s1515 = table2[s1514];
s1516 = s1513 ^ s1515;
s1517 = sbv_bv_extract_u32_15_8_u8(s1491);
s1518 = table3[s1517];
s1519 = s1516 ^ s1518;
s1520 = sbv_bv_extract_u32_7_0_u8(s1444);
s1521 = table4[s1520];
s1522 = s1519 ^ s1521;
s1523 = s1458 ^ s1508;
s1524 = s1522 ^ s1523;
s1525 = sbv_bv_extract_u32_23_16_u8(s1524);
s1526 = table2[s1525];
s1527 = s1511 ^ s1526;
s1528 = sbv_bv_extract_u32_31_24_u8(s1475);
s1529 = table1[s1528];
s1530 = sbv_bv_extract_u32_23_16_u8(s1491);
s1531 = table2[s1530];
s1532 = s1529 ^ s1531;
s1533 = sbv_bv_extract_u32_15_8_u8(s1444);
s1534 = table3[s1533];
s1535 = s1532 ^ s1534;
s1536 = sbv_bv_extract_u32_7_0_u8(s1459);
s1537 = table4[s1536];
s1538 = s1535 ^ s1537;
s1539 = s1474 ^ s1523;
s1540 = s1538 ^ s1539;
s1541 = sbv_bv_extract_u32_15_8_u8(s1540);
s1542 = table3[s1541];
s1543 = s1527 ^ s1542;
s1544 = sbv_bv_extract_u32_31_24_u8(s1491);
s1545 = table1[s1544];
s1546 = sbv_bv_extract_u32_23_16_u8(s1444);
s1547 = table2[s1546];
s1548 = s1545 ^ s1547;
s1549 = sbv_bv_extract_u32_15_8_u8(s1459);
s1550 = table3[s1549];
s1551 = s1548 ^ s1550;
s1552 = sbv_bv_extract_u32_7_0_u8(s1475);
s1553 = table4[s1552];
s1554 = s1551 ^ s1553;
s1555 = s1490 ^ s1539;
s1556 = s1554 ^ s1555;
s1557 = sbv_bv_extract_u32_7_0_u8(s1556);
s1558 = table4[s1557];
s1559 = s1543 ^ s1558;
s1560 = sbv_bv_u32_rotl(s1555, 8);
s1561 = sbv_bv_extract_u32_31_24_u8(s1560);
s1562 = table0[s1561];
s1563 = 16 ^ s1562;
s1564 = sbv_bv_extract_u32_23_16_u8(s1560);
s1565 = table0[s1564];
s1566 = sbv_bv_join_u8_u8_u16(s1563, s1565);
s1567 = sbv_bv_extract_u32_15_8_u8(s1560);
s1568 = table0[s1567];
s1569 = sbv_bv_extract_u32_7_0_u8(s1560);
s1570 = table0[s1569];
s1571 = sbv_bv_join_u8_u8_u16(s1568, s1570);
s1572 = sbv_bv_join_u16_u16_u32(s1566, s1571);
s1573 = s1508 ^ s1572;
s1574 = s1559 ^ s1573;
s1575 = sbv_bv_extract_u32_31_24_u8(s1574);
s1576 = table1[s1575];
s1577 = sbv_bv_extract_u32_31_24_u8(s1524);
s1578 = table1[s1577];
s1579 = sbv_bv_extract_u32_23_16_u8(s1540);
s1580 = table2[s1579];
s1581 = s1578 ^ s1580;
s1582 = sbv_bv_extract_u32_15_8_u8(s1556);
s1583 = table3[s1582];
s1584 = s1581 ^ s1583;
s1585 = sbv_bv_extract_u32_7_0_u8(s1509);
s1586 = table4[s1585];
s1587 = s1584 ^ s1586;
s1588 = s1523 ^ s1573;
s1589 = s1587 ^ s1588;
s1590 = sbv_bv_extract_u32_23_16_u8(s1589);
s1591 = table2[s1590];
s1592 = s1576 ^ s1591;
s1593 = sbv_bv_extract_u32_31_24_u8(s1540);
s1594 = table1[s1593];
s1595 = sbv_bv_extract_u32_23_16_u8(s1556);
s1596 = table2[s1595];
s1597 = s1594 ^ s1596;
s1598 = sbv_bv_extract_u32_15_8_u8(s1509);
s1599 = table3[s1598];
s1600 = s1597 ^ s1599;
s1601 = sbv_bv_extract_u32_7_0_u8(s1524);
s1602 = table4[s1601];
s1603 = s1600 ^ s1602;
s1604 = s1539 ^ s1588;
s1605 = s1603 ^ s1604;
s1606 = sbv_bv_extract_u32_15_8_u8(s1605);
s1607 = table3[s1606];
s1608 = s1592 ^ s1607;
s1609 = sbv_bv_extract_u32_31_24_u8(s1556);
s1610 = table1[s1609];
s1611 = sbv_bv_extract_u32_23_16_u8(s1509);
s1612 = table2[s1611];
s1613 = s1610 ^ s1612;
s1614 = sbv_bv_extract_u32_15_8_u8(s1524);
s1615 = table3[s1614];
s1616 = s1613 ^ s1615;
s1617 = sbv_bv_extract_u32_7_0_u8(s1540);
s1618 = table4[s1617];
s1619 = s1616 ^ s1618;
s1620 = s1555 ^ s1604;
s1621 = s1619 ^ s1620;
s1622 = sbv_bv_extract_u32_7_0_u8(s1621);
s1623 = table4[s1622];
s1624 = s1608 ^ s1623;
s1625 = sbv_bv_u32_rotl(s1620, 8);
s1626 = sbv_bv_extract_u32_31_24_u8(s1625);
s1627 = table0[s1626];
s1628 = 32 ^ s1627;
s1629 = sbv_bv_extract_u32_23_16_u8(s1625);
s1630 = table0[s1629];
s1631 = sbv_bv_join_u8_u8_u16(s1628, s1630);
s1632 = sbv_bv_extract_u32_15_8_u8(s1625);
s1633 = table0[s1632];
s1634 = sbv_bv_extract_u32_7_0_u8(s1625);
s1635 = table0[s1634];
s1636 = sbv_bv_join_u8_u8_u16(s1633, s1635);
s1637 = sbv_bv_join_u16_u16_u32(s1631, s1636);
s1638 = s1573 ^ s1637;
s1639 = s1624 ^ s1638;
s1640 = sbv_bv_extract_u32_31_24_u8(s1639);
s1641 = table1[s1640];
s1642 = sbv_bv_extract_u32_31_24_u8(s1589);
s1643 = table1[s1642];
s1644 = sbv_bv_extract_u32_23_16_u8(s1605);
s1645 = table2[s1644];
s1646 = s1643 ^ s1645;
s1647 = sbv_bv_extract_u32_15_8_u8(s1621);
s1648 = table3[s1647];
s1649 = s1646 ^ s1648;
s1650 = sbv_bv_extract_u32_7_0_u8(s1574);
s1651 = table4[s1650];
s1652 = s1649 ^ s1651;
s1653 = s1588 ^ s1638;
s1654 = s1652 ^ s1653;
s1655 = sbv_bv_extract_u32_23_16_u8(s1654);
s1656 = table2[s1655];
s1657 = s1641 ^ s1656;
s1658 = sbv_bv_extract_u32_31_24_u8(s1605);
s1659 = table1[s1658];
s1660 = sbv_bv_extract_u32_23_16_u8(s1621);
s1661 = table2[s1660];
s1662 = s1659 ^ s1661;
s1663 = sbv_bv_extract_u32_15_8_u8(s1574);
s1664 = table3[s1663];
s1665 = s1662 ^ s1664;
s1666 = sbv_bv_extract_u32_7_0_u8(s1589);
s1667 = table4[s1666];
s1668 = s1665 ^ s1667;
s1669 = s1604 ^ s1653;
s1670 = s1668 ^ s1669;
s1671 = sbv_bv_extract_u32_15_8_u8(s1670);
s1672 = table3[s1671];
s1673 = s1657 ^ s1672;
s1674 = sbv_bv_extract_u32_31_24_u8(s1621);
s1675 = table1[s1674];
s1676 = sbv_bv_extract_u32_23_16_u8(s1574);
s1677 = table2[s1676];
s1678 = s1675 ^ s1677;
s1679 = sbv_bv_extract_u32_15_8_u8(s1589);
s1680 = table3[s1679];
s1681 = s1678 ^ s1680;
s1682 = sbv_bv_extract_u32_7_0_u8(s1605);
s1683 = table4[s1682];
s1684 = s1681 ^ s1683;
s1685 = s1620 ^ s1669;
s1686 = s1684 ^ s1685;
s1687 = sbv_bv_extract_u32_7_0_u8(s1686);
s1688 = table4[s1687];
s1689 = s1673 ^ s1688;
s1690 = sbv_bv_u32_rotl(s1685, 8);
s1691 = sbv_bv_extract_u32_31_24_u8(s1690);
s1692 = table0[s1691];
s1693 = 64 ^ s1692;
s1694 = sbv_bv_extract_u32_23_16_u8(s1690);
s1695 = table0[s1694];
s1696 = sbv_bv_join_u8_u8_u16(s1693, s1695);
s1697 = sbv_bv_extract_u32_15_8_u8(s1690);
s1698 = table0[s1697];
s1699 = sbv_bv_extract_u32_7_0_u8(s1690);
s1700 = table0[s1699];
s1701 = sbv_bv_join_u8_u8_u16(s1698, s1700);
s1702 = sbv_bv_join_u16_u16_u32(s1696, s1701);
s1703 = s1638 ^ s1702;
s1704 = s1689 ^ s1703;
s1705 = sbv_bv_extract_u32_31_24_u8(s1704);
s1706 = table1[s1705];
s1707 = sbv_bv_extract_u32_31_24_u8(s1654);
s1708 = table1[s1707];
s1709 = sbv_bv_extract_u32_23_16_u8(s1670);
s1710 = table2[s1709];
s1711 = s1708 ^ s1710;
s1712 = sbv_bv_extract_u32_15_8_u8(s1686);
s1713 = table3[s1712];
s1714 = s1711 ^ s1713;
s1715 = sbv_bv_extract_u32_7_0_u8(s1639);
s1716 = table4[s1715];
s1717 = s1714 ^ s1716;
s1718 = s1653 ^ s1703;
s1719 = s1717 ^ s1718;
s1720 = sbv_bv_extract_u32_23_16_u8(s1719);
s1721 = table2[s1720];
s1722 = s1706 ^ s1721;
s1723 = sbv_bv_extract_u32_31_24_u8(s1670);
s1724 = table1[s1723];
s1725 = sbv_bv_extract_u32_23_16_u8(s1686);
s1726 = table2[s1725];
s1727 = s1724 ^ s1726;
s1728 = sbv_bv_extract_u32_15_8_u8(s1639);
s1729 = table3[s1728];
s1730 = s1727 ^ s1729;
s1731 = sbv_bv_extract_u32_7_0_u8(s1654);
s1732 = table4[s1731];
s1733 = s1730 ^ s1732;
s1734 = s1669 ^ s1718;
s1735 = s1733 ^ s1734;
s1736 = sbv_bv_extract_u32_15_8_u8(s1735);
s1737 = table3[s1736];
s1738 = s1722 ^ s1737;
s1739 = sbv_bv_extract_u32_31_24_u8(s1686);
s1740 = table1[s1739];
s1741 = sbv_bv_extract_u32_23_16_u8(s1639);
s1742 = table2[s1741];
s1743 = s1740 ^ s1742;
s1744 = sbv_bv_extract_u32_15_8_u8(s1654);
s1745 = table3[s1744];
s1746 = s1743 ^ s1745;
s1747 = sbv_bv_extract_u32_7_0_u8(s1670);
s1748 = table4[s1747];
s1749 = s1746 ^ s1748;
s1750 = s1685 ^ s1734;
s1751 = s1749 ^ s1750;
s1752 = sbv_bv_extract_u32_7_0_u8(s1751);
s1753 = table4[s1752];
s1754 = s1738 ^ s1753;
s1755 = sbv_bv_u32_rotl(s1750, 8);
s1756 = sbv_bv_extract_u32_31_24_u8(s1755);
s1757 = table0[s1756];
s1758 = 128 ^ s1757;
s1759 = sbv_bv_extract_u32_23_16_u8(s1755);
s1760 = table0[s1759];
s1761 = sbv_bv_join_u8_u8_u16(s1758, s1760);
s1762 = sbv_bv_extract_u32_15_8_u8(s1755);
s1763 = table0[s1762];
s1764 = sbv_bv_extract_u32_7_0_u8(s1755);
s1765 = table0[s1764];
s1766 = sbv_bv_join_u8_u8_u16(s1763, s1765);
s1767 = sbv_bv_join_u16_u16_u32(s1761, s1766);
s1768 = s1703 ^ s1767;
s1769 = s1754 ^ s1768;
s1770 = sbv_bv_extract_u32_31_24_u8(s1769);
s1771 = table1[s1770];
s1772 = sbv_bv_extract_u32_31_24_u8(s1719);
s1773 = table1[s1772];
s1774 = sbv_bv_extract_u32_23_16_u8(s1735);
s1775 = table2[s1774];
s1776 = s1773 ^ s1775;
s1777 = sbv_bv_extract_u32_15_8_u8(s1751);
s1778 = table3[s1777];
s1779 = s1776 ^ s1778;
s1780 = sbv_bv_extract_u32_7_0_u8(s1704);
s1781 = table4[s1780];
s1782 = s1779 ^ s1781;
s1783 = s1718 ^ s1768;
s1784 = s1782 ^ s1783;
s1785 = sbv_bv_extract_u32_23_16_u8(s1784);
s1786 = table2[s1785];
s1787 = s1771 ^ s1786;
s1788 = sbv_bv_extract_u32_31_24_u8(s1735);
s1789 = table1[s1788];
s1790 = sbv_bv_extract_u32_23_16_u8(s1751);
s1791 = table2[s1790];
s1792 = s1789 ^ s1791;
s1793 = sbv_bv_extract_u32_15_8_u8(s1704);
s1794 = table3[s1793];
s1795 = s1792 ^ s1794;
s1796 = sbv_bv_extract_u32_7_0_u8(s1719);
s1797 = table4[s1796];
s1798 = s1795 ^ s1797;
s1799 = s1734 ^ s1783;
s1800 = s1798 ^ s1799;
s1801 = sbv_bv_extract_u32_15_8_u8(s1800);
s1802 = table3[s1801];
s1803 = s1787 ^ s1802;
s1804 = sbv_bv_extract_u32_31_24_u8(s1751);
s1805 = table1[s1804];
s1806 = sbv_bv_extract_u32_23_16_u8(s1704);
s1807 = table2[s1806];
s1808 = s1805 ^ s1807;
s1809 = sbv_bv_extract_u32_15_8_u8(s1719);
s1810 = table3[s1809];
s1811 = s1808 ^ s1810;
s1812 = sbv_bv_extract_u32_7_0_u8(s1735);
s1813 = table4[s1812];
s1814 = s1811 ^ s1813;
s1815 = s1750 ^ s1799;
s1816 = s1814 ^ s1815;
s1817 = sbv_bv_extract_u32_7_0_u8(s1816);
s1818 = table4[s1817];
s1819 = s1803 ^ s1818;
s1820 = sbv_bv_u32_rotl(s1815, 8);
s1821 = sbv_bv_extract_u32_31_24_u8(s1820);
s1822 = table0[s1821];
s1823 = 27 ^ s1822;
s1824 = sbv_bv_extract_u32_23_16_u8(s1820);
s1825 = table0[s1824];
s1826 = sbv_bv_join_u8_u8_u16(s1823, s1825);
s1827 = sbv_bv_extract_u32_15_8_u8(s1820);
s1828 = table0[s1827];
s1829 = sbv_bv_extract_u32_7_0_u8(s1820);
s1830 = table0[s1829];
s1831 = sbv_bv_join_u8_u8_u16(s1828, s1830);
s1832 = sbv_bv_join_u16_u16_u32(s1826, s1831);
s1833 = s1768 ^ s1832;
s1834 = s1819 ^ s1833;
s1835 = sbv_bv_extract_u32_31_24_u8(s1834);
s1836 = table0[s1835];
s1837 = sbv_bv_extract_u32_31_24_u8(s1784);
s1838 = table1[s1837];
s1839 = sbv_bv_extract_u32_23_16_u8(s1800);
s1840 = table2[s1839];
s1841 = s1838 ^ s1840;
s1842 = sbv_bv_extract_u32_15_8_u8(s1816);
s1843 = table3[s1842];
s1844 = s1841 ^ s1843;
s1845 = sbv_bv_extract_u32_7_0_u8(s1769);
s1846 = table4[s1845];
s1847 = s1844 ^ s1846;
s1848 = s1783 ^ s1833;
s1849 = s1847 ^ s1848;
s1850 = sbv_bv_extract_u32_23_16_u8(s1849);
s1851 = table0[s1850];
s1852 = sbv_bv_join_u8_u8_u16(s1836, s1851);
s1853 = sbv_bv_extract_u32_31_24_u8(s1800);
s1854 = table1[s1853];
s1855 = sbv_bv_extract_u32_23_16_u8(s1816);
s1856 = table2[s1855];
s1857 = s1854 ^ s1856;
s1858 = sbv_bv_extract_u32_15_8_u8(s1769);
s1859 = table3[s1858];
s1860 = s1857 ^ s1859;
s1861 = sbv_bv_extract_u32_7_0_u8(s1784);
s1862 = table4[s1861];
s1863 = s1860 ^ s1862;
s1864 = s1799 ^ s1848;
s1865 = s1863 ^ s1864;
s1866 = sbv_bv_extract_u32_15_8_u8(s1865);
s1867 = table0[s1866];
s1868 = sbv_bv_extract_u32_31_24_u8(s1816);
s1869 = table1[s1868];
s1870 = sbv_bv_extract_u32_23_16_u8(s1769);
s1871 = table2[s1870];
s1872 = s1869 ^ s1871;
s1873 = sbv_bv_extract_u32_15_8_u8(s1784);
s1874 = table3[s1873];
s1875 = s1872 ^ s1874;
s1876 = sbv_bv_extract_u32_7_0_u8(s1800);
s1877 = table4[s1876];
s1878 = s1875 ^ s1877;
s1879 = s1815 ^ s1864;
s1880 = s1878 ^ s1879;
s1881 = sbv_bv_extract_u32_7_0_u8(s1880);
s1882 = table0[s1881];
s1883 = sbv_bv_join_u8_u8_u16(s1867, s1882);
s1884 = sbv_bv_join_u16_u16_u32(s1852, s1883);
s1885 = sbv_bv_u32_rotl(s1879, 8);
s1886 = sbv_bv_extract_u32_31_24_u8(s1885);
s1887 = table0[s1886];
s1888 = 54 ^ s1887;
s1889 = sbv_bv_extract_u32_23_16_u8(s1885);
s1890 = table0[s1889];
s1891 = sbv_bv_join_u8_u8_u16(s1888, s1890);
s1892 = sbv_bv_extract_u32_15_8_u8(s1885);
s1893 = table0[s1892];
s1894 = sbv_bv_extract_u32_7_0_u8(s1885);
s1895 = table0[s1894];
s1896 = sbv_bv_join_u8_u8_u16(s1893, s1895);
s1897 = sbv_bv_join_u16_u16_u32(s1891, s1896);
s1898 = s1833 ^ s1897;
s1899 = s1884 ^ s1898;
s1900 = sbv_bv_extract_u32_31_24_u8(s1849);
s1901 = table0[s1900];
s1902 = sbv_bv_extract_u32_23_16_u8(s1865);
s1903 = table0[s1902];
s1904 = sbv_bv_join_u8_u8_u16(s1901, s1903);
s1905 = sbv_bv_extract_u32_15_8_u8(s1880);
s1906 = table0[s1905];
s1907 = sbv_bv_extract_u32_7_0_u8(s1834);
s1908 = table0[s1907];
s1909 = sbv_bv_join_u8_u8_u16(s1906, s1908);
s1910 = sbv_bv_join_u16_u16_u32(s1904, s1909);
s1911 = s1848 ^ s1898;
s1912 = s1910 ^ s1911;
s1913 = sbv_bv_extract_u32_31_24_u8(s1865);
s1914 = table0[s1913];
s1915 = sbv_bv_extract_u32_23_16_u8(s1880);
s1916 = table0[s1915];
s1917 = sbv_bv_join_u8_u8_u16(s1914, s1916);
s1918 = sbv_bv_extract_u32_15_8_u8(s1834);
s1919 = table0[s1918];
s1920 = sbv_bv_extract_u32_7_0_u8(s1849);
s1921 = table0[s1920];
s1922 = sbv_bv_join_u8_u8_u16(s1919, s1921);
s1923 = sbv_bv_join_u16_u16_u32(s1917, s1922);
s1924 = s1864 ^ s1911;
s1925 = s1923 ^ s1924;
s1926 = sbv_bv_extract_u32_31_24_u8(s1880);
s1927 = table0[s1926];
s1928 = sbv_bv_extract_u32_23_16_u8(s1834);
s1929 = table0[s1928];
s1930 = sbv_bv_join_u8_u8_u16(s1927, s1929);
s1931 = sbv_bv_extract_u32_15_8_u8(s1849);
s1932 = table0[s1931];
s1933 = sbv_bv_extract_u32_7_0_u8(s1865);
s1934 = table0[s1933];
s1935 = sbv_bv_join_u8_u8_u16(s1932, s1934);
s1936 = sbv_bv_join_u16_u16_u32(s1930, s1935);
s1937 = s1879 ^ s1924;
s1938 = s1936 ^ s1937;
sbv_output_0[0] = s1899;
sbv_output_0[1] = s1912;
sbv_output_0[2] = s1925;
sbv_output_0[3] = s1938;
}
== END: "aes128Enc.c" ==================