From a5e3adab4c343744085e80cc204522f2f907ef1f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 14 May 2017 20:14:50 -0400 Subject: make display Not quite sure what changed.... --- .../IntegrationTestLadderstep130Display.log | 366 ++++++++++----------- 1 file changed, 183 insertions(+), 183 deletions(-) (limited to 'src') diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log index e823c43e0..9ccfe2be2 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -29,21 +29,21 @@ let (a, b) := Interp-η uint256_t x57 = 0x5 * x56; uint256_t x58 = x53 + x57; uint128_t x59 = (uint128_t) (x58 >> 0x55); - uint256_t x60 = x59 + x52; - uint128_t x61 = (uint128_t) (x60 >> 0x55); - uint256_t x62 = x61 + x46; - uint128_t x63 = (uint128_t) x58 & 0x1fffffffffffffffffffffL; - uint128_t x64 = (uint128_t) (x62 >> 0x55); - uint128_t x65 = 0x5 * x64; - uint128_t x66 = x63 + x65; - uint128_t x67 = x66 >> 0x55; - uint128_t x68 = (uint128_t) x60 & 0x1fffffffffffffffffffffL; - uint128_t x69 = x67 + x68; - uint128_t x70 = x69 >> 0x55; - uint128_t x71 = (uint128_t) x62 & 0x1fffffffffffffffffffffL; - uint128_t x72 = x70 + x71; - uint128_t x73 = x69 & 0x1fffffffffffffffffffffL; - uint128_t x74 = x66 & 0x1fffffffffffffffffffffL; + uint128_t x60 = (uint128_t) x58 & 0x1fffffffffffffffffffffL; + uint256_t x61 = x59 + x52; + uint128_t x62 = (uint128_t) (x61 >> 0x55); + uint128_t x63 = (uint128_t) x61 & 0x1fffffffffffffffffffffL; + uint256_t x64 = x62 + x46; + uint128_t x65 = (uint128_t) (x64 >> 0x55); + uint128_t x66 = (uint128_t) x64 & 0x1fffffffffffffffffffffL; + uint128_t x67 = 0x5 * x65; + uint128_t x68 = x60 + x67; + uint128_t x69 = x68 >> 0x55; + uint128_t x70 = x68 & 0x1fffffffffffffffffffffL; + uint128_t x71 = x69 + x63; + uint128_t x72 = x71 >> 0x55; + uint128_t x73 = x71 & 0x1fffffffffffffffffffffL; + uint128_t x74 = x72 + x66; uint256_t x75 = (uint256_t) x41 * x37; uint256_t x76 = (uint256_t) x39 * x39; uint256_t x77 = (uint256_t) x37 * x41; @@ -62,82 +62,82 @@ let (a, b) := Interp-η uint256_t x90 = 0x5 * x89; uint256_t x91 = x86 + x90; uint128_t x92 = (uint128_t) (x91 >> 0x55); - uint256_t x93 = x92 + x85; - uint128_t x94 = (uint128_t) (x93 >> 0x55); - uint256_t x95 = x94 + x79; - uint128_t x96 = (uint128_t) x91 & 0x1fffffffffffffffffffffL; - uint128_t x97 = (uint128_t) (x95 >> 0x55); - uint128_t x98 = 0x5 * x97; - uint128_t x99 = x96 + x98; - uint128_t x100 = x99 >> 0x55; - uint128_t x101 = (uint128_t) x93 & 0x1fffffffffffffffffffffL; - uint128_t x102 = x100 + x101; - uint128_t x103 = x102 >> 0x55; - uint128_t x104 = (uint128_t) x95 & 0x1fffffffffffffffffffffL; - uint128_t x105 = x103 + x104; - uint128_t x106 = x102 & 0x1fffffffffffffffffffffL; - uint128_t x107 = x99 & 0x1fffffffffffffffffffffL; - uint256_t x108 = (uint256_t) x74 * x105; + uint128_t x93 = (uint128_t) x91 & 0x1fffffffffffffffffffffL; + uint256_t x94 = x92 + x85; + uint128_t x95 = (uint128_t) (x94 >> 0x55); + uint128_t x96 = (uint128_t) x94 & 0x1fffffffffffffffffffffL; + uint256_t x97 = x95 + x79; + uint128_t x98 = (uint128_t) (x97 >> 0x55); + uint128_t x99 = (uint128_t) x97 & 0x1fffffffffffffffffffffL; + uint128_t x100 = 0x5 * x98; + uint128_t x101 = x93 + x100; + uint128_t x102 = x101 >> 0x55; + uint128_t x103 = x101 & 0x1fffffffffffffffffffffL; + uint128_t x104 = x102 + x96; + uint128_t x105 = x104 >> 0x55; + uint128_t x106 = x104 & 0x1fffffffffffffffffffffL; + uint128_t x107 = x105 + x99; + uint256_t x108 = (uint256_t) x70 * x107; uint256_t x109 = (uint256_t) x73 * x106; - uint256_t x110 = (uint256_t) x72 * x107; + uint256_t x110 = (uint256_t) x74 * x103; uint256_t x111 = x109 + x110; uint256_t x112 = x108 + x111; - uint256_t x113 = (uint256_t) x74 * x106; - uint256_t x114 = (uint256_t) x73 * x107; + uint256_t x113 = (uint256_t) x70 * x106; + uint256_t x114 = (uint256_t) x73 * x103; uint256_t x115 = x113 + x114; - uint256_t x116 = (uint256_t) x72 * x105; + uint256_t x116 = (uint256_t) x74 * x107; uint256_t x117 = 0x5 * x116; uint256_t x118 = x115 + x117; - uint256_t x119 = (uint256_t) x74 * x107; - uint256_t x120 = (uint256_t) x73 * x105; - uint256_t x121 = (uint256_t) x72 * x106; + uint256_t x119 = (uint256_t) x70 * x103; + uint256_t x120 = (uint256_t) x73 * x107; + uint256_t x121 = (uint256_t) x74 * x106; uint256_t x122 = x120 + x121; uint256_t x123 = 0x5 * x122; uint256_t x124 = x119 + x123; uint128_t x125 = (uint128_t) (x124 >> 0x55); - uint256_t x126 = x125 + x118; - uint128_t x127 = (uint128_t) (x126 >> 0x55); - uint256_t x128 = x127 + x112; - uint128_t x129 = (uint128_t) x124 & 0x1fffffffffffffffffffffL; - uint128_t x130 = (uint128_t) (x128 >> 0x55); - uint128_t x131 = 0x5 * x130; - uint128_t x132 = x129 + x131; - uint128_t x133 = x132 >> 0x55; - uint128_t x134 = (uint128_t) x126 & 0x1fffffffffffffffffffffL; - uint128_t x135 = x133 + x134; - uint128_t x136 = x135 >> 0x55; - uint128_t x137 = (uint128_t) x128 & 0x1fffffffffffffffffffffL; - uint128_t x138 = x136 + x137; - uint128_t x139 = x135 & 0x1fffffffffffffffffffffL; - uint128_t x140 = x132 & 0x1fffffffffffffffffffffL; - uint128_t x141 = 0x3ffffffffffffffffffffeL + x72; - uint128_t x142 = x141 - x105; + uint128_t x126 = (uint128_t) x124 & 0x1fffffffffffffffffffffL; + uint256_t x127 = x125 + x118; + uint128_t x128 = (uint128_t) (x127 >> 0x55); + uint128_t x129 = (uint128_t) x127 & 0x1fffffffffffffffffffffL; + uint256_t x130 = x128 + x112; + uint128_t x131 = (uint128_t) (x130 >> 0x55); + uint128_t x132 = (uint128_t) x130 & 0x1fffffffffffffffffffffL; + uint128_t x133 = 0x5 * x131; + uint128_t x134 = x126 + x133; + uint128_t x135 = x134 >> 0x55; + uint128_t x136 = x134 & 0x1fffffffffffffffffffffL; + uint128_t x137 = x135 + x129; + uint128_t x138 = x137 >> 0x55; + uint128_t x139 = x137 & 0x1fffffffffffffffffffffL; + uint128_t x140 = x138 + x132; + uint128_t x141 = 0x3ffffffffffffffffffffeL + x74; + uint128_t x142 = x141 - x107; uint128_t x143 = 0x3ffffffffffffffffffffeL + x73; uint128_t x144 = x143 - x106; - uint128_t x145 = 0x3ffffffffffffffffffff6L + x74; - uint128_t x146 = x145 - x107; + uint128_t x145 = 0x3ffffffffffffffffffff6L + x70; + uint128_t x146 = x145 - x103; uint128_t x147 = 0x1db41 * x142; uint128_t x148 = 0x1db41 * x144; uint128_t x149 = 0x1db41 * x146; uint128_t x150 = x149 >> 0x55; - uint128_t x151 = x150 + x148; - uint128_t x152 = x151 >> 0x55; - uint128_t x153 = x152 + x147; - uint128_t x154 = x149 & 0x1fffffffffffffffffffffL; - uint128_t x155 = x153 >> 0x55; - uint128_t x156 = 0x5 * x155; - uint128_t x157 = x154 + x156; - uint128_t x158 = x157 >> 0x55; - uint128_t x159 = x151 & 0x1fffffffffffffffffffffL; - uint128_t x160 = x158 + x159; - uint128_t x161 = x160 >> 0x55; - uint128_t x162 = x153 & 0x1fffffffffffffffffffffL; - uint128_t x163 = x161 + x162; - uint128_t x164 = x160 & 0x1fffffffffffffffffffffL; - uint128_t x165 = x157 & 0x1fffffffffffffffffffffL; - uint128_t x166 = x72 + x163; + uint128_t x151 = x149 & 0x1fffffffffffffffffffffL; + uint128_t x152 = x150 + x148; + uint128_t x153 = x152 >> 0x55; + uint128_t x154 = x152 & 0x1fffffffffffffffffffffL; + uint128_t x155 = x153 + x147; + uint128_t x156 = x155 >> 0x55; + uint128_t x157 = x155 & 0x1fffffffffffffffffffffL; + uint128_t x158 = 0x5 * x156; + uint128_t x159 = x151 + x158; + uint128_t x160 = x159 >> 0x55; + uint128_t x161 = x159 & 0x1fffffffffffffffffffffL; + uint128_t x162 = x160 + x154; + uint128_t x163 = x162 >> 0x55; + uint128_t x164 = x162 & 0x1fffffffffffffffffffffL; + uint128_t x165 = x163 + x157; + uint128_t x166 = x74 + x165; uint128_t x167 = x73 + x164; - uint128_t x168 = x74 + x165; + uint128_t x168 = x70 + x161; uint256_t x169 = (uint256_t) x146 * x166; uint256_t x170 = (uint256_t) x144 * x167; uint256_t x171 = (uint256_t) x142 * x168; @@ -156,21 +156,21 @@ let (a, b) := Interp-η uint256_t x184 = 0x5 * x183; uint256_t x185 = x180 + x184; uint128_t x186 = (uint128_t) (x185 >> 0x55); - uint256_t x187 = x186 + x179; - uint128_t x188 = (uint128_t) (x187 >> 0x55); - uint256_t x189 = x188 + x173; - uint128_t x190 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; - uint128_t x191 = (uint128_t) (x189 >> 0x55); - uint128_t x192 = 0x5 * x191; - uint128_t x193 = x190 + x192; - uint128_t x194 = x193 >> 0x55; - uint128_t x195 = (uint128_t) x187 & 0x1fffffffffffffffffffffL; - uint128_t x196 = x194 + x195; - uint128_t x197 = x196 >> 0x55; - uint128_t x198 = (uint128_t) x189 & 0x1fffffffffffffffffffffL; - uint128_t x199 = x197 + x198; - uint128_t x200 = x196 & 0x1fffffffffffffffffffffL; - uint128_t x201 = x193 & 0x1fffffffffffffffffffffL; + uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; + uint256_t x188 = x186 + x179; + uint128_t x189 = (uint128_t) (x188 >> 0x55); + uint128_t x190 = (uint128_t) x188 & 0x1fffffffffffffffffffffL; + uint256_t x191 = x189 + x173; + uint128_t x192 = (uint128_t) (x191 >> 0x55); + uint128_t x193 = (uint128_t) x191 & 0x1fffffffffffffffffffffL; + uint128_t x194 = 0x5 * x192; + uint128_t x195 = x187 + x194; + uint128_t x196 = x195 >> 0x55; + uint128_t x197 = x195 & 0x1fffffffffffffffffffffL; + uint128_t x198 = x196 + x190; + uint128_t x199 = x198 >> 0x55; + uint128_t x200 = x198 & 0x1fffffffffffffffffffffL; + uint128_t x201 = x199 + x193; uint128_t x202 = x27 + x31; uint128_t x203 = x28 + x32; uint128_t x204 = x26 + x30; @@ -198,21 +198,21 @@ let (a, b) := Interp-η uint256_t x226 = 0x5 * x225; uint256_t x227 = x222 + x226; uint128_t x228 = (uint128_t) (x227 >> 0x55); - uint256_t x229 = x228 + x221; - uint128_t x230 = (uint128_t) (x229 >> 0x55); - uint256_t x231 = x230 + x215; - uint128_t x232 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; - uint128_t x233 = (uint128_t) (x231 >> 0x55); - uint128_t x234 = 0x5 * x233; - uint128_t x235 = x232 + x234; - uint128_t x236 = x235 >> 0x55; - uint128_t x237 = (uint128_t) x229 & 0x1fffffffffffffffffffffL; - uint128_t x238 = x236 + x237; - uint128_t x239 = x238 >> 0x55; - uint128_t x240 = (uint128_t) x231 & 0x1fffffffffffffffffffffL; - uint128_t x241 = x239 + x240; - uint128_t x242 = x238 & 0x1fffffffffffffffffffffL; - uint128_t x243 = x235 & 0x1fffffffffffffffffffffL; + uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; + uint256_t x230 = x228 + x221; + uint128_t x231 = (uint128_t) (x230 >> 0x55); + uint128_t x232 = (uint128_t) x230 & 0x1fffffffffffffffffffffL; + uint256_t x233 = x231 + x215; + uint128_t x234 = (uint128_t) (x233 >> 0x55); + uint128_t x235 = (uint128_t) x233 & 0x1fffffffffffffffffffffL; + uint128_t x236 = 0x5 * x234; + uint128_t x237 = x229 + x236; + uint128_t x238 = x237 >> 0x55; + uint128_t x239 = x237 & 0x1fffffffffffffffffffffL; + uint128_t x240 = x238 + x232; + uint128_t x241 = x240 >> 0x55; + uint128_t x242 = x240 & 0x1fffffffffffffffffffffL; + uint128_t x243 = x241 + x235; uint256_t x244 = (uint256_t) x210 * x33; uint256_t x245 = (uint256_t) x208 * x34; uint256_t x246 = (uint256_t) x206 * x35; @@ -231,27 +231,27 @@ let (a, b) := Interp-η uint256_t x259 = 0x5 * x258; uint256_t x260 = x255 + x259; uint128_t x261 = (uint128_t) (x260 >> 0x55); - uint256_t x262 = x261 + x254; - uint128_t x263 = (uint128_t) (x262 >> 0x55); - uint256_t x264 = x263 + x248; - uint128_t x265 = (uint128_t) x260 & 0x1fffffffffffffffffffffL; - uint128_t x266 = (uint128_t) (x264 >> 0x55); - uint128_t x267 = 0x5 * x266; - uint128_t x268 = x265 + x267; - uint128_t x269 = x268 >> 0x55; - uint128_t x270 = (uint128_t) x262 & 0x1fffffffffffffffffffffL; - uint128_t x271 = x269 + x270; - uint128_t x272 = x271 >> 0x55; - uint128_t x273 = (uint128_t) x264 & 0x1fffffffffffffffffffffL; - uint128_t x274 = x272 + x273; - uint128_t x275 = x271 & 0x1fffffffffffffffffffffL; - uint128_t x276 = x268 & 0x1fffffffffffffffffffffL; - uint128_t x277 = x274 + x241; + uint128_t x262 = (uint128_t) x260 & 0x1fffffffffffffffffffffL; + uint256_t x263 = x261 + x254; + uint128_t x264 = (uint128_t) (x263 >> 0x55); + uint128_t x265 = (uint128_t) x263 & 0x1fffffffffffffffffffffL; + uint256_t x266 = x264 + x248; + uint128_t x267 = (uint128_t) (x266 >> 0x55); + uint128_t x268 = (uint128_t) x266 & 0x1fffffffffffffffffffffL; + uint128_t x269 = 0x5 * x267; + uint128_t x270 = x262 + x269; + uint128_t x271 = x270 >> 0x55; + uint128_t x272 = x270 & 0x1fffffffffffffffffffffL; + uint128_t x273 = x271 + x265; + uint128_t x274 = x273 >> 0x55; + uint128_t x275 = x273 & 0x1fffffffffffffffffffffL; + uint128_t x276 = x274 + x268; + uint128_t x277 = x276 + x243; uint128_t x278 = x275 + x242; - uint128_t x279 = x276 + x243; - uint128_t x280 = x274 + x241; + uint128_t x279 = x272 + x239; + uint128_t x280 = x276 + x243; uint128_t x281 = x275 + x242; - uint128_t x282 = x276 + x243; + uint128_t x282 = x272 + x239; uint256_t x283 = (uint256_t) x279 * x280; uint256_t x284 = (uint256_t) x278 * x281; uint256_t x285 = (uint256_t) x277 * x282; @@ -270,33 +270,33 @@ let (a, b) := Interp-η uint256_t x298 = 0x5 * x297; uint256_t x299 = x294 + x298; uint128_t x300 = (uint128_t) (x299 >> 0x55); - uint256_t x301 = x300 + x293; - uint128_t x302 = (uint128_t) (x301 >> 0x55); - uint256_t x303 = x302 + x287; - uint128_t x304 = (uint128_t) x299 & 0x1fffffffffffffffffffffL; - uint128_t x305 = (uint128_t) (x303 >> 0x55); - uint128_t x306 = 0x5 * x305; - uint128_t x307 = x304 + x306; - uint128_t x308 = x307 >> 0x55; - uint128_t x309 = (uint128_t) x301 & 0x1fffffffffffffffffffffL; - uint128_t x310 = x308 + x309; - uint128_t x311 = x310 >> 0x55; - uint128_t x312 = (uint128_t) x303 & 0x1fffffffffffffffffffffL; - uint128_t x313 = x311 + x312; - uint128_t x314 = x310 & 0x1fffffffffffffffffffffL; - uint128_t x315 = x307 & 0x1fffffffffffffffffffffL; - uint128_t x316 = 0x3ffffffffffffffffffffeL + x274; - uint128_t x317 = x316 - x241; + uint128_t x301 = (uint128_t) x299 & 0x1fffffffffffffffffffffL; + uint256_t x302 = x300 + x293; + uint128_t x303 = (uint128_t) (x302 >> 0x55); + uint128_t x304 = (uint128_t) x302 & 0x1fffffffffffffffffffffL; + uint256_t x305 = x303 + x287; + uint128_t x306 = (uint128_t) (x305 >> 0x55); + uint128_t x307 = (uint128_t) x305 & 0x1fffffffffffffffffffffL; + uint128_t x308 = 0x5 * x306; + uint128_t x309 = x301 + x308; + uint128_t x310 = x309 >> 0x55; + uint128_t x311 = x309 & 0x1fffffffffffffffffffffL; + uint128_t x312 = x310 + x304; + uint128_t x313 = x312 >> 0x55; + uint128_t x314 = x312 & 0x1fffffffffffffffffffffL; + uint128_t x315 = x313 + x307; + uint128_t x316 = 0x3ffffffffffffffffffffeL + x276; + uint128_t x317 = x316 - x243; uint128_t x318 = 0x3ffffffffffffffffffffeL + x275; uint128_t x319 = x318 - x242; - uint128_t x320 = 0x3ffffffffffffffffffff6L + x276; - uint128_t x321 = x320 - x243; - uint128_t x322 = 0x3ffffffffffffffffffffeL + x274; - uint128_t x323 = x322 - x241; + uint128_t x320 = 0x3ffffffffffffffffffff6L + x272; + uint128_t x321 = x320 - x239; + uint128_t x322 = 0x3ffffffffffffffffffffeL + x276; + uint128_t x323 = x322 - x243; uint128_t x324 = 0x3ffffffffffffffffffffeL + x275; uint128_t x325 = x324 - x242; - uint128_t x326 = 0x3ffffffffffffffffffff6L + x276; - uint128_t x327 = x326 - x243; + uint128_t x326 = 0x3ffffffffffffffffffff6L + x272; + uint128_t x327 = x326 - x239; uint256_t x328 = (uint256_t) x321 * x323; uint256_t x329 = (uint256_t) x319 * x325; uint256_t x330 = (uint256_t) x317 * x327; @@ -315,55 +315,55 @@ let (a, b) := Interp-η uint256_t x343 = 0x5 * x342; uint256_t x344 = x339 + x343; uint128_t x345 = (uint128_t) (x344 >> 0x55); - uint256_t x346 = x345 + x338; - uint128_t x347 = (uint128_t) (x346 >> 0x55); - uint256_t x348 = x347 + x332; - uint128_t x349 = (uint128_t) x344 & 0x1fffffffffffffffffffffL; - uint128_t x350 = (uint128_t) (x348 >> 0x55); - uint128_t x351 = 0x5 * x350; - uint128_t x352 = x349 + x351; - uint128_t x353 = x352 >> 0x55; - uint128_t x354 = (uint128_t) x346 & 0x1fffffffffffffffffffffL; - uint128_t x355 = x353 + x354; - uint128_t x356 = x355 >> 0x55; - uint128_t x357 = (uint128_t) x348 & 0x1fffffffffffffffffffffL; - uint128_t x358 = x356 + x357; - uint128_t x359 = x355 & 0x1fffffffffffffffffffffL; - uint128_t x360 = x352 & 0x1fffffffffffffffffffffL; - uint256_t x361 = (uint256_t) x10 * x358; + uint128_t x346 = (uint128_t) x344 & 0x1fffffffffffffffffffffL; + uint256_t x347 = x345 + x338; + uint128_t x348 = (uint128_t) (x347 >> 0x55); + uint128_t x349 = (uint128_t) x347 & 0x1fffffffffffffffffffffL; + uint256_t x350 = x348 + x332; + uint128_t x351 = (uint128_t) (x350 >> 0x55); + uint128_t x352 = (uint128_t) x350 & 0x1fffffffffffffffffffffL; + uint128_t x353 = 0x5 * x351; + uint128_t x354 = x346 + x353; + uint128_t x355 = x354 >> 0x55; + uint128_t x356 = x354 & 0x1fffffffffffffffffffffL; + uint128_t x357 = x355 + x349; + uint128_t x358 = x357 >> 0x55; + uint128_t x359 = x357 & 0x1fffffffffffffffffffffL; + uint128_t x360 = x358 + x352; + uint256_t x361 = (uint256_t) x10 * x360; uint256_t x362 = (uint256_t) x12 * x359; - uint256_t x363 = (uint256_t) x11 * x360; + uint256_t x363 = (uint256_t) x11 * x356; uint256_t x364 = x362 + x363; uint256_t x365 = x361 + x364; uint256_t x366 = (uint256_t) x10 * x359; - uint256_t x367 = (uint256_t) x12 * x360; + uint256_t x367 = (uint256_t) x12 * x356; uint256_t x368 = x366 + x367; - uint256_t x369 = (uint256_t) x11 * x358; + uint256_t x369 = (uint256_t) x11 * x360; uint256_t x370 = 0x5 * x369; uint256_t x371 = x368 + x370; - uint256_t x372 = (uint256_t) x10 * x360; - uint256_t x373 = (uint256_t) x12 * x358; + uint256_t x372 = (uint256_t) x10 * x356; + uint256_t x373 = (uint256_t) x12 * x360; uint256_t x374 = (uint256_t) x11 * x359; uint256_t x375 = x373 + x374; uint256_t x376 = 0x5 * x375; uint256_t x377 = x372 + x376; uint128_t x378 = (uint128_t) (x377 >> 0x55); - uint256_t x379 = x378 + x371; - uint128_t x380 = (uint128_t) (x379 >> 0x55); - uint256_t x381 = x380 + x365; - uint128_t x382 = (uint128_t) x377 & 0x1fffffffffffffffffffffL; - uint128_t x383 = (uint128_t) (x381 >> 0x55); - uint128_t x384 = 0x5 * x383; - uint128_t x385 = x382 + x384; - uint128_t x386 = x385 >> 0x55; - uint128_t x387 = (uint128_t) x379 & 0x1fffffffffffffffffffffL; - uint128_t x388 = x386 + x387; - uint128_t x389 = x388 >> 0x55; - uint128_t x390 = (uint128_t) x381 & 0x1fffffffffffffffffffffL; - uint128_t x391 = x389 + x390; - uint128_t x392 = x388 & 0x1fffffffffffffffffffffL; - uint128_t x393 = x385 & 0x1fffffffffffffffffffffL; - (Return x138, Return x139, Return x140, (Return x199, Return x200, Return x201), (Return x313, Return x314, Return x315, (Return x391, Return x392, Return x393)))) + uint128_t x379 = (uint128_t) x377 & 0x1fffffffffffffffffffffL; + uint256_t x380 = x378 + x371; + uint128_t x381 = (uint128_t) (x380 >> 0x55); + uint128_t x382 = (uint128_t) x380 & 0x1fffffffffffffffffffffL; + uint256_t x383 = x381 + x365; + uint128_t x384 = (uint128_t) (x383 >> 0x55); + uint128_t x385 = (uint128_t) x383 & 0x1fffffffffffffffffffffL; + uint128_t x386 = 0x5 * x384; + uint128_t x387 = x379 + x386; + uint128_t x388 = x387 >> 0x55; + uint128_t x389 = x387 & 0x1fffffffffffffffffffffL; + uint128_t x390 = x388 + x382; + uint128_t x391 = x390 >> 0x55; + uint128_t x392 = x390 & 0x1fffffffffffffffffffffL; + uint128_t x393 = x391 + x385; + (Return x140, Return x139, Return x136, (Return x201, Return x200, Return x197), (Return x315, Return x314, Return x311, (Return x393, Return x392, Return x389)))) (x, (x0, x1), (x2, x3))%core in (let (a0, b0) := a in (a0, b0), let (a0, b0) := b in -- cgit v1.2.3