diff options
Diffstat (limited to 'src/Specific/IntegrationTestLadderstep130Display.log')
| -rw-r--r-- | src/Specific/IntegrationTestLadderstep130Display.log | 366 |
1 files changed, 183 insertions, 183 deletions
diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log index 95f2237c0..deff79fe1 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -2,216 +2,216 @@ let (a, b) := Interp-η (λ var : Syntax.base_type → Type, λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core, - uint128_t x33 = x17 + x21; - uint128_t x34 = x18 + x22; - uint128_t x35 = x16 + x20; - uint128_t x36 = 0x3ffffffffffffffffffffeL + x17 - x21; - uint128_t x37 = 0x3ffffffffffffffffffffeL + x18 - x22; - uint128_t x38 = 0x3ffffffffffffffffffff6L + x16 - x20; - uint256_t x39 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35); - uint256_t x40 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33); - uint256_t x41 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34); + uint128_t x33 = (x17 + x21); + uint128_t x34 = (x18 + x22); + uint128_t x35 = (x16 + x20); + uint128_t x36 = ((0x3ffffffffffffffffffffeL + x17) - x21); + uint128_t x37 = ((0x3ffffffffffffffffffffeL + x18) - x22); + uint128_t x38 = ((0x3ffffffffffffffffffff6L + x16) - x20); + uint256_t x39 = (((uint256_t)x35 * x33) + (((uint256_t)x34 * x34) + ((uint256_t)x33 * x35))); + uint256_t x40 = ((((uint256_t)x35 * x34) + ((uint256_t)x34 * x35)) + (0x5 * ((uint256_t)x33 * x33))); + uint256_t x41 = (((uint256_t)x35 * x35) + (0x5 * (((uint256_t)x34 * x33) + ((uint256_t)x33 * x34)))); uint128_t x42 = (uint128_t) (x41 >> 0x55); - uint128_t x43 = (uint128_t) x41 & 0x1fffffffffffffffffffffL; - uint256_t x44 = x42 + x40; + uint128_t x43 = ((uint128_t)x41 & 0x1fffffffffffffffffffffL); + uint256_t x44 = (x42 + x40); uint128_t x45 = (uint128_t) (x44 >> 0x55); - uint128_t x46 = (uint128_t) x44 & 0x1fffffffffffffffffffffL; - uint256_t x47 = x45 + x39; + uint128_t x46 = ((uint128_t)x44 & 0x1fffffffffffffffffffffL); + uint256_t x47 = (x45 + x39); uint128_t x48 = (uint128_t) (x47 >> 0x55); - uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL; - uint128_t x50 = x43 + 0x5 * x48; - uint128_t x51 = x50 >> 0x55; - uint128_t x52 = x50 & 0x1fffffffffffffffffffffL; - uint128_t x53 = x51 + x46; - uint128_t x54 = x53 >> 0x55; - uint128_t x55 = x53 & 0x1fffffffffffffffffffffL; - uint128_t x56 = x54 + x49; - uint256_t x57 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38); - uint256_t x58 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36); - uint256_t x59 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37); + uint128_t x49 = ((uint128_t)x47 & 0x1fffffffffffffffffffffL); + uint128_t x50 = (x43 + (0x5 * x48)); + uint128_t x51 = (x50 >> 0x55); + uint128_t x52 = (x50 & 0x1fffffffffffffffffffffL); + uint128_t x53 = (x51 + x46); + uint128_t x54 = (x53 >> 0x55); + uint128_t x55 = (x53 & 0x1fffffffffffffffffffffL); + uint128_t x56 = (x54 + x49); + uint256_t x57 = (((uint256_t)x38 * x36) + (((uint256_t)x37 * x37) + ((uint256_t)x36 * x38))); + uint256_t x58 = ((((uint256_t)x38 * x37) + ((uint256_t)x37 * x38)) + (0x5 * ((uint256_t)x36 * x36))); + uint256_t x59 = (((uint256_t)x38 * x38) + (0x5 * (((uint256_t)x37 * x36) + ((uint256_t)x36 * x37)))); uint128_t x60 = (uint128_t) (x59 >> 0x55); - uint128_t x61 = (uint128_t) x59 & 0x1fffffffffffffffffffffL; - uint256_t x62 = x60 + x58; + uint128_t x61 = ((uint128_t)x59 & 0x1fffffffffffffffffffffL); + uint256_t x62 = (x60 + x58); uint128_t x63 = (uint128_t) (x62 >> 0x55); - uint128_t x64 = (uint128_t) x62 & 0x1fffffffffffffffffffffL; - uint256_t x65 = x63 + x57; + uint128_t x64 = ((uint128_t)x62 & 0x1fffffffffffffffffffffL); + uint256_t x65 = (x63 + x57); uint128_t x66 = (uint128_t) (x65 >> 0x55); - uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; - uint128_t x68 = x61 + 0x5 * x66; - uint128_t x69 = x68 >> 0x55; - uint128_t x70 = x68 & 0x1fffffffffffffffffffffL; - uint128_t x71 = x69 + x64; - uint128_t x72 = x71 >> 0x55; - uint128_t x73 = x71 & 0x1fffffffffffffffffffffL; - uint128_t x74 = x72 + x67; - uint256_t x75 = (uint256_t) x52 * x74 + ((uint256_t) x55 * x73 + (uint256_t) x56 * x70); - uint256_t x76 = (uint256_t) x52 * x73 + (uint256_t) x55 * x70 + 0x5 * ((uint256_t) x56 * x74); - uint256_t x77 = (uint256_t) x52 * x70 + 0x5 * ((uint256_t) x55 * x74 + (uint256_t) x56 * x73); + uint128_t x67 = ((uint128_t)x65 & 0x1fffffffffffffffffffffL); + uint128_t x68 = (x61 + (0x5 * x66)); + uint128_t x69 = (x68 >> 0x55); + uint128_t x70 = (x68 & 0x1fffffffffffffffffffffL); + uint128_t x71 = (x69 + x64); + uint128_t x72 = (x71 >> 0x55); + uint128_t x73 = (x71 & 0x1fffffffffffffffffffffL); + uint128_t x74 = (x72 + x67); + uint256_t x75 = (((uint256_t)x52 * x74) + (((uint256_t)x55 * x73) + ((uint256_t)x56 * x70))); + uint256_t x76 = ((((uint256_t)x52 * x73) + ((uint256_t)x55 * x70)) + (0x5 * ((uint256_t)x56 * x74))); + uint256_t x77 = (((uint256_t)x52 * x70) + (0x5 * (((uint256_t)x55 * x74) + ((uint256_t)x56 * x73)))); uint128_t x78 = (uint128_t) (x77 >> 0x55); - uint128_t x79 = (uint128_t) x77 & 0x1fffffffffffffffffffffL; - uint256_t x80 = x78 + x76; + uint128_t x79 = ((uint128_t)x77 & 0x1fffffffffffffffffffffL); + uint256_t x80 = (x78 + x76); uint128_t x81 = (uint128_t) (x80 >> 0x55); - uint128_t x82 = (uint128_t) x80 & 0x1fffffffffffffffffffffL; - uint256_t x83 = x81 + x75; + uint128_t x82 = ((uint128_t)x80 & 0x1fffffffffffffffffffffL); + uint256_t x83 = (x81 + x75); uint128_t x84 = (uint128_t) (x83 >> 0x55); - uint128_t x85 = (uint128_t) x83 & 0x1fffffffffffffffffffffL; - uint128_t x86 = x79 + 0x5 * x84; - uint128_t x87 = x86 >> 0x55; - uint128_t x88 = x86 & 0x1fffffffffffffffffffffL; - uint128_t x89 = x87 + x82; - uint128_t x90 = x89 >> 0x55; - uint128_t x91 = x89 & 0x1fffffffffffffffffffffL; - uint128_t x92 = x90 + x85; - uint128_t x93 = 0x3ffffffffffffffffffffeL + x56 - x74; - uint128_t x94 = 0x3ffffffffffffffffffffeL + x55 - x73; - uint128_t x95 = 0x3ffffffffffffffffffff6L + x52 - x70; - uint128_t x96 = 0x1db41 * x93; - uint128_t x97 = 0x1db41 * x94; - uint128_t x98 = 0x1db41 * x95; - uint128_t x99 = x98 >> 0x55; - uint128_t x100 = x98 & 0x1fffffffffffffffffffffL; - uint128_t x101 = x99 + x97; - 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 = x100 + 0x5 * x105; - uint128_t x108 = x107 >> 0x55; - uint128_t x109 = x107 & 0x1fffffffffffffffffffffL; - uint128_t x110 = x108 + x103; - uint128_t x111 = x110 >> 0x55; - uint128_t x112 = x110 & 0x1fffffffffffffffffffffL; - uint128_t x113 = x111 + x106; - uint128_t x114 = x56 + x113; - uint128_t x115 = x55 + x112; - uint128_t x116 = x52 + x109; - uint256_t x117 = (uint256_t) x95 * x114 + ((uint256_t) x94 * x115 + (uint256_t) x93 * x116); - uint256_t x118 = (uint256_t) x95 * x115 + (uint256_t) x94 * x116 + 0x5 * ((uint256_t) x93 * x114); - uint256_t x119 = (uint256_t) x95 * x116 + 0x5 * ((uint256_t) x94 * x114 + (uint256_t) x93 * x115); + uint128_t x85 = ((uint128_t)x83 & 0x1fffffffffffffffffffffL); + uint128_t x86 = (x79 + (0x5 * x84)); + uint128_t x87 = (x86 >> 0x55); + uint128_t x88 = (x86 & 0x1fffffffffffffffffffffL); + uint128_t x89 = (x87 + x82); + uint128_t x90 = (x89 >> 0x55); + uint128_t x91 = (x89 & 0x1fffffffffffffffffffffL); + uint128_t x92 = (x90 + x85); + uint128_t x93 = ((0x3ffffffffffffffffffffeL + x56) - x74); + uint128_t x94 = ((0x3ffffffffffffffffffffeL + x55) - x73); + uint128_t x95 = ((0x3ffffffffffffffffffff6L + x52) - x70); + uint128_t x96 = (0x1db41 * x93); + uint128_t x97 = (0x1db41 * x94); + uint128_t x98 = (0x1db41 * x95); + uint128_t x99 = (x98 >> 0x55); + uint128_t x100 = (x98 & 0x1fffffffffffffffffffffL); + uint128_t x101 = (x99 + x97); + 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 = (x100 + (0x5 * x105)); + uint128_t x108 = (x107 >> 0x55); + uint128_t x109 = (x107 & 0x1fffffffffffffffffffffL); + uint128_t x110 = (x108 + x103); + uint128_t x111 = (x110 >> 0x55); + uint128_t x112 = (x110 & 0x1fffffffffffffffffffffL); + uint128_t x113 = (x111 + x106); + uint128_t x114 = (x56 + x113); + uint128_t x115 = (x55 + x112); + uint128_t x116 = (x52 + x109); + uint256_t x117 = (((uint256_t)x95 * x114) + (((uint256_t)x94 * x115) + ((uint256_t)x93 * x116))); + uint256_t x118 = ((((uint256_t)x95 * x115) + ((uint256_t)x94 * x116)) + (0x5 * ((uint256_t)x93 * x114))); + uint256_t x119 = (((uint256_t)x95 * x116) + (0x5 * (((uint256_t)x94 * x114) + ((uint256_t)x93 * x115)))); uint128_t x120 = (uint128_t) (x119 >> 0x55); - uint128_t x121 = (uint128_t) x119 & 0x1fffffffffffffffffffffL; - uint256_t x122 = x120 + x118; + uint128_t x121 = ((uint128_t)x119 & 0x1fffffffffffffffffffffL); + uint256_t x122 = (x120 + x118); uint128_t x123 = (uint128_t) (x122 >> 0x55); - uint128_t x124 = (uint128_t) x122 & 0x1fffffffffffffffffffffL; - uint256_t x125 = x123 + x117; + uint128_t x124 = ((uint128_t)x122 & 0x1fffffffffffffffffffffL); + uint256_t x125 = (x123 + x117); uint128_t x126 = (uint128_t) (x125 >> 0x55); - uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL; - uint128_t x128 = x121 + 0x5 * x126; - uint128_t x129 = x128 >> 0x55; - uint128_t x130 = x128 & 0x1fffffffffffffffffffffL; - uint128_t x131 = x129 + x124; - uint128_t x132 = x131 >> 0x55; - uint128_t x133 = x131 & 0x1fffffffffffffffffffffL; - uint128_t x134 = x132 + x127; - uint128_t x135 = x27 + x31; - uint128_t x136 = x28 + x32; - uint128_t x137 = x26 + x30; - uint128_t x138 = 0x3ffffffffffffffffffffeL + x27 - x31; - uint128_t x139 = 0x3ffffffffffffffffffffeL + x28 - x32; - uint128_t x140 = 0x3ffffffffffffffffffff6L + x26 - x30; - uint256_t x141 = (uint256_t) x137 * x36 + ((uint256_t) x136 * x37 + (uint256_t) x135 * x38); - uint256_t x142 = (uint256_t) x137 * x37 + (uint256_t) x136 * x38 + 0x5 * ((uint256_t) x135 * x36); - uint256_t x143 = (uint256_t) x137 * x38 + 0x5 * ((uint256_t) x136 * x36 + (uint256_t) x135 * x37); + uint128_t x127 = ((uint128_t)x125 & 0x1fffffffffffffffffffffL); + uint128_t x128 = (x121 + (0x5 * x126)); + uint128_t x129 = (x128 >> 0x55); + uint128_t x130 = (x128 & 0x1fffffffffffffffffffffL); + uint128_t x131 = (x129 + x124); + uint128_t x132 = (x131 >> 0x55); + uint128_t x133 = (x131 & 0x1fffffffffffffffffffffL); + uint128_t x134 = (x132 + x127); + uint128_t x135 = (x27 + x31); + uint128_t x136 = (x28 + x32); + uint128_t x137 = (x26 + x30); + uint128_t x138 = ((0x3ffffffffffffffffffffeL + x27) - x31); + uint128_t x139 = ((0x3ffffffffffffffffffffeL + x28) - x32); + uint128_t x140 = ((0x3ffffffffffffffffffff6L + x26) - x30); + uint256_t x141 = (((uint256_t)x137 * x36) + (((uint256_t)x136 * x37) + ((uint256_t)x135 * x38))); + uint256_t x142 = ((((uint256_t)x137 * x37) + ((uint256_t)x136 * x38)) + (0x5 * ((uint256_t)x135 * x36))); + uint256_t x143 = (((uint256_t)x137 * x38) + (0x5 * (((uint256_t)x136 * x36) + ((uint256_t)x135 * x37)))); uint128_t x144 = (uint128_t) (x143 >> 0x55); - uint128_t x145 = (uint128_t) x143 & 0x1fffffffffffffffffffffL; - uint256_t x146 = x144 + x142; + uint128_t x145 = ((uint128_t)x143 & 0x1fffffffffffffffffffffL); + uint256_t x146 = (x144 + x142); uint128_t x147 = (uint128_t) (x146 >> 0x55); - uint128_t x148 = (uint128_t) x146 & 0x1fffffffffffffffffffffL; - uint256_t x149 = x147 + x141; + uint128_t x148 = ((uint128_t)x146 & 0x1fffffffffffffffffffffL); + uint256_t x149 = (x147 + x141); uint128_t x150 = (uint128_t) (x149 >> 0x55); - uint128_t x151 = (uint128_t) x149 & 0x1fffffffffffffffffffffL; - uint128_t x152 = x145 + 0x5 * x150; - uint128_t x153 = x152 >> 0x55; - uint128_t x154 = x152 & 0x1fffffffffffffffffffffL; - uint128_t x155 = x153 + x148; - uint128_t x156 = x155 >> 0x55; - uint128_t x157 = x155 & 0x1fffffffffffffffffffffL; - uint128_t x158 = x156 + x151; - uint256_t x159 = (uint256_t) x140 * x33 + ((uint256_t) x139 * x34 + (uint256_t) x138 * x35); - uint256_t x160 = (uint256_t) x140 * x34 + (uint256_t) x139 * x35 + 0x5 * ((uint256_t) x138 * x33); - uint256_t x161 = (uint256_t) x140 * x35 + 0x5 * ((uint256_t) x139 * x33 + (uint256_t) x138 * x34); + uint128_t x151 = ((uint128_t)x149 & 0x1fffffffffffffffffffffL); + uint128_t x152 = (x145 + (0x5 * x150)); + uint128_t x153 = (x152 >> 0x55); + uint128_t x154 = (x152 & 0x1fffffffffffffffffffffL); + uint128_t x155 = (x153 + x148); + uint128_t x156 = (x155 >> 0x55); + uint128_t x157 = (x155 & 0x1fffffffffffffffffffffL); + uint128_t x158 = (x156 + x151); + uint256_t x159 = (((uint256_t)x140 * x33) + (((uint256_t)x139 * x34) + ((uint256_t)x138 * x35))); + uint256_t x160 = ((((uint256_t)x140 * x34) + ((uint256_t)x139 * x35)) + (0x5 * ((uint256_t)x138 * x33))); + uint256_t x161 = (((uint256_t)x140 * x35) + (0x5 * (((uint256_t)x139 * x33) + ((uint256_t)x138 * x34)))); uint128_t x162 = (uint128_t) (x161 >> 0x55); - uint128_t x163 = (uint128_t) x161 & 0x1fffffffffffffffffffffL; - uint256_t x164 = x162 + x160; + uint128_t x163 = ((uint128_t)x161 & 0x1fffffffffffffffffffffL); + uint256_t x164 = (x162 + x160); uint128_t x165 = (uint128_t) (x164 >> 0x55); - uint128_t x166 = (uint128_t) x164 & 0x1fffffffffffffffffffffL; - uint256_t x167 = x165 + x159; + uint128_t x166 = ((uint128_t)x164 & 0x1fffffffffffffffffffffL); + uint256_t x167 = (x165 + x159); uint128_t x168 = (uint128_t) (x167 >> 0x55); - uint128_t x169 = (uint128_t) x167 & 0x1fffffffffffffffffffffL; - uint128_t x170 = x163 + 0x5 * x168; - uint128_t x171 = x170 >> 0x55; - uint128_t x172 = x170 & 0x1fffffffffffffffffffffL; - uint128_t x173 = x171 + x166; - uint128_t x174 = x173 >> 0x55; - uint128_t x175 = x173 & 0x1fffffffffffffffffffffL; - uint128_t x176 = x174 + x169; - uint128_t x177 = x176 + x158; - uint128_t x178 = x175 + x157; - uint128_t x179 = x172 + x154; - uint128_t x180 = x176 + x158; - uint128_t x181 = x175 + x157; - uint128_t x182 = x172 + x154; - uint256_t x183 = (uint256_t) x179 * x180 + ((uint256_t) x178 * x181 + (uint256_t) x177 * x182); - uint256_t x184 = (uint256_t) x179 * x181 + (uint256_t) x178 * x182 + 0x5 * ((uint256_t) x177 * x180); - uint256_t x185 = (uint256_t) x179 * x182 + 0x5 * ((uint256_t) x178 * x180 + (uint256_t) x177 * x181); + uint128_t x169 = ((uint128_t)x167 & 0x1fffffffffffffffffffffL); + uint128_t x170 = (x163 + (0x5 * x168)); + uint128_t x171 = (x170 >> 0x55); + uint128_t x172 = (x170 & 0x1fffffffffffffffffffffL); + uint128_t x173 = (x171 + x166); + uint128_t x174 = (x173 >> 0x55); + uint128_t x175 = (x173 & 0x1fffffffffffffffffffffL); + uint128_t x176 = (x174 + x169); + uint128_t x177 = (x176 + x158); + uint128_t x178 = (x175 + x157); + uint128_t x179 = (x172 + x154); + uint128_t x180 = (x176 + x158); + uint128_t x181 = (x175 + x157); + uint128_t x182 = (x172 + x154); + uint256_t x183 = (((uint256_t)x179 * x180) + (((uint256_t)x178 * x181) + ((uint256_t)x177 * x182))); + uint256_t x184 = ((((uint256_t)x179 * x181) + ((uint256_t)x178 * x182)) + (0x5 * ((uint256_t)x177 * x180))); + uint256_t x185 = (((uint256_t)x179 * x182) + (0x5 * (((uint256_t)x178 * x180) + ((uint256_t)x177 * x181)))); uint128_t x186 = (uint128_t) (x185 >> 0x55); - uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; - uint256_t x188 = x186 + x184; + uint128_t x187 = ((uint128_t)x185 & 0x1fffffffffffffffffffffL); + uint256_t x188 = (x186 + x184); uint128_t x189 = (uint128_t) (x188 >> 0x55); - uint128_t x190 = (uint128_t) x188 & 0x1fffffffffffffffffffffL; - uint256_t x191 = x189 + x183; + uint128_t x190 = ((uint128_t)x188 & 0x1fffffffffffffffffffffL); + uint256_t x191 = (x189 + x183); uint128_t x192 = (uint128_t) (x191 >> 0x55); - uint128_t x193 = (uint128_t) x191 & 0x1fffffffffffffffffffffL; - uint128_t x194 = x187 + 0x5 * x192; - uint128_t x195 = x194 >> 0x55; - uint128_t x196 = x194 & 0x1fffffffffffffffffffffL; - uint128_t x197 = x195 + x190; - uint128_t x198 = x197 >> 0x55; - uint128_t x199 = x197 & 0x1fffffffffffffffffffffL; - uint128_t x200 = x198 + x193; - uint128_t x201 = 0x3ffffffffffffffffffffeL + x176 - x158; - uint128_t x202 = 0x3ffffffffffffffffffffeL + x175 - x157; - uint128_t x203 = 0x3ffffffffffffffffffff6L + x172 - x154; - uint128_t x204 = 0x3ffffffffffffffffffffeL + x176 - x158; - uint128_t x205 = 0x3ffffffffffffffffffffeL + x175 - x157; - uint128_t x206 = 0x3ffffffffffffffffffff6L + x172 - x154; - uint256_t x207 = (uint256_t) x203 * x204 + ((uint256_t) x202 * x205 + (uint256_t) x201 * x206); - uint256_t x208 = (uint256_t) x203 * x205 + (uint256_t) x202 * x206 + 0x5 * ((uint256_t) x201 * x204); - uint256_t x209 = (uint256_t) x203 * x206 + 0x5 * ((uint256_t) x202 * x204 + (uint256_t) x201 * x205); + uint128_t x193 = ((uint128_t)x191 & 0x1fffffffffffffffffffffL); + uint128_t x194 = (x187 + (0x5 * x192)); + uint128_t x195 = (x194 >> 0x55); + uint128_t x196 = (x194 & 0x1fffffffffffffffffffffL); + uint128_t x197 = (x195 + x190); + uint128_t x198 = (x197 >> 0x55); + uint128_t x199 = (x197 & 0x1fffffffffffffffffffffL); + uint128_t x200 = (x198 + x193); + uint128_t x201 = ((0x3ffffffffffffffffffffeL + x176) - x158); + uint128_t x202 = ((0x3ffffffffffffffffffffeL + x175) - x157); + uint128_t x203 = ((0x3ffffffffffffffffffff6L + x172) - x154); + uint128_t x204 = ((0x3ffffffffffffffffffffeL + x176) - x158); + uint128_t x205 = ((0x3ffffffffffffffffffffeL + x175) - x157); + uint128_t x206 = ((0x3ffffffffffffffffffff6L + x172) - x154); + uint256_t x207 = (((uint256_t)x203 * x204) + (((uint256_t)x202 * x205) + ((uint256_t)x201 * x206))); + uint256_t x208 = ((((uint256_t)x203 * x205) + ((uint256_t)x202 * x206)) + (0x5 * ((uint256_t)x201 * x204))); + uint256_t x209 = (((uint256_t)x203 * x206) + (0x5 * (((uint256_t)x202 * x204) + ((uint256_t)x201 * x205)))); uint128_t x210 = (uint128_t) (x209 >> 0x55); - uint128_t x211 = (uint128_t) x209 & 0x1fffffffffffffffffffffL; - uint256_t x212 = x210 + x208; + uint128_t x211 = ((uint128_t)x209 & 0x1fffffffffffffffffffffL); + uint256_t x212 = (x210 + x208); uint128_t x213 = (uint128_t) (x212 >> 0x55); - uint128_t x214 = (uint128_t) x212 & 0x1fffffffffffffffffffffL; - uint256_t x215 = x213 + x207; + uint128_t x214 = ((uint128_t)x212 & 0x1fffffffffffffffffffffL); + uint256_t x215 = (x213 + x207); uint128_t x216 = (uint128_t) (x215 >> 0x55); - uint128_t x217 = (uint128_t) x215 & 0x1fffffffffffffffffffffL; - uint128_t x218 = x211 + 0x5 * x216; - uint128_t x219 = x218 >> 0x55; - uint128_t x220 = x218 & 0x1fffffffffffffffffffffL; - uint128_t x221 = x219 + x214; - uint128_t x222 = x221 >> 0x55; - uint128_t x223 = x221 & 0x1fffffffffffffffffffffL; - uint128_t x224 = x222 + x217; - uint256_t x225 = (uint256_t) x10 * x224 + ((uint256_t) x12 * x223 + (uint256_t) x11 * x220); - uint256_t x226 = (uint256_t) x10 * x223 + (uint256_t) x12 * x220 + 0x5 * ((uint256_t) x11 * x224); - uint256_t x227 = (uint256_t) x10 * x220 + 0x5 * ((uint256_t) x12 * x224 + (uint256_t) x11 * x223); + uint128_t x217 = ((uint128_t)x215 & 0x1fffffffffffffffffffffL); + uint128_t x218 = (x211 + (0x5 * x216)); + uint128_t x219 = (x218 >> 0x55); + uint128_t x220 = (x218 & 0x1fffffffffffffffffffffL); + uint128_t x221 = (x219 + x214); + uint128_t x222 = (x221 >> 0x55); + uint128_t x223 = (x221 & 0x1fffffffffffffffffffffL); + uint128_t x224 = (x222 + x217); + uint256_t x225 = (((uint256_t)x10 * x224) + (((uint256_t)x12 * x223) + ((uint256_t)x11 * x220))); + uint256_t x226 = ((((uint256_t)x10 * x223) + ((uint256_t)x12 * x220)) + (0x5 * ((uint256_t)x11 * x224))); + uint256_t x227 = (((uint256_t)x10 * x220) + (0x5 * (((uint256_t)x12 * x224) + ((uint256_t)x11 * x223)))); uint128_t x228 = (uint128_t) (x227 >> 0x55); - uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; - uint256_t x230 = x228 + x226; + uint128_t x229 = ((uint128_t)x227 & 0x1fffffffffffffffffffffL); + uint256_t x230 = (x228 + x226); uint128_t x231 = (uint128_t) (x230 >> 0x55); - uint128_t x232 = (uint128_t) x230 & 0x1fffffffffffffffffffffL; - uint256_t x233 = x231 + x225; + uint128_t x232 = ((uint128_t)x230 & 0x1fffffffffffffffffffffL); + uint256_t x233 = (x231 + x225); uint128_t x234 = (uint128_t) (x233 >> 0x55); - uint128_t x235 = (uint128_t) x233 & 0x1fffffffffffffffffffffL; - uint128_t x236 = x229 + 0x5 * x234; - uint128_t x237 = x236 >> 0x55; - uint128_t x238 = x236 & 0x1fffffffffffffffffffffL; - uint128_t x239 = x237 + x232; - uint128_t x240 = x239 >> 0x55; - uint128_t x241 = x239 & 0x1fffffffffffffffffffffL; - uint128_t x242 = x240 + x235; + uint128_t x235 = ((uint128_t)x233 & 0x1fffffffffffffffffffffL); + uint128_t x236 = (x229 + (0x5 * x234)); + uint128_t x237 = (x236 >> 0x55); + uint128_t x238 = (x236 & 0x1fffffffffffffffffffffL); + uint128_t x239 = (x237 + x232); + uint128_t x240 = (x239 >> 0x55); + uint128_t x241 = (x239 & 0x1fffffffffffffffffffffL); + uint128_t x242 = (x240 + x235); return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238)))) (x, (x0, x1), (x2, x3))%core in (let (a0, b0) := a in |