int __VERIFIER_nondet_int();
void __VERIFIER_error();
int g0 = 0;
int g1 = 0;
int g2 = 0;
int g3 = 0;
int g4 = 0;
int g5 = 0;
int g6 = 0;
int g7 = 0;
int g8 = 0;
int g9 = 0;
int g10 = 0;
int g11 = 0;
int l4 = 0;
int l3 = 0;
int l2 = 0;
int l1 = 0;
int l0 = 0;
int address = 0;
int balance = 0;
int calldataload = 0;
int calldatasize = 0;
int caller = 0;
int callvalue = 0;
int extcodesize = 0;
int gas = 0;
int proof = 0;
int proofP = 0;
int queryId = 0;
int random = 0;
int result = 0;
int returndatasize = 0;
int timestamp = 0;
void init_globals();
void jump0(int s1, int s0);
void block0();
void block13();
void jump13(int s2, int s1, int s0);
void jump65(int s2, int s1, int s0);
void block65(int s0);
void block76(int s0);
void jump76(int s2, int s1, int s0);
void jump87(int s2, int s1, int s0);
void block87(int s0);
void block98(int s0);
void jump98(int s2, int s1, int s0);
void block109(int s0);
void jump109(int s2, int s1, int s0);
void block120(int s0);
void jump120(int s2, int s1, int s0);
void block131(int s0);
void jump131(int s2, int s1, int s0);
void jump142(int s2, int s1, int s0);
void block142(int s0);
void jump153(int s2, int s1, int s0);
void block153(int s0);
void jump164(int s2, int s1, int s0);
void block164(int s0);
void jump175(int s2, int s1, int s0);
void block175(int s0);
void block186(int s0);
void jump186(int s2, int s1, int s0);
void jump197(int s2, int s1, int s0);
void block197(int s0);
void block208(int s0);
void jump208(int s2, int s1, int s0);
void jump219(int s2, int s1, int s0);
void block219(int s0);
void block230(int s0);
void jump230(int s2, int s1, int s0);
void jump241(int s2, int s1, int s0);
void block241(int s0);
void jump252(int s2, int s1, int s0);
void block252(int s0);
void block263(int s0);
void jump263(int s2, int s1, int s0);
void block274();
void jump279(int s2, int s1, int s0);
void block279(int s0);
void block287(int s1, int s0);
void block291(int s1, int s0);
void block322(int s1, int s0);
void block388(int s0);
void block396(int s0);
void jump398(int s2, int s1, int s0);
void block398(int s0);
void block406(int s1, int s0);
void block410(int s1, int s0);
void block419(int s2, int s1, int s0);
void jump441(int s2, int s1, int s0);
void block441(int s0);
void block449(int s1, int s0);
void block453(int s1, int s0);
void block462(int s2, int s1, int s0);
void jump484(int s2, int s1, int s0);
void block484(int s0);
void block492(int s1, int s0);
void block496(int s1, int s0);
void block527(int s2, int s1, int s0);
void block549(int s0);
void jump549(int s2, int s1, int s0);
void block557(int s1, int s0);
void block561(int s1, int s0);
void block736(int s0);
void block738(int s0);
void jump738(int s2, int s1, int s0);
void block746(int s1, int s0);
void block750(int s1, int s0);
void block759(int s1, int s0);
void block781(int s0);
void jump781(int s2, int s1, int s0);
void block789(int s1, int s0);
void block793(int s1, int s0);
void block802(int s2, int s1, int s0);
void block824(int s0);
void jump824(int s2, int s1, int s0);
void block832(int s1, int s0);
void block836(int s1, int s0);
void block845(int s2, int s1, int s0);
void block867(int s0);
void jump867(int s2, int s1, int s0);
void block875(int s1, int s0);
void block879(int s1, int s0);
void block888(int s1, int s0);
void jump928(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block928(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block937(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block955(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump975(int s2, int s1, int s0);
void block975(int s0);
void block983(int s1, int s0);
void block987(int s1, int s0);
void block996(int s2, int s1, int s0);
void jump1062(int s2, int s1, int s0);
void block1062(int s0);
void block1070(int s1, int s0);
void block1074(int s1, int s0);
void block1083(int s0);
void block1085(int s0);
void jump1085(int s2, int s1, int s0);
void block1093(int s1, int s0);
void block1097(int s1, int s0);
void block1106(int s2, int s1, int s0);
void jump1132(int s2, int s1, int s0);
void block1132(int s0);
void block1140(int s1, int s0);
void block1144(int s1, int s0);
void block1209(int s0);
void jump1211(int s2, int s1, int s0);
void block1211(int s0);
void block1219(int s1, int s0);
void block1223(int s1, int s0);
void block1232(int s2, int s1, int s0);
void jump1298(int s2, int s1, int s0);
void block1298(int s0);
void block1306(int s1, int s0);
void block1310(int s1, int s0);
void block1341(int s2, int s1, int s0);
void jump1407(int s2, int s1, int s0);
void block1407(int s0);
void block1415(int s1, int s0);
void block1419(int s1, int s0);
void block1428(int s2, int s1, int s0);
void jump1450(int s2, int s1, int s0);
void block1450(int s0);
void block1458(int s1, int s0);
void block1462(int s1, int s0);
void block1471(int s1, int s0);
void jump1511(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1511(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1520(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1538(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1558(int s0);
void jump1558(int s2, int s1, int s0);
void block1566(int s1, int s0);
void block1570(int s1, int s0);
void block1579(int s2, int s1, int s0);
void block1601(int s0);
void block1609(int s0);
void jump1751(int s5, int s4, int s3, int s2, int s1, int s0);
void block1751(int s1, int s0);
void block1765(int s3, int s2, int s1, int s0);
void block1769(int s3, int s2, int s1, int s0);
void jump1769(int s4, int s3, int s2, int s1, int s0);
void block1791(int s3, int s2, int s1, int s0);
void block1795(int s3, int s2, int s1, int s0);
void block1803(int s3, int s2, int s1, int s0);
void jump1803(int s5, int s4, int s3, int s2, int s1, int s0);
void block1815(int s3, int s2, int s1, int s0);
void jump1834(int s5, int s4, int s3, int s2, int s1, int s0);
void block1834(int s3, int s2, int s1, int s0);
void block1844(int s3, int s2, int s1, int s0);
void block2136(int s3, int s2, int s1, int s0);
void block2140(int s1, int s0);
void block2146(int s1, int s0);
void block2152(int s2, int s1, int s0);
void jump2152(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2166(int s4, int s3, int s2, int s1, int s0);
void block2167(int s4, int s3, int s2, int s1, int s0);
void block2187(int s4, int s3, int s2, int s1, int s0);
void jump2195(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2195(int s5, int s4, int s3, int s2, int s1, int s0);
void block2248(int s4, int s3, int s2, int s1, int s0);
void block2252(int s4, int s3, int s2, int s1, int s0);
void jump2274(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2274(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2285(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2311(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump2311(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2368(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2369(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2388(int s5, int s4, int s3, int s2, int s1, int s0);
void jump2388(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2489(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2490(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump2490(int s5, int s4, int s3, int s2, int s1, int s0);
void jump2735(int s5, int s4, int s3, int s2, int s1, int s0);
void block2735(int s4, int s3, int s2, int s1, int s0);
void block2849(int s4, int s3, int s2, int s1, int s0);
void block2856(int s4, int s3, int s2, int s1, int s0);
void block2857(int s4, int s3, int s2, int s1, int s0);
void block2858(int s4, int s3, int s2, int s1, int s0);
void block2863(int s1, int s0);
void block2873(int s1, int s0);
void block2879(int s1, int s0);
void jump2885(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2885(int s1, int s0);
void block2927(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump2943(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2943(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3017(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3027(int s1, int s0);
void jump3064(int s3, int s2, int s1, int s0);
void block3064(int s1, int s0);
void block3150(int s1, int s0);
void block3207(int s1, int s0);
void block3209(int s1, int s0);
void jump3228(int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3228(int s2, int s1, int s0);
void block3437(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3441(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump3441(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3452(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3461(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3468(int s1, int s0);
void jump3506(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3506(int s2, int s1, int s0);
void block3520(int s4, int s3, int s2, int s1, int s0);
void block3521(int s4, int s3, int s2, int s1, int s0);
void block3568(int s1, int s0);
void jump3574(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3574(int s1, int s0);
void block3616(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump3632(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3632(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3652(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block3662(int s1, int s0);
void block3668(int s1, int s0);
void jump3668(int s3, int s2, int s1, int s0);
void block3679(int s1, int s0);
void block3683(int s1, int s0);
void jump3683(int s2, int s1, int s0);
void block3705(int s1, int s0);
void jump3709(int s3, int s2, int s1, int s0);
void block3709(int s1, int s0);
void block3748(int s1, int s0);
void jump3748(int s3, int s2, int s1, int s0);
void block3761(int s1, int s0);
void block3862(int s1, int s0);
void block3870(int s1, int s0);
void block3871(int s1, int s0);
void block3876(int s1, int s0);
void block3992(int s1, int s0);
void block3993(int s1, int s0);
void block3995(int s5, int s4, int s3, int s2, int s1, int s0);
void jump3995(int s17, int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4127(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4131(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4131(int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4142(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4151(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4151(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4169(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4173(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4330(int s2, int s1, int s0);
void block1611_0(int s2, int s1, int s0);
void block1611_1(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1619_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1619_0(int s4, int s3, int s2, int s1, int s0);
void jump1619_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1619_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1633_0(int s4, int s3, int s2, int s1, int s0);
void jump1633_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1633_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1633_1(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1646_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1646_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1647_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1647_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1647_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1647_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1667_0(int s4, int s3, int s2, int s1, int s0);
void jump1667_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1667_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1667_1(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1680_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1680_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1681_0(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1681_1(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1731_0(int s4, int s3, int s2, int s1, int s0);
void block1731_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1744_0(int s4, int s3, int s2, int s1, int s0);
void block1744_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1745_0(int s4, int s3, int s2, int s1, int s0);
void block1745_1(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4195_0(int s5, int s4, int s3, int s2, int s1, int s0);
void block4195_1(int s2, int s1, int s0);
void block4314_0(int s5, int s4, int s3, int s2, int s1, int s0);
void block4314_1(int s2, int s1, int s0);
void block4328_0(int s5, int s4, int s3, int s2, int s1, int s0);
void block4328_1(int s2, int s1, int s0);
void block4350_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4350_1(int s5, int s4, int s3, int s2, int s1, int s0);
void block4380_0(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4380_1(int s4, int s3, int s2, int s1, int s0);
void block4383_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4383_1(int s5, int s4, int s3, int s2, int s1, int s0);
void block4413_0(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4413_1(int s4, int s3, int s2, int s1, int s0);
void block4416_0_0(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4416_0_1(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4416_1_0(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4416_1_1(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4422_0_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4422_0_0(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4422_0_1(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4422_0_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4422_1_0(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4422_1_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4422_1_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4422_1_1(int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4431_0_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4431_0_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4431_1_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4431_1_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4446_0_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4446_0_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4446_1_0(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4446_1_1(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4450_0_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4450_0_1(int s5, int s4, int s3, int s2, int s1, int s0);
void block4450_1_0(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4450_1_1(int s5, int s4, int s3, int s2, int s1, int s0);
int main();
extern void __VERIFIER_error(void);
void block549_0(int s0);
void init_globals_1();
void jump549_2(int s2, int s1, int s0);
void block561_3(int s1, int s0);
void block2187_4(int s4, int s3, int s2, int s1, int s0);
void block3995_5(int s5, int s4, int s3, int s2, int s1, int s0);
void jump3995_6(int s17, int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4131_7(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4131_8(int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4151_9(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump4151_10(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block4173_11(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2195_12(int s5, int s4, int s3, int s2, int s1, int s0);
void jump2195_13(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2252_14(int s4, int s3, int s2, int s1, int s0);
void block2274_15(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump2274_16(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2311_17(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump2311_18(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block2369_19(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1611_1_20(int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1619_1_21(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1619_1_22(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1633_1_23(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1633_1_24(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1647_1_25(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1647_1_26(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1667_1_27(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void jump1667_1_28(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block1680_1_29(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0);
void block549_0(int s0) {
  int s1;
  int s2;
  init_globals_1();
  s1 = callvalue;
  s2 = s1;
  jump549_2(s2, s1, s0);
}

void init_globals_1() {
  g0 = __VERIFIER_nondet_int();
  g1 = __VERIFIER_nondet_int();
  g2 = __VERIFIER_nondet_int();
  g3 = __VERIFIER_nondet_int();
  g4 = __VERIFIER_nondet_int();
  g5 = __VERIFIER_nondet_int();
  g6 = __VERIFIER_nondet_int();
  g7 = __VERIFIER_nondet_int();
  g8 = __VERIFIER_nondet_int();
  g9 = __VERIFIER_nondet_int();
  g10 = __VERIFIER_nondet_int();
  g11 = __VERIFIER_nondet_int();
  l4 = __VERIFIER_nondet_int();
  l3 = __VERIFIER_nondet_int();
  l2 = __VERIFIER_nondet_int();
  l1 = __VERIFIER_nondet_int();
  l0 = __VERIFIER_nondet_int();
  address = __VERIFIER_nondet_int();
  balance = __VERIFIER_nondet_int();
  calldataload = __VERIFIER_nondet_int();
  calldatasize = __VERIFIER_nondet_int();
  caller = __VERIFIER_nondet_int();
  callvalue = __VERIFIER_nondet_int();
  extcodesize = __VERIFIER_nondet_int();
  gas = __VERIFIER_nondet_int();
  proof = __VERIFIER_nondet_int();
  proofP = __VERIFIER_nondet_int();
  queryId = __VERIFIER_nondet_int();
  random = __VERIFIER_nondet_int();
  result = __VERIFIER_nondet_int();
  returndatasize = __VERIFIER_nondet_int();
  timestamp = __VERIFIER_nondet_int();
}

void jump549_2(int s2, int s1, int s0) {
  __CPROVER_assume(s2 == 0);
  block561_3(s1, s0);
}

void block561_3(int s1, int s0) {
  int s2;
  int s3;
  int s4;
  int s5;
  int s6;
  int s7;
  int s8;
  int s9;
  int s10;
  int s11;
  int s12;
  int s13;
  int s14;
  int s15;
  int s16;
  int ls1;
  int ls2;
  s1 = 736;
  s2 = 4;
  s3 = s2;
  s4 = calldatasize;
  s3 = s4 - s3;
  s4 = s2;
  s3 = s4 + s3;
  s4 = s2;
  s2 = s3;
  s3 = s4;
  s4 = s3;
  s5 = s4;
  s5 = queryId;
  s6 = 0;
  s6 = __VERIFIER_nondet_int();
  s5 = __VERIFIER_nondet_int();
  s6 = s4;
  s4 = s5;
  s5 = s6;
  s6 = 32;
  s5 = s6 + s5;
  s6 = s4;
  s4 = s5;
  s5 = s6;
  s6 = s2;
  s2 = s5;
  s5 = s6;
  s6 = s3;
  s3 = s5;
  s5 = s6;
  s6 = s4;
  s4 = s5;
  s5 = s6;
  s6 = s5;
  s6 = result;
  s7 = s5;
  s5 = s6;
  s6 = s7;
  s7 = 32;
  s6 = s7 + s6;
  s7 = s5;
  s5 = s6;
  s6 = s7;
  s7 = s4;
  s6 = s7 + s6;
  s7 = s6;
  s7 = result;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s8 = 32;
  s7 = s8 + s7;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s8 = s7;
  s9 = s8;
  s10 = 31;
  s9 = s10 + s9;
  s10 = 32;
  s11 = s10;
  s12 = s9;
  s9 = s11;
  s11 = s12;
  s10 = s11 / s10;
  s9 = s10 * s9;
  s10 = 32;
  s9 = s10 + s9;
  s10 = 64;
  s10 = l0;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s11 = s9;
  s10 = s11 + s10;
  s11 = 64;
  l0 = s10;
  s10 = s9;
  s11 = s6;
  s6 = s10;
  s10 = s11;
  s11 = s7;
  s7 = s10;
  s10 = s11;
  s11 = s8;
  s8 = s10;
  s10 = s11;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s11 = s9;
  s12 = s10;
  l1 = s11;
  s11 = 32;
  s10 = s11 + s10;
  s11 = s7;
  s12 = s8;
  s13 = s12;
  s14 = s11;
  s15 = s10;
  s13 = s10;
  s12 = s13 + s12;
  s13 = s10;
  s10 = s12;
  s12 = s13;
  s7 = s4;
  s4 = s6;
  s6 = s7;
  s7 = s3;
  s3 = s6;
  s6 = s7;
  s7 = s4;
  s4 = s6;
  s6 = s7;
  s7 = s3;
  s3 = s6;
  s6 = s7;
  s7 = s5;
  s5 = s6;
  s6 = s7;
  s7 = s6;
  s7 = proof;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s8 = 32;
  s7 = s8 + s7;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s8 = s5;
  s7 = s8 + s7;
  s8 = s7;
  s8 = proof;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s9 = 32;
  s8 = s9 + s8;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s9 = s8;
  s10 = s9;
  s11 = 31;
  s10 = s11 + s10;
  s11 = 32;
  s12 = s11;
  s13 = s10;
  s10 = s12;
  s12 = s13;
  s11 = s12 / s11;
  s10 = s11 * s10;
  s11 = 32;
  s10 = s11 + s10;
  s11 = 64;
  s11 = l0;
  s12 = s10;
  s10 = s11;
  s11 = s12;
  s12 = s10;
  s11 = s12 + s11;
  s12 = 64;
  l0 = s11;
  s11 = s10;
  s12 = s7;
  s7 = s11;
  s11 = s12;
  s12 = s8;
  s8 = s11;
  s11 = s12;
  s12 = s9;
  s9 = s11;
  s11 = s12;
  s12 = s10;
  s10 = s11;
  s11 = s12;
  s12 = s10;
  s13 = s11;
  ls1 = s12;
  ls2 = s13;
  s12 = 32;
  s11 = s12 + s11;
  s12 = s8;
  s13 = s9;
  s14 = s13;
  s15 = s12;
  s16 = s11;
  s14 = s11;
  s13 = s14 + s13;
  s14 = s11;
  s11 = s13;
  s13 = s14;
  s8 = s5;
  s5 = s7;
  s7 = s8;
  s8 = s4;
  s4 = s7;
  s7 = s8;
  s8 = s5;
  s5 = s7;
  s7 = s8;
  s8 = s4;
  s4 = s7;
  s7 = s8;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s5 = 2187;
  block2187_4(s4, s3, s2, s1, s0);
}

void block2187_4(int s4, int s3, int s2, int s1, int s0) {
  int s5;
  int s6;
  s5 = 2195;
  s6 = 3995;
  block3995_5(s5, s4, s3, s2, s1, s0);
}

void block3995_5(int s5, int s4, int s3, int s2, int s1, int s0) {
  int s6;
  int s7;
  int s8;
  int s9;
  int s10;
  int s11;
  int s12;
  int s13;
  int s14;
  int s15;
  int s16;
  int s17;
  int ls1;
  int ls2;
  s6 = 0;
  s7 = 11;
  s8 = 1;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s8 = g11;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s9 = 256;
  s8 = __VERIFIER_nondet_int();
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s7 = s8 / s7;
  s8 = 4294967295U;
  s7 = __VERIFIER_nondet_int();
  s8 = 4294967295U;
  s7 = __VERIFIER_nondet_int();
  s8 = 3263287710U;
  s9 = 64;
  s9 = l0;
  s10 = s8;
  s11 = 4294967295U;
  s10 = __VERIFIER_nondet_int();
  s11 = 4294967295U;
  s10 = s11 * s10;
  s11 = s9;
  ls1 = s10;
  ls2 = s11;
  s10 = 4;
  s9 = s10 + s9;
  s10 = 32;
  s11 = 64;
  s11 = l0;
  s12 = s11;
  s13 = s9;
  s12 = s13 - s12;
  s13 = s11;
  s14 = 0;
  s15 = s7;
  s16 = s15;
  s16 = extcodesize;
  s16 = s16 == 0;
  s17 = s16;
  jump3995_6(s17, s16, s15, s14, s13, s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump3995_6(int s17, int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s17 == 0);
  block4131_7(s16, s15, s14, s13, s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block4131_7(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  s16 = gas;
  s10 = 1;
  s10 = s10 == 0;
  s11 = s10;
  jump4131_8(s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump4131_8(int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s11 == 0);
  block4151_9(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block4151_9(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  s7 = 64;
  s7 = l0;
  s8 = returndatasize;
  s9 = 32;
  s10 = s8;
  jump4151_10(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump4151_10(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s10 >= s9);
  block4173_11(s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block4173_11(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s9;
  int s10;
  int s11;
  int ll;
  s9 = s7;
  s8 = s9 + s8;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s9 = s8;
  s10 = s9;
  ll = s10;
  s10 = __VERIFIER_nondet_int();
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s11 = 32;
  s10 = s11 + s10;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s11 = s7;
  s7 = s10;
  s10 = s11;
  s11 = s8;
  s8 = s10;
  s10 = s11;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  s7 = s5;
  s5 = s6;
  s6 = s7;
  block2195_12(s5, s4, s3, s2, s1, s0);
}

void block2195_12(int s5, int s4, int s3, int s2, int s1, int s0) {
  int s6;
  int s7;
  s6 = 4294967295U;
  s5 = __VERIFIER_nondet_int();
  s6 = caller;
  s7 = 4294967295U;
  s6 = __VERIFIER_nondet_int();
  jump2195_13(s6, s5, s4, s3, s2, s1, s0);
}

void jump2195_13(int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s6 == s5);
  block2252_14(s4, s3, s2, s1, s0);
}

void block2252_14(int s4, int s3, int s2, int s1, int s0) {
  int s5;
  int s6;
  int s7;
  int s8;
  int s9;
  int s10;
  int s11;
  int s12;
  int s13;
  int s14;
  s5 = 1;
  s6 = 5;
  s6 = g5;
  s7 = s3;
  s8 = 64;
  s8 = l0;
  s9 = s8;
  s10 = s7;
  s11 = s10;
  s11 = l1;
  s12 = s10;
  s10 = s11;
  s11 = s12;
  s12 = 32;
  s11 = s12 + s11;
  s12 = s10;
  s10 = s11;
  s11 = s12;
  s12 = s11;
  s13 = s9;
  s14 = s10;
  block2274_15(s14, s13, s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block2274_15(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s15;
  int s16;
  s15 = 32;
  s16 = s12;
  jump2274_16(s16, s15, s14, s13, s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump2274_16(int s16, int s15, int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s16 < s15);
  block2311_17(s14, s13, s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block2311_17(int s14, int s13, int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s15;
  int s16;
  int s17;
  int s18;
  int s19;
  int ll;
  int ls1;
  int ls2;
  s15 = 1;
  s16 = s12;
  s17 = 32;
  s16 = s17 - s16;
  s17 = 256;
  s16 = __VERIFIER_nondet_int();
  s15 = s16 - s15;
  s16 = s15;
  s16 = __VERIFIER_nondet_int();
  s17 = s14;
  s17 = l3;
  s16 = __VERIFIER_nondet_int();
  s17 = s15;
  s18 = s13;
  ll = s18;
  s18 = __VERIFIER_nondet_int();
  s17 = __VERIFIER_nondet_int();
  s18 = s17;
  s19 = s16;
  s18 = __VERIFIER_nondet_int();
  s19 = s13;
  ls1 = s18;
  ls2 = s19;
  s12 = s10;
  s10 = s11;
  s11 = s12;
  s9 = s10 + s9;
  s10 = s7;
  s7 = s9;
  s9 = s10;
  s8 = 64;
  s8 = l0;
  s9 = s8;
  s10 = s7;
  s7 = s9;
  s9 = s10;
  s8 = s9 - s8;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s7 = __VERIFIER_nondet_int();
  s8 = 1;
  s9 = s7;
  s7 = s8;
  s8 = s9;
  s7 = s8 / s7;
  s8 = s6;
  jump2311_18(s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump2311_18(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s8 != 0);
  block2369_19(s7, s6, s5, s4, s3, s2, s1, s0);
}

void block2369_19(int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s8;
  s6 = s7 % s6;
  s5 = s6 + s5;
  s6 = 10;
  s7 = s5;
  s8 = s6;
  s6 = s7;
  s7 = s8;
  g10 = s6;
  s5 = 2388;
  s6 = 10;
  s6 = g10;
  s7 = 1611;
  block1611_1_20(s6, s5, s4, s3, s2, s1, s0);
}

void block1611_1_20(int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s7;
  int s8;
  int s9;
  int s10;
  s7 = 0;
  s8 = s7;
  s9 = 0;
  s10 = s8;
  s8 = s9;
  s9 = s10;
  block1619_1_21(s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block1619_1_21(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s9;
  int s10;
  int s11;
  s9 = 3;
  s10 = s9;
  s10 = g3;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s10 = s8;
  jump1619_1_22(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump1619_1_22(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(!(s10 >= s9));
  block1633_1_23(s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block1633_1_23(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s9;
  int s10;
  int s11;
  int s12;
  s9 = 3;
  s10 = s8;
  s11 = s9;
  s11 = g3;
  s12 = s10;
  jump1633_1_24(s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump1633_1_24(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(s12 < s11);
  block1647_1_25(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block1647_1_25(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s11;
  int gl;
  s11 = s9;
  s9 = s10;
  s10 = s11;
  s11 = 0;
  l2 = __VERIFIER_nondet_int();
  s10 = 32;
  s11 = 0;
  s10 = __VERIFIER_nondet_int();
  s9 = s10 + s9;
  gl = s9;
  s9 = __VERIFIER_nondet_int();
  s10 = s6;
  jump1647_1_26(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump1647_1_26(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(!(s10 > s9));
  block1667_1_27(s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block1667_1_27(int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  int s9;
  int s10;
  int s11;
  int s12;
  s9 = 1;
  s10 = s8;
  s11 = s9;
  s11 = g1;
  s12 = s10;
  jump1667_1_28(s12, s11, s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void jump1667_1_28(int s12, int s11, int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __CPROVER_assume(!(s12 < s11));
  block1680_1_29(s10, s9, s8, s7, s6, s5, s4, s3, s2, s1, s0);
}

void block1680_1_29(int s10, int s9, int s8, int s7, int s6, int s5, int s4, int s3, int s2, int s1, int s0) {
  __VERIFIER_error(); // target state
  __VERIFIER_error();
}
