make display

5 files changed, 543 insertions, 543 deletions

diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log
index 77239ffb7..e823c43e0 100644
--- a/src/Specific/IntegrationTestLadderstep130Display.log
+++ b/src/Specific/IntegrationTestLadderstep130Display.log
@@ -11,101 +11,101 @@ let (a, b) := Interp-η
  uint128_t x39 = x38 - x22;
  uint128_t x40 = 0x3ffffffffffffffffffff6L + x16;
  uint128_t x41 = x40 - x20;
- uint256_t x42 = (uint256_t) x35 * (uint256_t) x33;
- uint256_t x43 = (uint256_t) x34 * (uint256_t) x34;
- uint256_t x44 = (uint256_t) x33 * (uint256_t) x35;
+ uint256_t x42 = (uint256_t) x35 * x33;
+ uint256_t x43 = (uint256_t) x34 * x34;
+ uint256_t x44 = (uint256_t) x33 * x35;
  uint256_t x45 = x43 + x44;
  uint256_t x46 = x42 + x45;
- uint256_t x47 = (uint256_t) x35 * (uint256_t) x34;
- uint256_t x48 = (uint256_t) x34 * (uint256_t) x35;
+ uint256_t x47 = (uint256_t) x35 * x34;
+ uint256_t x48 = (uint256_t) x34 * x35;
  uint256_t x49 = x47 + x48;
- uint256_t x50 = (uint256_t) x33 * (uint256_t) x33;
- uint256_t x51 = (uint256_t) 0x5 * x50;
+ uint256_t x50 = (uint256_t) x33 * x33;
+ uint256_t x51 = 0x5 * x50;
  uint256_t x52 = x49 + x51;
- uint256_t x53 = (uint256_t) x35 * (uint256_t) x35;
- uint256_t x54 = (uint256_t) x34 * (uint256_t) x33;
- uint256_t x55 = (uint256_t) x33 * (uint256_t) x34;
+ uint256_t x53 = (uint256_t) x35 * x35;
+ uint256_t x54 = (uint256_t) x34 * x33;
+ uint256_t x55 = (uint256_t) x33 * x34;
  uint256_t x56 = x54 + x55;
- uint256_t x57 = (uint256_t) 0x5 * x56;
+ uint256_t x57 = 0x5 * x56;
  uint256_t x58 = x53 + x57;
  uint128_t x59 = (uint128_t) (x58 >> 0x55);
- uint256_t x60 = (uint256_t) x59 + x52;
+ uint256_t x60 = x59 + x52;
  uint128_t x61 = (uint128_t) (x60 >> 0x55);
- uint256_t x62 = (uint256_t) x61 + x46;
+ 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 = (uint128_t) (x66 >> 0x55);
+ uint128_t x67 = x66 >> 0x55;
  uint128_t x68 = (uint128_t) x60 & 0x1fffffffffffffffffffffL;
  uint128_t x69 = x67 + x68;
- uint128_t x70 = (uint128_t) (x69 >> 0x55);
+ 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;
- uint256_t x75 = (uint256_t) x41 * (uint256_t) x37;
- uint256_t x76 = (uint256_t) x39 * (uint256_t) x39;
- uint256_t x77 = (uint256_t) x37 * (uint256_t) x41;
+ uint256_t x75 = (uint256_t) x41 * x37;
+ uint256_t x76 = (uint256_t) x39 * x39;
+ uint256_t x77 = (uint256_t) x37 * x41;
  uint256_t x78 = x76 + x77;
  uint256_t x79 = x75 + x78;
- uint256_t x80 = (uint256_t) x41 * (uint256_t) x39;
- uint256_t x81 = (uint256_t) x39 * (uint256_t) x41;
+ uint256_t x80 = (uint256_t) x41 * x39;
+ uint256_t x81 = (uint256_t) x39 * x41;
  uint256_t x82 = x80 + x81;
- uint256_t x83 = (uint256_t) x37 * (uint256_t) x37;
- uint256_t x84 = (uint256_t) 0x5 * x83;
+ uint256_t x83 = (uint256_t) x37 * x37;
+ uint256_t x84 = 0x5 * x83;
  uint256_t x85 = x82 + x84;
- uint256_t x86 = (uint256_t) x41 * (uint256_t) x41;
- uint256_t x87 = (uint256_t) x39 * (uint256_t) x37;
- uint256_t x88 = (uint256_t) x37 * (uint256_t) x39;
+ uint256_t x86 = (uint256_t) x41 * x41;
+ uint256_t x87 = (uint256_t) x39 * x37;
+ uint256_t x88 = (uint256_t) x37 * x39;
  uint256_t x89 = x87 + x88;
- uint256_t x90 = (uint256_t) 0x5 * x89;
+ uint256_t x90 = 0x5 * x89;
  uint256_t x91 = x86 + x90;
  uint128_t x92 = (uint128_t) (x91 >> 0x55);
- uint256_t x93 = (uint256_t) x92 + x85;
+ uint256_t x93 = x92 + x85;
  uint128_t x94 = (uint128_t) (x93 >> 0x55);
- uint256_t x95 = (uint256_t) x94 + x79;
+ 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 = (uint128_t) (x99 >> 0x55);
+ uint128_t x100 = x99 >> 0x55;
  uint128_t x101 = (uint128_t) x93 & 0x1fffffffffffffffffffffL;
  uint128_t x102 = x100 + x101;
- uint128_t x103 = (uint128_t) (x102 >> 0x55);
+ 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 * (uint256_t) x105;
- uint256_t x109 = (uint256_t) x73 * (uint256_t) x106;
- uint256_t x110 = (uint256_t) x72 * (uint256_t) x107;
+ uint256_t x108 = (uint256_t) x74 * x105;
+ uint256_t x109 = (uint256_t) x73 * x106;
+ uint256_t x110 = (uint256_t) x72 * x107;
  uint256_t x111 = x109 + x110;
  uint256_t x112 = x108 + x111;
- uint256_t x113 = (uint256_t) x74 * (uint256_t) x106;
- uint256_t x114 = (uint256_t) x73 * (uint256_t) x107;
+ uint256_t x113 = (uint256_t) x74 * x106;
+ uint256_t x114 = (uint256_t) x73 * x107;
  uint256_t x115 = x113 + x114;
- uint256_t x116 = (uint256_t) x72 * (uint256_t) x105;
- uint256_t x117 = (uint256_t) 0x5 * x116;
+ uint256_t x116 = (uint256_t) x72 * x105;
+ uint256_t x117 = 0x5 * x116;
  uint256_t x118 = x115 + x117;
- uint256_t x119 = (uint256_t) x74 * (uint256_t) x107;
- uint256_t x120 = (uint256_t) x73 * (uint256_t) x105;
- uint256_t x121 = (uint256_t) x72 * (uint256_t) x106;
+ uint256_t x119 = (uint256_t) x74 * x107;
+ uint256_t x120 = (uint256_t) x73 * x105;
+ uint256_t x121 = (uint256_t) x72 * x106;
  uint256_t x122 = x120 + x121;
- uint256_t x123 = (uint256_t) 0x5 * x122;
+ uint256_t x123 = 0x5 * x122;
  uint256_t x124 = x119 + x123;
  uint128_t x125 = (uint128_t) (x124 >> 0x55);
- uint256_t x126 = (uint256_t) x125 + x118;
+ uint256_t x126 = x125 + x118;
  uint128_t x127 = (uint128_t) (x126 >> 0x55);
- uint256_t x128 = (uint256_t) x127 + x112;
+ 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 = (uint128_t) (x132 >> 0x55);
+ uint128_t x133 = x132 >> 0x55;
  uint128_t x134 = (uint128_t) x126 & 0x1fffffffffffffffffffffL;
  uint128_t x135 = x133 + x134;
- uint128_t x136 = (uint128_t) (x135 >> 0x55);
+ uint128_t x136 = x135 >> 0x55;
  uint128_t x137 = (uint128_t) x128 & 0x1fffffffffffffffffffffL;
  uint128_t x138 = x136 + x137;
  uint128_t x139 = x135 & 0x1fffffffffffffffffffffL;
@@ -119,18 +119,18 @@ let (a, b) := Interp-η
  uint128_t x147 = 0x1db41 * x142;
  uint128_t x148 = 0x1db41 * x144;
  uint128_t x149 = 0x1db41 * x146;
- uint128_t x150 = (uint128_t) (x149 >> 0x55);
+ uint128_t x150 = x149 >> 0x55;
  uint128_t x151 = x150 + x148;
- uint128_t x152 = (uint128_t) (x151 >> 0x55);
+ uint128_t x152 = x151 >> 0x55;
  uint128_t x153 = x152 + x147;
  uint128_t x154 = x149 & 0x1fffffffffffffffffffffL;
- uint128_t x155 = (uint128_t) (x153 >> 0x55);
+ uint128_t x155 = x153 >> 0x55;
  uint128_t x156 = 0x5 * x155;
  uint128_t x157 = x154 + x156;
- uint128_t x158 = (uint128_t) (x157 >> 0x55);
+ uint128_t x158 = x157 >> 0x55;
  uint128_t x159 = x151 & 0x1fffffffffffffffffffffL;
  uint128_t x160 = x158 + x159;
- uint128_t x161 = (uint128_t) (x160 >> 0x55);
+ uint128_t x161 = x160 >> 0x55;
  uint128_t x162 = x153 & 0x1fffffffffffffffffffffL;
  uint128_t x163 = x161 + x162;
  uint128_t x164 = x160 & 0x1fffffffffffffffffffffL;
@@ -138,35 +138,35 @@ let (a, b) := Interp-η
  uint128_t x166 = x72 + x163;
  uint128_t x167 = x73 + x164;
  uint128_t x168 = x74 + x165;
- uint256_t x169 = (uint256_t) x146 * (uint256_t) x166;
- uint256_t x170 = (uint256_t) x144 * (uint256_t) x167;
- uint256_t x171 = (uint256_t) x142 * (uint256_t) x168;
+ uint256_t x169 = (uint256_t) x146 * x166;
+ uint256_t x170 = (uint256_t) x144 * x167;
+ uint256_t x171 = (uint256_t) x142 * x168;
  uint256_t x172 = x170 + x171;
  uint256_t x173 = x169 + x172;
- uint256_t x174 = (uint256_t) x146 * (uint256_t) x167;
- uint256_t x175 = (uint256_t) x144 * (uint256_t) x168;
+ uint256_t x174 = (uint256_t) x146 * x167;
+ uint256_t x175 = (uint256_t) x144 * x168;
  uint256_t x176 = x174 + x175;
- uint256_t x177 = (uint256_t) x142 * (uint256_t) x166;
- uint256_t x178 = (uint256_t) 0x5 * x177;
+ uint256_t x177 = (uint256_t) x142 * x166;
+ uint256_t x178 = 0x5 * x177;
  uint256_t x179 = x176 + x178;
- uint256_t x180 = (uint256_t) x146 * (uint256_t) x168;
- uint256_t x181 = (uint256_t) x144 * (uint256_t) x166;
- uint256_t x182 = (uint256_t) x142 * (uint256_t) x167;
+ uint256_t x180 = (uint256_t) x146 * x168;
+ uint256_t x181 = (uint256_t) x144 * x166;
+ uint256_t x182 = (uint256_t) x142 * x167;
  uint256_t x183 = x181 + x182;
- uint256_t x184 = (uint256_t) 0x5 * x183;
+ uint256_t x184 = 0x5 * x183;
  uint256_t x185 = x180 + x184;
  uint128_t x186 = (uint128_t) (x185 >> 0x55);
- uint256_t x187 = (uint256_t) x186 + x179;
+ uint256_t x187 = x186 + x179;
  uint128_t x188 = (uint128_t) (x187 >> 0x55);
- uint256_t x189 = (uint256_t) x188 + x173;
+ 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 = (uint128_t) (x193 >> 0x55);
+ uint128_t x194 = x193 >> 0x55;
  uint128_t x195 = (uint128_t) x187 & 0x1fffffffffffffffffffffL;
  uint128_t x196 = x194 + x195;
- uint128_t x197 = (uint128_t) (x196 >> 0x55);
+ uint128_t x197 = x196 >> 0x55;
  uint128_t x198 = (uint128_t) x189 & 0x1fffffffffffffffffffffL;
  uint128_t x199 = x197 + x198;
  uint128_t x200 = x196 & 0x1fffffffffffffffffffffL;
@@ -180,68 +180,68 @@ let (a, b) := Interp-η
  uint128_t x208 = x207 - x32;
  uint128_t x209 = 0x3ffffffffffffffffffff6L + x26;
  uint128_t x210 = x209 - x30;
- uint256_t x211 = (uint256_t) x204 * (uint256_t) x37;
- uint256_t x212 = (uint256_t) x203 * (uint256_t) x39;
- uint256_t x213 = (uint256_t) x202 * (uint256_t) x41;
+ uint256_t x211 = (uint256_t) x204 * x37;
+ uint256_t x212 = (uint256_t) x203 * x39;
+ uint256_t x213 = (uint256_t) x202 * x41;
  uint256_t x214 = x212 + x213;
  uint256_t x215 = x211 + x214;
- uint256_t x216 = (uint256_t) x204 * (uint256_t) x39;
- uint256_t x217 = (uint256_t) x203 * (uint256_t) x41;
+ uint256_t x216 = (uint256_t) x204 * x39;
+ uint256_t x217 = (uint256_t) x203 * x41;
  uint256_t x218 = x216 + x217;
- uint256_t x219 = (uint256_t) x202 * (uint256_t) x37;
- uint256_t x220 = (uint256_t) 0x5 * x219;
+ uint256_t x219 = (uint256_t) x202 * x37;
+ uint256_t x220 = 0x5 * x219;
  uint256_t x221 = x218 + x220;
- uint256_t x222 = (uint256_t) x204 * (uint256_t) x41;
- uint256_t x223 = (uint256_t) x203 * (uint256_t) x37;
- uint256_t x224 = (uint256_t) x202 * (uint256_t) x39;
+ uint256_t x222 = (uint256_t) x204 * x41;
+ uint256_t x223 = (uint256_t) x203 * x37;
+ uint256_t x224 = (uint256_t) x202 * x39;
  uint256_t x225 = x223 + x224;
- uint256_t x226 = (uint256_t) 0x5 * x225;
+ uint256_t x226 = 0x5 * x225;
  uint256_t x227 = x222 + x226;
  uint128_t x228 = (uint128_t) (x227 >> 0x55);
- uint256_t x229 = (uint256_t) x228 + x221;
+ uint256_t x229 = x228 + x221;
  uint128_t x230 = (uint128_t) (x229 >> 0x55);
- uint256_t x231 = (uint256_t) x230 + x215;
+ 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 = (uint128_t) (x235 >> 0x55);
+ uint128_t x236 = x235 >> 0x55;
  uint128_t x237 = (uint128_t) x229 & 0x1fffffffffffffffffffffL;
  uint128_t x238 = x236 + x237;
- uint128_t x239 = (uint128_t) (x238 >> 0x55);
+ 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;
- uint256_t x244 = (uint256_t) x210 * (uint256_t) x33;
- uint256_t x245 = (uint256_t) x208 * (uint256_t) x34;
- uint256_t x246 = (uint256_t) x206 * (uint256_t) x35;
+ uint256_t x244 = (uint256_t) x210 * x33;
+ uint256_t x245 = (uint256_t) x208 * x34;
+ uint256_t x246 = (uint256_t) x206 * x35;
  uint256_t x247 = x245 + x246;
  uint256_t x248 = x244 + x247;
- uint256_t x249 = (uint256_t) x210 * (uint256_t) x34;
- uint256_t x250 = (uint256_t) x208 * (uint256_t) x35;
+ uint256_t x249 = (uint256_t) x210 * x34;
+ uint256_t x250 = (uint256_t) x208 * x35;
  uint256_t x251 = x249 + x250;
- uint256_t x252 = (uint256_t) x206 * (uint256_t) x33;
- uint256_t x253 = (uint256_t) 0x5 * x252;
+ uint256_t x252 = (uint256_t) x206 * x33;
+ uint256_t x253 = 0x5 * x252;
  uint256_t x254 = x251 + x253;
- uint256_t x255 = (uint256_t) x210 * (uint256_t) x35;
- uint256_t x256 = (uint256_t) x208 * (uint256_t) x33;
- uint256_t x257 = (uint256_t) x206 * (uint256_t) x34;
+ uint256_t x255 = (uint256_t) x210 * x35;
+ uint256_t x256 = (uint256_t) x208 * x33;
+ uint256_t x257 = (uint256_t) x206 * x34;
  uint256_t x258 = x256 + x257;
- uint256_t x259 = (uint256_t) 0x5 * x258;
+ uint256_t x259 = 0x5 * x258;
  uint256_t x260 = x255 + x259;
  uint128_t x261 = (uint128_t) (x260 >> 0x55);
- uint256_t x262 = (uint256_t) x261 + x254;
+ uint256_t x262 = x261 + x254;
  uint128_t x263 = (uint128_t) (x262 >> 0x55);
- uint256_t x264 = (uint256_t) x263 + x248;
+ 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 = (uint128_t) (x268 >> 0x55);
+ uint128_t x269 = x268 >> 0x55;
  uint128_t x270 = (uint128_t) x262 & 0x1fffffffffffffffffffffL;
  uint128_t x271 = x269 + x270;
- uint128_t x272 = (uint128_t) (x271 >> 0x55);
+ uint128_t x272 = x271 >> 0x55;
  uint128_t x273 = (uint128_t) x264 & 0x1fffffffffffffffffffffL;
  uint128_t x274 = x272 + x273;
  uint128_t x275 = x271 & 0x1fffffffffffffffffffffL;
@@ -252,35 +252,35 @@ let (a, b) := Interp-η
  uint128_t x280 = x274 + x241;
  uint128_t x281 = x275 + x242;
  uint128_t x282 = x276 + x243;
- uint256_t x283 = (uint256_t) x279 * (uint256_t) x280;
- uint256_t x284 = (uint256_t) x278 * (uint256_t) x281;
- uint256_t x285 = (uint256_t) x277 * (uint256_t) x282;
+ uint256_t x283 = (uint256_t) x279 * x280;
+ uint256_t x284 = (uint256_t) x278 * x281;
+ uint256_t x285 = (uint256_t) x277 * x282;
  uint256_t x286 = x284 + x285;
  uint256_t x287 = x283 + x286;
- uint256_t x288 = (uint256_t) x279 * (uint256_t) x281;
- uint256_t x289 = (uint256_t) x278 * (uint256_t) x282;
+ uint256_t x288 = (uint256_t) x279 * x281;
+ uint256_t x289 = (uint256_t) x278 * x282;
  uint256_t x290 = x288 + x289;
- uint256_t x291 = (uint256_t) x277 * (uint256_t) x280;
- uint256_t x292 = (uint256_t) 0x5 * x291;
+ uint256_t x291 = (uint256_t) x277 * x280;
+ uint256_t x292 = 0x5 * x291;
  uint256_t x293 = x290 + x292;
- uint256_t x294 = (uint256_t) x279 * (uint256_t) x282;
- uint256_t x295 = (uint256_t) x278 * (uint256_t) x280;
- uint256_t x296 = (uint256_t) x277 * (uint256_t) x281;
+ uint256_t x294 = (uint256_t) x279 * x282;
+ uint256_t x295 = (uint256_t) x278 * x280;
+ uint256_t x296 = (uint256_t) x277 * x281;
  uint256_t x297 = x295 + x296;
- uint256_t x298 = (uint256_t) 0x5 * x297;
+ uint256_t x298 = 0x5 * x297;
  uint256_t x299 = x294 + x298;
  uint128_t x300 = (uint128_t) (x299 >> 0x55);
- uint256_t x301 = (uint256_t) x300 + x293;
+ uint256_t x301 = x300 + x293;
  uint128_t x302 = (uint128_t) (x301 >> 0x55);
- uint256_t x303 = (uint256_t) x302 + x287;
+ 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 = (uint128_t) (x307 >> 0x55);
+ uint128_t x308 = x307 >> 0x55;
  uint128_t x309 = (uint128_t) x301 & 0x1fffffffffffffffffffffL;
  uint128_t x310 = x308 + x309;
- uint128_t x311 = (uint128_t) (x310 >> 0x55);
+ uint128_t x311 = x310 >> 0x55;
  uint128_t x312 = (uint128_t) x303 & 0x1fffffffffffffffffffffL;
  uint128_t x313 = x311 + x312;
  uint128_t x314 = x310 & 0x1fffffffffffffffffffffL;
@@ -297,68 +297,68 @@ let (a, b) := Interp-η
  uint128_t x325 = x324 - x242;
  uint128_t x326 = 0x3ffffffffffffffffffff6L + x276;
  uint128_t x327 = x326 - x243;
- uint256_t x328 = (uint256_t) x321 * (uint256_t) x323;
- uint256_t x329 = (uint256_t) x319 * (uint256_t) x325;
- uint256_t x330 = (uint256_t) x317 * (uint256_t) x327;
+ uint256_t x328 = (uint256_t) x321 * x323;
+ uint256_t x329 = (uint256_t) x319 * x325;
+ uint256_t x330 = (uint256_t) x317 * x327;
  uint256_t x331 = x329 + x330;
  uint256_t x332 = x328 + x331;
- uint256_t x333 = (uint256_t) x321 * (uint256_t) x325;
- uint256_t x334 = (uint256_t) x319 * (uint256_t) x327;
+ uint256_t x333 = (uint256_t) x321 * x325;
+ uint256_t x334 = (uint256_t) x319 * x327;
  uint256_t x335 = x333 + x334;
- uint256_t x336 = (uint256_t) x317 * (uint256_t) x323;
- uint256_t x337 = (uint256_t) 0x5 * x336;
+ uint256_t x336 = (uint256_t) x317 * x323;
+ uint256_t x337 = 0x5 * x336;
  uint256_t x338 = x335 + x337;
- uint256_t x339 = (uint256_t) x321 * (uint256_t) x327;
- uint256_t x340 = (uint256_t) x319 * (uint256_t) x323;
- uint256_t x341 = (uint256_t) x317 * (uint256_t) x325;
+ uint256_t x339 = (uint256_t) x321 * x327;
+ uint256_t x340 = (uint256_t) x319 * x323;
+ uint256_t x341 = (uint256_t) x317 * x325;
  uint256_t x342 = x340 + x341;
- uint256_t x343 = (uint256_t) 0x5 * x342;
+ uint256_t x343 = 0x5 * x342;
  uint256_t x344 = x339 + x343;
  uint128_t x345 = (uint128_t) (x344 >> 0x55);
- uint256_t x346 = (uint256_t) x345 + x338;
+ uint256_t x346 = x345 + x338;
  uint128_t x347 = (uint128_t) (x346 >> 0x55);
- uint256_t x348 = (uint256_t) x347 + x332;
+ 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 = (uint128_t) (x352 >> 0x55);
+ uint128_t x353 = x352 >> 0x55;
  uint128_t x354 = (uint128_t) x346 & 0x1fffffffffffffffffffffL;
  uint128_t x355 = x353 + x354;
- uint128_t x356 = (uint128_t) (x355 >> 0x55);
+ 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 * (uint256_t) x358;
- uint256_t x362 = (uint256_t) x12 * (uint256_t) x359;
- uint256_t x363 = (uint256_t) x11 * (uint256_t) x360;
+ uint256_t x361 = (uint256_t) x10 * x358;
+ uint256_t x362 = (uint256_t) x12 * x359;
+ uint256_t x363 = (uint256_t) x11 * x360;
  uint256_t x364 = x362 + x363;
  uint256_t x365 = x361 + x364;
- uint256_t x366 = (uint256_t) x10 * (uint256_t) x359;
- uint256_t x367 = (uint256_t) x12 * (uint256_t) x360;
+ uint256_t x366 = (uint256_t) x10 * x359;
+ uint256_t x367 = (uint256_t) x12 * x360;
  uint256_t x368 = x366 + x367;
- uint256_t x369 = (uint256_t) x11 * (uint256_t) x358;
- uint256_t x370 = (uint256_t) 0x5 * x369;
+ uint256_t x369 = (uint256_t) x11 * x358;
+ uint256_t x370 = 0x5 * x369;
  uint256_t x371 = x368 + x370;
- uint256_t x372 = (uint256_t) x10 * (uint256_t) x360;
- uint256_t x373 = (uint256_t) x12 * (uint256_t) x358;
- uint256_t x374 = (uint256_t) x11 * (uint256_t) x359;
+ uint256_t x372 = (uint256_t) x10 * x360;
+ uint256_t x373 = (uint256_t) x12 * x358;
+ uint256_t x374 = (uint256_t) x11 * x359;
  uint256_t x375 = x373 + x374;
- uint256_t x376 = (uint256_t) 0x5 * x375;
+ uint256_t x376 = 0x5 * x375;
  uint256_t x377 = x372 + x376;
  uint128_t x378 = (uint128_t) (x377 >> 0x55);
- uint256_t x379 = (uint256_t) x378 + x371;
+ uint256_t x379 = x378 + x371;
  uint128_t x380 = (uint128_t) (x379 >> 0x55);
- uint256_t x381 = (uint256_t) x380 + x365;
+ 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 = (uint128_t) (x385 >> 0x55);
+ uint128_t x386 = x385 >> 0x55;
  uint128_t x387 = (uint128_t) x379 & 0x1fffffffffffffffffffffL;
  uint128_t x388 = x386 + x387;
- uint128_t x389 = (uint128_t) (x388 >> 0x55);
+ uint128_t x389 = x388 >> 0x55;
  uint128_t x390 = (uint128_t) x381 & 0x1fffffffffffffffffffffL;
  uint128_t x391 = x389 + x390;
  uint128_t x392 = x388 & 0x1fffffffffffffffffffffL;
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index c01911c2d..9007985cf 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -17,215 +17,215 @@ let (a, b) := Interp-η
  uint64_t x65 = x64 - x30;
  uint64_t x66 = 0xfffffffffffda + x20;
  uint64_t x67 = x66 - x28;
- uint128_t x68 = (uint128_t) x57 * (uint128_t) x53;
- uint128_t x69 = (uint128_t) x56 * (uint128_t) x54;
- uint128_t x70 = (uint128_t) x55 * (uint128_t) x55;
- uint128_t x71 = (uint128_t) x54 * (uint128_t) x56;
- uint128_t x72 = (uint128_t) x53 * (uint128_t) x57;
+ uint128_t x68 = (uint128_t) x57 * x53;
+ uint128_t x69 = (uint128_t) x56 * x54;
+ uint128_t x70 = (uint128_t) x55 * x55;
+ uint128_t x71 = (uint128_t) x54 * x56;
+ uint128_t x72 = (uint128_t) x53 * x57;
  uint128_t x73 = x71 + x72;
  uint128_t x74 = x70 + x73;
  uint128_t x75 = x69 + x74;
  uint128_t x76 = x68 + x75;
- uint128_t x77 = (uint128_t) x57 * (uint128_t) x54;
- uint128_t x78 = (uint128_t) x56 * (uint128_t) x55;
- uint128_t x79 = (uint128_t) x55 * (uint128_t) x56;
- uint128_t x80 = (uint128_t) x54 * (uint128_t) x57;
+ uint128_t x77 = (uint128_t) x57 * x54;
+ uint128_t x78 = (uint128_t) x56 * x55;
+ uint128_t x79 = (uint128_t) x55 * x56;
+ uint128_t x80 = (uint128_t) x54 * x57;
  uint128_t x81 = x79 + x80;
  uint128_t x82 = x78 + x81;
  uint128_t x83 = x77 + x82;
- uint128_t x84 = (uint128_t) x53 * (uint128_t) x53;
- uint128_t x85 = (uint128_t) 0x13 * x84;
+ uint128_t x84 = (uint128_t) x53 * x53;
+ uint128_t x85 = 0x13 * x84;
  uint128_t x86 = x83 + x85;
- uint128_t x87 = (uint128_t) x57 * (uint128_t) x55;
- uint128_t x88 = (uint128_t) x56 * (uint128_t) x56;
- uint128_t x89 = (uint128_t) x55 * (uint128_t) x57;
+ uint128_t x87 = (uint128_t) x57 * x55;
+ uint128_t x88 = (uint128_t) x56 * x56;
+ uint128_t x89 = (uint128_t) x55 * x57;
  uint128_t x90 = x88 + x89;
  uint128_t x91 = x87 + x90;
- uint128_t x92 = (uint128_t) x54 * (uint128_t) x53;
- uint128_t x93 = (uint128_t) x53 * (uint128_t) x54;
+ uint128_t x92 = (uint128_t) x54 * x53;
+ uint128_t x93 = (uint128_t) x53 * x54;
  uint128_t x94 = x92 + x93;
- uint128_t x95 = (uint128_t) 0x13 * x94;
+ uint128_t x95 = 0x13 * x94;
  uint128_t x96 = x91 + x95;
- uint128_t x97 = (uint128_t) x57 * (uint128_t) x56;
- uint128_t x98 = (uint128_t) x56 * (uint128_t) x57;
+ uint128_t x97 = (uint128_t) x57 * x56;
+ uint128_t x98 = (uint128_t) x56 * x57;
  uint128_t x99 = x97 + x98;
- uint128_t x100 = (uint128_t) x55 * (uint128_t) x53;
- uint128_t x101 = (uint128_t) x54 * (uint128_t) x54;
- uint128_t x102 = (uint128_t) x53 * (uint128_t) x55;
+ uint128_t x100 = (uint128_t) x55 * x53;
+ uint128_t x101 = (uint128_t) x54 * x54;
+ uint128_t x102 = (uint128_t) x53 * x55;
  uint128_t x103 = x101 + x102;
  uint128_t x104 = x100 + x103;
- uint128_t x105 = (uint128_t) 0x13 * x104;
+ uint128_t x105 = 0x13 * x104;
  uint128_t x106 = x99 + x105;
- uint128_t x107 = (uint128_t) x57 * (uint128_t) x57;
- uint128_t x108 = (uint128_t) x56 * (uint128_t) x53;
- uint128_t x109 = (uint128_t) x55 * (uint128_t) x54;
- uint128_t x110 = (uint128_t) x54 * (uint128_t) x55;
- uint128_t x111 = (uint128_t) x53 * (uint128_t) x56;
+ uint128_t x107 = (uint128_t) x57 * x57;
+ uint128_t x108 = (uint128_t) x56 * x53;
+ uint128_t x109 = (uint128_t) x55 * x54;
+ uint128_t x110 = (uint128_t) x54 * x55;
+ uint128_t x111 = (uint128_t) x53 * x56;
  uint128_t x112 = x110 + x111;
  uint128_t x113 = x109 + x112;
  uint128_t x114 = x108 + x113;
- uint128_t x115 = (uint128_t) 0x13 * x114;
+ uint128_t x115 = 0x13 * x114;
  uint128_t x116 = x107 + x115;
  uint64_t x117 = (uint64_t) (x116 >> 0x33);
- uint128_t x118 = (uint128_t) x117 + x106;
+ uint128_t x118 = x117 + x106;
  uint64_t x119 = (uint64_t) (x118 >> 0x33);
- uint128_t x120 = (uint128_t) x119 + x96;
+ uint128_t x120 = x119 + x96;
  uint64_t x121 = (uint64_t) (x120 >> 0x33);
- uint128_t x122 = (uint128_t) x121 + x86;
+ uint128_t x122 = x121 + x86;
  uint64_t x123 = (uint64_t) (x122 >> 0x33);
- uint128_t x124 = (uint128_t) x123 + x76;
+ uint128_t x124 = x123 + x76;
  uint64_t x125 = (uint64_t) x116 & 0x7ffffffffffff;
  uint64_t x126 = (uint64_t) (x124 >> 0x33);
  uint64_t x127 = 0x13 * x126;
  uint64_t x128 = x125 + x127;
- uint64_t x129 = (uint64_t) (x128 >> 0x33);
+ uint64_t x129 = x128 >> 0x33;
  uint64_t x130 = (uint64_t) x118 & 0x7ffffffffffff;
  uint64_t x131 = x129 + x130;
  uint64_t x132 = (uint64_t) x124 & 0x7ffffffffffff;
  uint64_t x133 = (uint64_t) x122 & 0x7ffffffffffff;
- uint64_t x134 = (uint64_t) (x131 >> 0x33);
+ uint64_t x134 = x131 >> 0x33;
  uint64_t x135 = (uint64_t) x120 & 0x7ffffffffffff;
  uint64_t x136 = x134 + x135;
  uint64_t x137 = x131 & 0x7ffffffffffff;
  uint64_t x138 = x128 & 0x7ffffffffffff;
- uint128_t x139 = (uint128_t) x67 * (uint128_t) x59;
- uint128_t x140 = (uint128_t) x65 * (uint128_t) x61;
- uint128_t x141 = (uint128_t) x63 * (uint128_t) x63;
- uint128_t x142 = (uint128_t) x61 * (uint128_t) x65;
- uint128_t x143 = (uint128_t) x59 * (uint128_t) x67;
+ uint128_t x139 = (uint128_t) x67 * x59;
+ uint128_t x140 = (uint128_t) x65 * x61;
+ uint128_t x141 = (uint128_t) x63 * x63;
+ uint128_t x142 = (uint128_t) x61 * x65;
+ uint128_t x143 = (uint128_t) x59 * x67;
  uint128_t x144 = x142 + x143;
  uint128_t x145 = x141 + x144;
  uint128_t x146 = x140 + x145;
  uint128_t x147 = x139 + x146;
- uint128_t x148 = (uint128_t) x67 * (uint128_t) x61;
- uint128_t x149 = (uint128_t) x65 * (uint128_t) x63;
- uint128_t x150 = (uint128_t) x63 * (uint128_t) x65;
- uint128_t x151 = (uint128_t) x61 * (uint128_t) x67;
+ uint128_t x148 = (uint128_t) x67 * x61;
+ uint128_t x149 = (uint128_t) x65 * x63;
+ uint128_t x150 = (uint128_t) x63 * x65;
+ uint128_t x151 = (uint128_t) x61 * x67;
  uint128_t x152 = x150 + x151;
  uint128_t x153 = x149 + x152;
  uint128_t x154 = x148 + x153;
- uint128_t x155 = (uint128_t) x59 * (uint128_t) x59;
- uint128_t x156 = (uint128_t) 0x13 * x155;
+ uint128_t x155 = (uint128_t) x59 * x59;
+ uint128_t x156 = 0x13 * x155;
  uint128_t x157 = x154 + x156;
- uint128_t x158 = (uint128_t) x67 * (uint128_t) x63;
- uint128_t x159 = (uint128_t) x65 * (uint128_t) x65;
- uint128_t x160 = (uint128_t) x63 * (uint128_t) x67;
+ uint128_t x158 = (uint128_t) x67 * x63;
+ uint128_t x159 = (uint128_t) x65 * x65;
+ uint128_t x160 = (uint128_t) x63 * x67;
  uint128_t x161 = x159 + x160;
  uint128_t x162 = x158 + x161;
- uint128_t x163 = (uint128_t) x61 * (uint128_t) x59;
- uint128_t x164 = (uint128_t) x59 * (uint128_t) x61;
+ uint128_t x163 = (uint128_t) x61 * x59;
+ uint128_t x164 = (uint128_t) x59 * x61;
  uint128_t x165 = x163 + x164;
- uint128_t x166 = (uint128_t) 0x13 * x165;
+ uint128_t x166 = 0x13 * x165;
  uint128_t x167 = x162 + x166;
- uint128_t x168 = (uint128_t) x67 * (uint128_t) x65;
- uint128_t x169 = (uint128_t) x65 * (uint128_t) x67;
+ uint128_t x168 = (uint128_t) x67 * x65;
+ uint128_t x169 = (uint128_t) x65 * x67;
  uint128_t x170 = x168 + x169;
- uint128_t x171 = (uint128_t) x63 * (uint128_t) x59;
- uint128_t x172 = (uint128_t) x61 * (uint128_t) x61;
- uint128_t x173 = (uint128_t) x59 * (uint128_t) x63;
+ uint128_t x171 = (uint128_t) x63 * x59;
+ uint128_t x172 = (uint128_t) x61 * x61;
+ uint128_t x173 = (uint128_t) x59 * x63;
  uint128_t x174 = x172 + x173;
  uint128_t x175 = x171 + x174;
- uint128_t x176 = (uint128_t) 0x13 * x175;
+ uint128_t x176 = 0x13 * x175;
  uint128_t x177 = x170 + x176;
- uint128_t x178 = (uint128_t) x67 * (uint128_t) x67;
- uint128_t x179 = (uint128_t) x65 * (uint128_t) x59;
- uint128_t x180 = (uint128_t) x63 * (uint128_t) x61;
- uint128_t x181 = (uint128_t) x61 * (uint128_t) x63;
- uint128_t x182 = (uint128_t) x59 * (uint128_t) x65;
+ uint128_t x178 = (uint128_t) x67 * x67;
+ uint128_t x179 = (uint128_t) x65 * x59;
+ uint128_t x180 = (uint128_t) x63 * x61;
+ uint128_t x181 = (uint128_t) x61 * x63;
+ uint128_t x182 = (uint128_t) x59 * x65;
  uint128_t x183 = x181 + x182;
  uint128_t x184 = x180 + x183;
  uint128_t x185 = x179 + x184;
- uint128_t x186 = (uint128_t) 0x13 * x185;
+ uint128_t x186 = 0x13 * x185;
  uint128_t x187 = x178 + x186;
  uint64_t x188 = (uint64_t) (x187 >> 0x33);
- uint128_t x189 = (uint128_t) x188 + x177;
+ uint128_t x189 = x188 + x177;
  uint64_t x190 = (uint64_t) (x189 >> 0x33);
- uint128_t x191 = (uint128_t) x190 + x167;
+ uint128_t x191 = x190 + x167;
  uint64_t x192 = (uint64_t) (x191 >> 0x33);
- uint128_t x193 = (uint128_t) x192 + x157;
+ uint128_t x193 = x192 + x157;
  uint64_t x194 = (uint64_t) (x193 >> 0x33);
- uint128_t x195 = (uint128_t) x194 + x147;
+ uint128_t x195 = x194 + x147;
  uint64_t x196 = (uint64_t) x187 & 0x7ffffffffffff;
  uint64_t x197 = (uint64_t) (x195 >> 0x33);
  uint64_t x198 = 0x13 * x197;
  uint64_t x199 = x196 + x198;
- uint64_t x200 = (uint64_t) (x199 >> 0x33);
+ uint64_t x200 = x199 >> 0x33;
  uint64_t x201 = (uint64_t) x189 & 0x7ffffffffffff;
  uint64_t x202 = x200 + x201;
  uint64_t x203 = (uint64_t) x195 & 0x7ffffffffffff;
  uint64_t x204 = (uint64_t) x193 & 0x7ffffffffffff;
- uint64_t x205 = (uint64_t) (x202 >> 0x33);
+ uint64_t x205 = x202 >> 0x33;
  uint64_t x206 = (uint64_t) x191 & 0x7ffffffffffff;
  uint64_t x207 = x205 + x206;
  uint64_t x208 = x202 & 0x7ffffffffffff;
  uint64_t x209 = x199 & 0x7ffffffffffff;
- uint128_t x210 = (uint128_t) x138 * (uint128_t) x203;
- uint128_t x211 = (uint128_t) x137 * (uint128_t) x204;
- uint128_t x212 = (uint128_t) x136 * (uint128_t) x207;
- uint128_t x213 = (uint128_t) x133 * (uint128_t) x208;
- uint128_t x214 = (uint128_t) x132 * (uint128_t) x209;
+ uint128_t x210 = (uint128_t) x138 * x203;
+ uint128_t x211 = (uint128_t) x137 * x204;
+ uint128_t x212 = (uint128_t) x136 * x207;
+ uint128_t x213 = (uint128_t) x133 * x208;
+ uint128_t x214 = (uint128_t) x132 * x209;
  uint128_t x215 = x213 + x214;
  uint128_t x216 = x212 + x215;
  uint128_t x217 = x211 + x216;
  uint128_t x218 = x210 + x217;
- uint128_t x219 = (uint128_t) x138 * (uint128_t) x204;
- uint128_t x220 = (uint128_t) x137 * (uint128_t) x207;
- uint128_t x221 = (uint128_t) x136 * (uint128_t) x208;
- uint128_t x222 = (uint128_t) x133 * (uint128_t) x209;
+ uint128_t x219 = (uint128_t) x138 * x204;
+ uint128_t x220 = (uint128_t) x137 * x207;
+ uint128_t x221 = (uint128_t) x136 * x208;
+ uint128_t x222 = (uint128_t) x133 * x209;
  uint128_t x223 = x221 + x222;
  uint128_t x224 = x220 + x223;
  uint128_t x225 = x219 + x224;
- uint128_t x226 = (uint128_t) x132 * (uint128_t) x203;
- uint128_t x227 = (uint128_t) 0x13 * x226;
+ uint128_t x226 = (uint128_t) x132 * x203;
+ uint128_t x227 = 0x13 * x226;
  uint128_t x228 = x225 + x227;
- uint128_t x229 = (uint128_t) x138 * (uint128_t) x207;
- uint128_t x230 = (uint128_t) x137 * (uint128_t) x208;
- uint128_t x231 = (uint128_t) x136 * (uint128_t) x209;
+ uint128_t x229 = (uint128_t) x138 * x207;
+ uint128_t x230 = (uint128_t) x137 * x208;
+ uint128_t x231 = (uint128_t) x136 * x209;
  uint128_t x232 = x230 + x231;
  uint128_t x233 = x229 + x232;
- uint128_t x234 = (uint128_t) x133 * (uint128_t) x203;
- uint128_t x235 = (uint128_t) x132 * (uint128_t) x204;
+ uint128_t x234 = (uint128_t) x133 * x203;
+ uint128_t x235 = (uint128_t) x132 * x204;
  uint128_t x236 = x234 + x235;
- uint128_t x237 = (uint128_t) 0x13 * x236;
+ uint128_t x237 = 0x13 * x236;
  uint128_t x238 = x233 + x237;
- uint128_t x239 = (uint128_t) x138 * (uint128_t) x208;
- uint128_t x240 = (uint128_t) x137 * (uint128_t) x209;
+ uint128_t x239 = (uint128_t) x138 * x208;
+ uint128_t x240 = (uint128_t) x137 * x209;
  uint128_t x241 = x239 + x240;
- uint128_t x242 = (uint128_t) x136 * (uint128_t) x203;
- uint128_t x243 = (uint128_t) x133 * (uint128_t) x204;
- uint128_t x244 = (uint128_t) x132 * (uint128_t) x207;
+ uint128_t x242 = (uint128_t) x136 * x203;
+ uint128_t x243 = (uint128_t) x133 * x204;
+ uint128_t x244 = (uint128_t) x132 * x207;
  uint128_t x245 = x243 + x244;
  uint128_t x246 = x242 + x245;
- uint128_t x247 = (uint128_t) 0x13 * x246;
+ uint128_t x247 = 0x13 * x246;
  uint128_t x248 = x241 + x247;
- uint128_t x249 = (uint128_t) x138 * (uint128_t) x209;
- uint128_t x250 = (uint128_t) x137 * (uint128_t) x203;
- uint128_t x251 = (uint128_t) x136 * (uint128_t) x204;
- uint128_t x252 = (uint128_t) x133 * (uint128_t) x207;
- uint128_t x253 = (uint128_t) x132 * (uint128_t) x208;
+ uint128_t x249 = (uint128_t) x138 * x209;
+ uint128_t x250 = (uint128_t) x137 * x203;
+ uint128_t x251 = (uint128_t) x136 * x204;
+ uint128_t x252 = (uint128_t) x133 * x207;
+ uint128_t x253 = (uint128_t) x132 * x208;
  uint128_t x254 = x252 + x253;
  uint128_t x255 = x251 + x254;
  uint128_t x256 = x250 + x255;
- uint128_t x257 = (uint128_t) 0x13 * x256;
+ uint128_t x257 = 0x13 * x256;
  uint128_t x258 = x249 + x257;
  uint64_t x259 = (uint64_t) (x258 >> 0x33);
- uint128_t x260 = (uint128_t) x259 + x248;
+ uint128_t x260 = x259 + x248;
  uint64_t x261 = (uint64_t) (x260 >> 0x33);
- uint128_t x262 = (uint128_t) x261 + x238;
+ uint128_t x262 = x261 + x238;
  uint64_t x263 = (uint64_t) (x262 >> 0x33);
- uint128_t x264 = (uint128_t) x263 + x228;
+ uint128_t x264 = x263 + x228;
  uint64_t x265 = (uint64_t) (x264 >> 0x33);
- uint128_t x266 = (uint128_t) x265 + x218;
+ uint128_t x266 = x265 + x218;
  uint64_t x267 = (uint64_t) x258 & 0x7ffffffffffff;
  uint64_t x268 = (uint64_t) (x266 >> 0x33);
  uint64_t x269 = 0x13 * x268;
  uint64_t x270 = x267 + x269;
- uint64_t x271 = (uint64_t) (x270 >> 0x33);
+ uint64_t x271 = x270 >> 0x33;
  uint64_t x272 = (uint64_t) x260 & 0x7ffffffffffff;
  uint64_t x273 = x271 + x272;
  uint64_t x274 = (uint64_t) x266 & 0x7ffffffffffff;
  uint64_t x275 = (uint64_t) x264 & 0x7ffffffffffff;
- uint64_t x276 = (uint64_t) (x273 >> 0x33);
+ uint64_t x276 = x273 >> 0x33;
  uint64_t x277 = (uint64_t) x262 & 0x7ffffffffffff;
  uint64_t x278 = x276 + x277;
  uint64_t x279 = x273 & 0x7ffffffffffff;
@@ -240,29 +240,29 @@ let (a, b) := Interp-η
  uint64_t x288 = x287 - x208;
  uint64_t x289 = 0xfffffffffffda + x138;
  uint64_t x290 = x289 - x209;
- uint128_t x291 = (uint128_t) Const 121665 * (uint128_t) x282;
- uint128_t x292 = (uint128_t) Const 121665 * (uint128_t) x284;
- uint128_t x293 = (uint128_t) Const 121665 * (uint128_t) x286;
- uint128_t x294 = (uint128_t) Const 121665 * (uint128_t) x288;
- uint128_t x295 = (uint128_t) Const 121665 * (uint128_t) x290;
+ uint128_t x291 = (uint128_t) 0x1db41 * x282;
+ uint128_t x292 = (uint128_t) 0x1db41 * x284;
+ uint128_t x293 = (uint128_t) 0x1db41 * x286;
+ uint128_t x294 = (uint128_t) 0x1db41 * x288;
+ uint128_t x295 = (uint128_t) 0x1db41 * x290;
  uint64_t x296 = (uint64_t) (x295 >> 0x33);
- uint128_t x297 = (uint128_t) x296 + x294;
+ uint128_t x297 = x296 + x294;
  uint64_t x298 = (uint64_t) (x297 >> 0x33);
- uint128_t x299 = (uint128_t) x298 + x293;
+ uint128_t x299 = x298 + x293;
  uint64_t x300 = (uint64_t) (x299 >> 0x33);
- uint128_t x301 = (uint128_t) x300 + x292;
+ uint128_t x301 = x300 + x292;
  uint64_t x302 = (uint64_t) (x301 >> 0x33);
- uint128_t x303 = (uint128_t) x302 + x291;
+ uint128_t x303 = x302 + x291;
  uint64_t x304 = (uint64_t) x295 & 0x7ffffffffffff;
  uint64_t x305 = (uint64_t) (x303 >> 0x33);
  uint64_t x306 = 0x13 * x305;
  uint64_t x307 = x304 + x306;
- uint64_t x308 = (uint64_t) (x307 >> 0x33);
+ uint64_t x308 = x307 >> 0x33;
  uint64_t x309 = (uint64_t) x297 & 0x7ffffffffffff;
  uint64_t x310 = x308 + x309;
  uint64_t x311 = (uint64_t) x303 & 0x7ffffffffffff;
  uint64_t x312 = (uint64_t) x301 & 0x7ffffffffffff;
- uint64_t x313 = (uint64_t) (x310 >> 0x33);
+ uint64_t x313 = x310 >> 0x33;
  uint64_t x314 = (uint64_t) x299 & 0x7ffffffffffff;
  uint64_t x315 = x313 + x314;
  uint64_t x316 = x310 & 0x7ffffffffffff;
@@ -272,73 +272,73 @@ let (a, b) := Interp-η
  uint64_t x320 = x136 + x315;
  uint64_t x321 = x137 + x316;
  uint64_t x322 = x138 + x317;
- uint128_t x323 = (uint128_t) x290 * (uint128_t) x318;
- uint128_t x324 = (uint128_t) x288 * (uint128_t) x319;
- uint128_t x325 = (uint128_t) x286 * (uint128_t) x320;
- uint128_t x326 = (uint128_t) x284 * (uint128_t) x321;
- uint128_t x327 = (uint128_t) x282 * (uint128_t) x322;
+ uint128_t x323 = (uint128_t) x290 * x318;
+ uint128_t x324 = (uint128_t) x288 * x319;
+ uint128_t x325 = (uint128_t) x286 * x320;
+ uint128_t x326 = (uint128_t) x284 * x321;
+ uint128_t x327 = (uint128_t) x282 * x322;
  uint128_t x328 = x326 + x327;
  uint128_t x329 = x325 + x328;
  uint128_t x330 = x324 + x329;
  uint128_t x331 = x323 + x330;
- uint128_t x332 = (uint128_t) x290 * (uint128_t) x319;
- uint128_t x333 = (uint128_t) x288 * (uint128_t) x320;
- uint128_t x334 = (uint128_t) x286 * (uint128_t) x321;
- uint128_t x335 = (uint128_t) x284 * (uint128_t) x322;
+ uint128_t x332 = (uint128_t) x290 * x319;
+ uint128_t x333 = (uint128_t) x288 * x320;
+ uint128_t x334 = (uint128_t) x286 * x321;
+ uint128_t x335 = (uint128_t) x284 * x322;
  uint128_t x336 = x334 + x335;
  uint128_t x337 = x333 + x336;
  uint128_t x338 = x332 + x337;
- uint128_t x339 = (uint128_t) x282 * (uint128_t) x318;
- uint128_t x340 = (uint128_t) 0x13 * x339;
+ uint128_t x339 = (uint128_t) x282 * x318;
+ uint128_t x340 = 0x13 * x339;
  uint128_t x341 = x338 + x340;
- uint128_t x342 = (uint128_t) x290 * (uint128_t) x320;
- uint128_t x343 = (uint128_t) x288 * (uint128_t) x321;
- uint128_t x344 = (uint128_t) x286 * (uint128_t) x322;
+ uint128_t x342 = (uint128_t) x290 * x320;
+ uint128_t x343 = (uint128_t) x288 * x321;
+ uint128_t x344 = (uint128_t) x286 * x322;
  uint128_t x345 = x343 + x344;
  uint128_t x346 = x342 + x345;
- uint128_t x347 = (uint128_t) x284 * (uint128_t) x318;
- uint128_t x348 = (uint128_t) x282 * (uint128_t) x319;
+ uint128_t x347 = (uint128_t) x284 * x318;
+ uint128_t x348 = (uint128_t) x282 * x319;
  uint128_t x349 = x347 + x348;
- uint128_t x350 = (uint128_t) 0x13 * x349;
+ uint128_t x350 = 0x13 * x349;
  uint128_t x351 = x346 + x350;
- uint128_t x352 = (uint128_t) x290 * (uint128_t) x321;
- uint128_t x353 = (uint128_t) x288 * (uint128_t) x322;
+ uint128_t x352 = (uint128_t) x290 * x321;
+ uint128_t x353 = (uint128_t) x288 * x322;
  uint128_t x354 = x352 + x353;
- uint128_t x355 = (uint128_t) x286 * (uint128_t) x318;
- uint128_t x356 = (uint128_t) x284 * (uint128_t) x319;
- uint128_t x357 = (uint128_t) x282 * (uint128_t) x320;
+ uint128_t x355 = (uint128_t) x286 * x318;
+ uint128_t x356 = (uint128_t) x284 * x319;
+ uint128_t x357 = (uint128_t) x282 * x320;
  uint128_t x358 = x356 + x357;
  uint128_t x359 = x355 + x358;
- uint128_t x360 = (uint128_t) 0x13 * x359;
+ uint128_t x360 = 0x13 * x359;
  uint128_t x361 = x354 + x360;
- uint128_t x362 = (uint128_t) x290 * (uint128_t) x322;
- uint128_t x363 = (uint128_t) x288 * (uint128_t) x318;
- uint128_t x364 = (uint128_t) x286 * (uint128_t) x319;
- uint128_t x365 = (uint128_t) x284 * (uint128_t) x320;
- uint128_t x366 = (uint128_t) x282 * (uint128_t) x321;
+ uint128_t x362 = (uint128_t) x290 * x322;
+ uint128_t x363 = (uint128_t) x288 * x318;
+ uint128_t x364 = (uint128_t) x286 * x319;
+ uint128_t x365 = (uint128_t) x284 * x320;
+ uint128_t x366 = (uint128_t) x282 * x321;
  uint128_t x367 = x365 + x366;
  uint128_t x368 = x364 + x367;
  uint128_t x369 = x363 + x368;
- uint128_t x370 = (uint128_t) 0x13 * x369;
+ uint128_t x370 = 0x13 * x369;
  uint128_t x371 = x362 + x370;
  uint64_t x372 = (uint64_t) (x371 >> 0x33);
- uint128_t x373 = (uint128_t) x372 + x361;
+ uint128_t x373 = x372 + x361;
  uint64_t x374 = (uint64_t) (x373 >> 0x33);
- uint128_t x375 = (uint128_t) x374 + x351;
+ uint128_t x375 = x374 + x351;
  uint64_t x376 = (uint64_t) (x375 >> 0x33);
- uint128_t x377 = (uint128_t) x376 + x341;
+ uint128_t x377 = x376 + x341;
  uint64_t x378 = (uint64_t) (x377 >> 0x33);
- uint128_t x379 = (uint128_t) x378 + x331;
+ uint128_t x379 = x378 + x331;
  uint64_t x380 = (uint64_t) x371 & 0x7ffffffffffff;
  uint64_t x381 = (uint64_t) (x379 >> 0x33);
  uint64_t x382 = 0x13 * x381;
  uint64_t x383 = x380 + x382;
- uint64_t x384 = (uint64_t) (x383 >> 0x33);
+ uint64_t x384 = x383 >> 0x33;
  uint64_t x385 = (uint64_t) x373 & 0x7ffffffffffff;
  uint64_t x386 = x384 + x385;
  uint64_t x387 = (uint64_t) x379 & 0x7ffffffffffff;
  uint64_t x388 = (uint64_t) x377 & 0x7ffffffffffff;
- uint64_t x389 = (uint64_t) (x386 >> 0x33);
+ uint64_t x389 = x386 >> 0x33;
  uint64_t x390 = (uint64_t) x375 & 0x7ffffffffffff;
  uint64_t x391 = x389 + x390;
  uint64_t x392 = x386 & 0x7ffffffffffff;
@@ -358,144 +358,144 @@ let (a, b) := Interp-η
  uint64_t x406 = x405 - x48;
  uint64_t x407 = 0xfffffffffffda + x38;
  uint64_t x408 = x407 - x46;
- uint128_t x409 = (uint128_t) x398 * (uint128_t) x59;
- uint128_t x410 = (uint128_t) x397 * (uint128_t) x61;
- uint128_t x411 = (uint128_t) x396 * (uint128_t) x63;
- uint128_t x412 = (uint128_t) x395 * (uint128_t) x65;
- uint128_t x413 = (uint128_t) x394 * (uint128_t) x67;
+ uint128_t x409 = (uint128_t) x398 * x59;
+ uint128_t x410 = (uint128_t) x397 * x61;
+ uint128_t x411 = (uint128_t) x396 * x63;
+ uint128_t x412 = (uint128_t) x395 * x65;
+ uint128_t x413 = (uint128_t) x394 * x67;
  uint128_t x414 = x412 + x413;
  uint128_t x415 = x411 + x414;
  uint128_t x416 = x410 + x415;
  uint128_t x417 = x409 + x416;
- uint128_t x418 = (uint128_t) x398 * (uint128_t) x61;
- uint128_t x419 = (uint128_t) x397 * (uint128_t) x63;
- uint128_t x420 = (uint128_t) x396 * (uint128_t) x65;
- uint128_t x421 = (uint128_t) x395 * (uint128_t) x67;
+ uint128_t x418 = (uint128_t) x398 * x61;
+ uint128_t x419 = (uint128_t) x397 * x63;
+ uint128_t x420 = (uint128_t) x396 * x65;
+ uint128_t x421 = (uint128_t) x395 * x67;
  uint128_t x422 = x420 + x421;
  uint128_t x423 = x419 + x422;
  uint128_t x424 = x418 + x423;
- uint128_t x425 = (uint128_t) x394 * (uint128_t) x59;
- uint128_t x426 = (uint128_t) 0x13 * x425;
+ uint128_t x425 = (uint128_t) x394 * x59;
+ uint128_t x426 = 0x13 * x425;
  uint128_t x427 = x424 + x426;
- uint128_t x428 = (uint128_t) x398 * (uint128_t) x63;
- uint128_t x429 = (uint128_t) x397 * (uint128_t) x65;
- uint128_t x430 = (uint128_t) x396 * (uint128_t) x67;
+ uint128_t x428 = (uint128_t) x398 * x63;
+ uint128_t x429 = (uint128_t) x397 * x65;
+ uint128_t x430 = (uint128_t) x396 * x67;
  uint128_t x431 = x429 + x430;
  uint128_t x432 = x428 + x431;
- uint128_t x433 = (uint128_t) x395 * (uint128_t) x59;
- uint128_t x434 = (uint128_t) x394 * (uint128_t) x61;
+ uint128_t x433 = (uint128_t) x395 * x59;
+ uint128_t x434 = (uint128_t) x394 * x61;
  uint128_t x435 = x433 + x434;
- uint128_t x436 = (uint128_t) 0x13 * x435;
+ uint128_t x436 = 0x13 * x435;
  uint128_t x437 = x432 + x436;
- uint128_t x438 = (uint128_t) x398 * (uint128_t) x65;
- uint128_t x439 = (uint128_t) x397 * (uint128_t) x67;
+ uint128_t x438 = (uint128_t) x398 * x65;
+ uint128_t x439 = (uint128_t) x397 * x67;
  uint128_t x440 = x438 + x439;
- uint128_t x441 = (uint128_t) x396 * (uint128_t) x59;
- uint128_t x442 = (uint128_t) x395 * (uint128_t) x61;
- uint128_t x443 = (uint128_t) x394 * (uint128_t) x63;
+ uint128_t x441 = (uint128_t) x396 * x59;
+ uint128_t x442 = (uint128_t) x395 * x61;
+ uint128_t x443 = (uint128_t) x394 * x63;
  uint128_t x444 = x442 + x443;
  uint128_t x445 = x441 + x444;
- uint128_t x446 = (uint128_t) 0x13 * x445;
+ uint128_t x446 = 0x13 * x445;
  uint128_t x447 = x440 + x446;
- uint128_t x448 = (uint128_t) x398 * (uint128_t) x67;
- uint128_t x449 = (uint128_t) x397 * (uint128_t) x59;
- uint128_t x450 = (uint128_t) x396 * (uint128_t) x61;
- uint128_t x451 = (uint128_t) x395 * (uint128_t) x63;
- uint128_t x452 = (uint128_t) x394 * (uint128_t) x65;
+ uint128_t x448 = (uint128_t) x398 * x67;
+ uint128_t x449 = (uint128_t) x397 * x59;
+ uint128_t x450 = (uint128_t) x396 * x61;
+ uint128_t x451 = (uint128_t) x395 * x63;
+ uint128_t x452 = (uint128_t) x394 * x65;
  uint128_t x453 = x451 + x452;
  uint128_t x454 = x450 + x453;
  uint128_t x455 = x449 + x454;
- uint128_t x456 = (uint128_t) 0x13 * x455;
+ uint128_t x456 = 0x13 * x455;
  uint128_t x457 = x448 + x456;
  uint64_t x458 = (uint64_t) (x457 >> 0x33);
- uint128_t x459 = (uint128_t) x458 + x447;
+ uint128_t x459 = x458 + x447;
  uint64_t x460 = (uint64_t) (x459 >> 0x33);
- uint128_t x461 = (uint128_t) x460 + x437;
+ uint128_t x461 = x460 + x437;
  uint64_t x462 = (uint64_t) (x461 >> 0x33);
- uint128_t x463 = (uint128_t) x462 + x427;
+ uint128_t x463 = x462 + x427;
  uint64_t x464 = (uint64_t) (x463 >> 0x33);
- uint128_t x465 = (uint128_t) x464 + x417;
+ uint128_t x465 = x464 + x417;
  uint64_t x466 = (uint64_t) x457 & 0x7ffffffffffff;
  uint64_t x467 = (uint64_t) (x465 >> 0x33);
  uint64_t x468 = 0x13 * x467;
  uint64_t x469 = x466 + x468;
- uint64_t x470 = (uint64_t) (x469 >> 0x33);
+ uint64_t x470 = x469 >> 0x33;
  uint64_t x471 = (uint64_t) x459 & 0x7ffffffffffff;
  uint64_t x472 = x470 + x471;
  uint64_t x473 = (uint64_t) x465 & 0x7ffffffffffff;
  uint64_t x474 = (uint64_t) x463 & 0x7ffffffffffff;
- uint64_t x475 = (uint64_t) (x472 >> 0x33);
+ uint64_t x475 = x472 >> 0x33;
  uint64_t x476 = (uint64_t) x461 & 0x7ffffffffffff;
  uint64_t x477 = x475 + x476;
  uint64_t x478 = x472 & 0x7ffffffffffff;
  uint64_t x479 = x469 & 0x7ffffffffffff;
- uint128_t x480 = (uint128_t) x408 * (uint128_t) x53;
- uint128_t x481 = (uint128_t) x406 * (uint128_t) x54;
- uint128_t x482 = (uint128_t) x404 * (uint128_t) x55;
- uint128_t x483 = (uint128_t) x402 * (uint128_t) x56;
- uint128_t x484 = (uint128_t) x400 * (uint128_t) x57;
+ uint128_t x480 = (uint128_t) x408 * x53;
+ uint128_t x481 = (uint128_t) x406 * x54;
+ uint128_t x482 = (uint128_t) x404 * x55;
+ uint128_t x483 = (uint128_t) x402 * x56;
+ uint128_t x484 = (uint128_t) x400 * x57;
  uint128_t x485 = x483 + x484;
  uint128_t x486 = x482 + x485;
  uint128_t x487 = x481 + x486;
  uint128_t x488 = x480 + x487;
- uint128_t x489 = (uint128_t) x408 * (uint128_t) x54;
- uint128_t x490 = (uint128_t) x406 * (uint128_t) x55;
- uint128_t x491 = (uint128_t) x404 * (uint128_t) x56;
- uint128_t x492 = (uint128_t) x402 * (uint128_t) x57;
+ uint128_t x489 = (uint128_t) x408 * x54;
+ uint128_t x490 = (uint128_t) x406 * x55;
+ uint128_t x491 = (uint128_t) x404 * x56;
+ uint128_t x492 = (uint128_t) x402 * x57;
  uint128_t x493 = x491 + x492;
  uint128_t x494 = x490 + x493;
  uint128_t x495 = x489 + x494;
- uint128_t x496 = (uint128_t) x400 * (uint128_t) x53;
- uint128_t x497 = (uint128_t) 0x13 * x496;
+ uint128_t x496 = (uint128_t) x400 * x53;
+ uint128_t x497 = 0x13 * x496;
  uint128_t x498 = x495 + x497;
- uint128_t x499 = (uint128_t) x408 * (uint128_t) x55;
- uint128_t x500 = (uint128_t) x406 * (uint128_t) x56;
- uint128_t x501 = (uint128_t) x404 * (uint128_t) x57;
+ uint128_t x499 = (uint128_t) x408 * x55;
+ uint128_t x500 = (uint128_t) x406 * x56;
+ uint128_t x501 = (uint128_t) x404 * x57;
  uint128_t x502 = x500 + x501;
  uint128_t x503 = x499 + x502;
- uint128_t x504 = (uint128_t) x402 * (uint128_t) x53;
- uint128_t x505 = (uint128_t) x400 * (uint128_t) x54;
+ uint128_t x504 = (uint128_t) x402 * x53;
+ uint128_t x505 = (uint128_t) x400 * x54;
  uint128_t x506 = x504 + x505;
- uint128_t x507 = (uint128_t) 0x13 * x506;
+ uint128_t x507 = 0x13 * x506;
  uint128_t x508 = x503 + x507;
- uint128_t x509 = (uint128_t) x408 * (uint128_t) x56;
- uint128_t x510 = (uint128_t) x406 * (uint128_t) x57;
+ uint128_t x509 = (uint128_t) x408 * x56;
+ uint128_t x510 = (uint128_t) x406 * x57;
  uint128_t x511 = x509 + x510;
- uint128_t x512 = (uint128_t) x404 * (uint128_t) x53;
- uint128_t x513 = (uint128_t) x402 * (uint128_t) x54;
- uint128_t x514 = (uint128_t) x400 * (uint128_t) x55;
+ uint128_t x512 = (uint128_t) x404 * x53;
+ uint128_t x513 = (uint128_t) x402 * x54;
+ uint128_t x514 = (uint128_t) x400 * x55;
  uint128_t x515 = x513 + x514;
  uint128_t x516 = x512 + x515;
- uint128_t x517 = (uint128_t) 0x13 * x516;
+ uint128_t x517 = 0x13 * x516;
  uint128_t x518 = x511 + x517;
- uint128_t x519 = (uint128_t) x408 * (uint128_t) x57;
- uint128_t x520 = (uint128_t) x406 * (uint128_t) x53;
- uint128_t x521 = (uint128_t) x404 * (uint128_t) x54;
- uint128_t x522 = (uint128_t) x402 * (uint128_t) x55;
- uint128_t x523 = (uint128_t) x400 * (uint128_t) x56;
+ uint128_t x519 = (uint128_t) x408 * x57;
+ uint128_t x520 = (uint128_t) x406 * x53;
+ uint128_t x521 = (uint128_t) x404 * x54;
+ uint128_t x522 = (uint128_t) x402 * x55;
+ uint128_t x523 = (uint128_t) x400 * x56;
  uint128_t x524 = x522 + x523;
  uint128_t x525 = x521 + x524;
  uint128_t x526 = x520 + x525;
- uint128_t x527 = (uint128_t) 0x13 * x526;
+ uint128_t x527 = 0x13 * x526;
  uint128_t x528 = x519 + x527;
  uint64_t x529 = (uint64_t) (x528 >> 0x33);
- uint128_t x530 = (uint128_t) x529 + x518;
+ uint128_t x530 = x529 + x518;
  uint64_t x531 = (uint64_t) (x530 >> 0x33);
- uint128_t x532 = (uint128_t) x531 + x508;
+ uint128_t x532 = x531 + x508;
  uint64_t x533 = (uint64_t) (x532 >> 0x33);
- uint128_t x534 = (uint128_t) x533 + x498;
+ uint128_t x534 = x533 + x498;
  uint64_t x535 = (uint64_t) (x534 >> 0x33);
- uint128_t x536 = (uint128_t) x535 + x488;
+ uint128_t x536 = x535 + x488;
  uint64_t x537 = (uint64_t) x528 & 0x7ffffffffffff;
  uint64_t x538 = (uint64_t) (x536 >> 0x33);
  uint64_t x539 = 0x13 * x538;
  uint64_t x540 = x537 + x539;
- uint64_t x541 = (uint64_t) (x540 >> 0x33);
+ uint64_t x541 = x540 >> 0x33;
  uint64_t x542 = (uint64_t) x530 & 0x7ffffffffffff;
  uint64_t x543 = x541 + x542;
  uint64_t x544 = (uint64_t) x536 & 0x7ffffffffffff;
  uint64_t x545 = (uint64_t) x534 & 0x7ffffffffffff;
- uint64_t x546 = (uint64_t) (x543 >> 0x33);
+ uint64_t x546 = x543 >> 0x33;
  uint64_t x547 = (uint64_t) x532 & 0x7ffffffffffff;
  uint64_t x548 = x546 + x547;
  uint64_t x549 = x543 & 0x7ffffffffffff;
@@ -510,73 +510,73 @@ let (a, b) := Interp-η
  uint64_t x558 = x548 + x477;
  uint64_t x559 = x549 + x478;
  uint64_t x560 = x550 + x479;
- uint128_t x561 = (uint128_t) x555 * (uint128_t) x556;
- uint128_t x562 = (uint128_t) x554 * (uint128_t) x557;
- uint128_t x563 = (uint128_t) x553 * (uint128_t) x558;
- uint128_t x564 = (uint128_t) x552 * (uint128_t) x559;
- uint128_t x565 = (uint128_t) x551 * (uint128_t) x560;
+ uint128_t x561 = (uint128_t) x555 * x556;
+ uint128_t x562 = (uint128_t) x554 * x557;
+ uint128_t x563 = (uint128_t) x553 * x558;
+ uint128_t x564 = (uint128_t) x552 * x559;
+ uint128_t x565 = (uint128_t) x551 * x560;
  uint128_t x566 = x564 + x565;
  uint128_t x567 = x563 + x566;
  uint128_t x568 = x562 + x567;
  uint128_t x569 = x561 + x568;
- uint128_t x570 = (uint128_t) x555 * (uint128_t) x557;
- uint128_t x571 = (uint128_t) x554 * (uint128_t) x558;
- uint128_t x572 = (uint128_t) x553 * (uint128_t) x559;
- uint128_t x573 = (uint128_t) x552 * (uint128_t) x560;
+ uint128_t x570 = (uint128_t) x555 * x557;
+ uint128_t x571 = (uint128_t) x554 * x558;
+ uint128_t x572 = (uint128_t) x553 * x559;
+ uint128_t x573 = (uint128_t) x552 * x560;
  uint128_t x574 = x572 + x573;
  uint128_t x575 = x571 + x574;
  uint128_t x576 = x570 + x575;
- uint128_t x577 = (uint128_t) x551 * (uint128_t) x556;
- uint128_t x578 = (uint128_t) 0x13 * x577;
+ uint128_t x577 = (uint128_t) x551 * x556;
+ uint128_t x578 = 0x13 * x577;
  uint128_t x579 = x576 + x578;
- uint128_t x580 = (uint128_t) x555 * (uint128_t) x558;
- uint128_t x581 = (uint128_t) x554 * (uint128_t) x559;
- uint128_t x582 = (uint128_t) x553 * (uint128_t) x560;
+ uint128_t x580 = (uint128_t) x555 * x558;
+ uint128_t x581 = (uint128_t) x554 * x559;
+ uint128_t x582 = (uint128_t) x553 * x560;
  uint128_t x583 = x581 + x582;
  uint128_t x584 = x580 + x583;
- uint128_t x585 = (uint128_t) x552 * (uint128_t) x556;
- uint128_t x586 = (uint128_t) x551 * (uint128_t) x557;
+ uint128_t x585 = (uint128_t) x552 * x556;
+ uint128_t x586 = (uint128_t) x551 * x557;
  uint128_t x587 = x585 + x586;
- uint128_t x588 = (uint128_t) 0x13 * x587;
+ uint128_t x588 = 0x13 * x587;
  uint128_t x589 = x584 + x588;
- uint128_t x590 = (uint128_t) x555 * (uint128_t) x559;
- uint128_t x591 = (uint128_t) x554 * (uint128_t) x560;
+ uint128_t x590 = (uint128_t) x555 * x559;
+ uint128_t x591 = (uint128_t) x554 * x560;
  uint128_t x592 = x590 + x591;
- uint128_t x593 = (uint128_t) x553 * (uint128_t) x556;
- uint128_t x594 = (uint128_t) x552 * (uint128_t) x557;
- uint128_t x595 = (uint128_t) x551 * (uint128_t) x558;
+ uint128_t x593 = (uint128_t) x553 * x556;
+ uint128_t x594 = (uint128_t) x552 * x557;
+ uint128_t x595 = (uint128_t) x551 * x558;
  uint128_t x596 = x594 + x595;
  uint128_t x597 = x593 + x596;
- uint128_t x598 = (uint128_t) 0x13 * x597;
+ uint128_t x598 = 0x13 * x597;
  uint128_t x599 = x592 + x598;
- uint128_t x600 = (uint128_t) x555 * (uint128_t) x560;
- uint128_t x601 = (uint128_t) x554 * (uint128_t) x556;
- uint128_t x602 = (uint128_t) x553 * (uint128_t) x557;
- uint128_t x603 = (uint128_t) x552 * (uint128_t) x558;
- uint128_t x604 = (uint128_t) x551 * (uint128_t) x559;
+ uint128_t x600 = (uint128_t) x555 * x560;
+ uint128_t x601 = (uint128_t) x554 * x556;
+ uint128_t x602 = (uint128_t) x553 * x557;
+ uint128_t x603 = (uint128_t) x552 * x558;
+ uint128_t x604 = (uint128_t) x551 * x559;
  uint128_t x605 = x603 + x604;
  uint128_t x606 = x602 + x605;
  uint128_t x607 = x601 + x606;
- uint128_t x608 = (uint128_t) 0x13 * x607;
+ uint128_t x608 = 0x13 * x607;
  uint128_t x609 = x600 + x608;
  uint64_t x610 = (uint64_t) (x609 >> 0x33);
- uint128_t x611 = (uint128_t) x610 + x599;
+ uint128_t x611 = x610 + x599;
  uint64_t x612 = (uint64_t) (x611 >> 0x33);
- uint128_t x613 = (uint128_t) x612 + x589;
+ uint128_t x613 = x612 + x589;
  uint64_t x614 = (uint64_t) (x613 >> 0x33);
- uint128_t x615 = (uint128_t) x614 + x579;
+ uint128_t x615 = x614 + x579;
  uint64_t x616 = (uint64_t) (x615 >> 0x33);
- uint128_t x617 = (uint128_t) x616 + x569;
+ uint128_t x617 = x616 + x569;
  uint64_t x618 = (uint64_t) x609 & 0x7ffffffffffff;
  uint64_t x619 = (uint64_t) (x617 >> 0x33);
  uint64_t x620 = 0x13 * x619;
  uint64_t x621 = x618 + x620;
- uint64_t x622 = (uint64_t) (x621 >> 0x33);
+ uint64_t x622 = x621 >> 0x33;
  uint64_t x623 = (uint64_t) x611 & 0x7ffffffffffff;
  uint64_t x624 = x622 + x623;
  uint64_t x625 = (uint64_t) x617 & 0x7ffffffffffff;
  uint64_t x626 = (uint64_t) x615 & 0x7ffffffffffff;
- uint64_t x627 = (uint64_t) (x624 >> 0x33);
+ uint64_t x627 = x624 >> 0x33;
  uint64_t x628 = (uint64_t) x613 & 0x7ffffffffffff;
  uint64_t x629 = x627 + x628;
  uint64_t x630 = x624 & 0x7ffffffffffff;
@@ -601,144 +601,144 @@ let (a, b) := Interp-η
  uint64_t x649 = x648 - x478;
  uint64_t x650 = 0xfffffffffffda + x550;
  uint64_t x651 = x650 - x479;
- uint128_t x652 = (uint128_t) x641 * (uint128_t) x643;
- uint128_t x653 = (uint128_t) x639 * (uint128_t) x645;
- uint128_t x654 = (uint128_t) x637 * (uint128_t) x647;
- uint128_t x655 = (uint128_t) x635 * (uint128_t) x649;
- uint128_t x656 = (uint128_t) x633 * (uint128_t) x651;
+ uint128_t x652 = (uint128_t) x641 * x643;
+ uint128_t x653 = (uint128_t) x639 * x645;
+ uint128_t x654 = (uint128_t) x637 * x647;
+ uint128_t x655 = (uint128_t) x635 * x649;
+ uint128_t x656 = (uint128_t) x633 * x651;
  uint128_t x657 = x655 + x656;
  uint128_t x658 = x654 + x657;
  uint128_t x659 = x653 + x658;
  uint128_t x660 = x652 + x659;
- uint128_t x661 = (uint128_t) x641 * (uint128_t) x645;
- uint128_t x662 = (uint128_t) x639 * (uint128_t) x647;
- uint128_t x663 = (uint128_t) x637 * (uint128_t) x649;
- uint128_t x664 = (uint128_t) x635 * (uint128_t) x651;
+ uint128_t x661 = (uint128_t) x641 * x645;
+ uint128_t x662 = (uint128_t) x639 * x647;
+ uint128_t x663 = (uint128_t) x637 * x649;
+ uint128_t x664 = (uint128_t) x635 * x651;
  uint128_t x665 = x663 + x664;
  uint128_t x666 = x662 + x665;
  uint128_t x667 = x661 + x666;
- uint128_t x668 = (uint128_t) x633 * (uint128_t) x643;
- uint128_t x669 = (uint128_t) 0x13 * x668;
+ uint128_t x668 = (uint128_t) x633 * x643;
+ uint128_t x669 = 0x13 * x668;
  uint128_t x670 = x667 + x669;
- uint128_t x671 = (uint128_t) x641 * (uint128_t) x647;
- uint128_t x672 = (uint128_t) x639 * (uint128_t) x649;
- uint128_t x673 = (uint128_t) x637 * (uint128_t) x651;
+ uint128_t x671 = (uint128_t) x641 * x647;
+ uint128_t x672 = (uint128_t) x639 * x649;
+ uint128_t x673 = (uint128_t) x637 * x651;
  uint128_t x674 = x672 + x673;
  uint128_t x675 = x671 + x674;
- uint128_t x676 = (uint128_t) x635 * (uint128_t) x643;
- uint128_t x677 = (uint128_t) x633 * (uint128_t) x645;
+ uint128_t x676 = (uint128_t) x635 * x643;
+ uint128_t x677 = (uint128_t) x633 * x645;
  uint128_t x678 = x676 + x677;
- uint128_t x679 = (uint128_t) 0x13 * x678;
+ uint128_t x679 = 0x13 * x678;
  uint128_t x680 = x675 + x679;
- uint128_t x681 = (uint128_t) x641 * (uint128_t) x649;
- uint128_t x682 = (uint128_t) x639 * (uint128_t) x651;
+ uint128_t x681 = (uint128_t) x641 * x649;
+ uint128_t x682 = (uint128_t) x639 * x651;
  uint128_t x683 = x681 + x682;
- uint128_t x684 = (uint128_t) x637 * (uint128_t) x643;
- uint128_t x685 = (uint128_t) x635 * (uint128_t) x645;
- uint128_t x686 = (uint128_t) x633 * (uint128_t) x647;
+ uint128_t x684 = (uint128_t) x637 * x643;
+ uint128_t x685 = (uint128_t) x635 * x645;
+ uint128_t x686 = (uint128_t) x633 * x647;
  uint128_t x687 = x685 + x686;
  uint128_t x688 = x684 + x687;
- uint128_t x689 = (uint128_t) 0x13 * x688;
+ uint128_t x689 = 0x13 * x688;
  uint128_t x690 = x683 + x689;
- uint128_t x691 = (uint128_t) x641 * (uint128_t) x651;
- uint128_t x692 = (uint128_t) x639 * (uint128_t) x643;
- uint128_t x693 = (uint128_t) x637 * (uint128_t) x645;
- uint128_t x694 = (uint128_t) x635 * (uint128_t) x647;
- uint128_t x695 = (uint128_t) x633 * (uint128_t) x649;
+ uint128_t x691 = (uint128_t) x641 * x651;
+ uint128_t x692 = (uint128_t) x639 * x643;
+ uint128_t x693 = (uint128_t) x637 * x645;
+ uint128_t x694 = (uint128_t) x635 * x647;
+ uint128_t x695 = (uint128_t) x633 * x649;
  uint128_t x696 = x694 + x695;
  uint128_t x697 = x693 + x696;
  uint128_t x698 = x692 + x697;
- uint128_t x699 = (uint128_t) 0x13 * x698;
+ uint128_t x699 = 0x13 * x698;
  uint128_t x700 = x691 + x699;
  uint64_t x701 = (uint64_t) (x700 >> 0x33);
- uint128_t x702 = (uint128_t) x701 + x690;
+ uint128_t x702 = x701 + x690;
  uint64_t x703 = (uint64_t) (x702 >> 0x33);
- uint128_t x704 = (uint128_t) x703 + x680;
+ uint128_t x704 = x703 + x680;
  uint64_t x705 = (uint64_t) (x704 >> 0x33);
- uint128_t x706 = (uint128_t) x705 + x670;
+ uint128_t x706 = x705 + x670;
  uint64_t x707 = (uint64_t) (x706 >> 0x33);
- uint128_t x708 = (uint128_t) x707 + x660;
+ uint128_t x708 = x707 + x660;
  uint64_t x709 = (uint64_t) x700 & 0x7ffffffffffff;
  uint64_t x710 = (uint64_t) (x708 >> 0x33);
  uint64_t x711 = 0x13 * x710;
  uint64_t x712 = x709 + x711;
- uint64_t x713 = (uint64_t) (x712 >> 0x33);
+ uint64_t x713 = x712 >> 0x33;
  uint64_t x714 = (uint64_t) x702 & 0x7ffffffffffff;
  uint64_t x715 = x713 + x714;
  uint64_t x716 = (uint64_t) x708 & 0x7ffffffffffff;
  uint64_t x717 = (uint64_t) x706 & 0x7ffffffffffff;
- uint64_t x718 = (uint64_t) (x715 >> 0x33);
+ uint64_t x718 = x715 >> 0x33;
  uint64_t x719 = (uint64_t) x704 & 0x7ffffffffffff;
  uint64_t x720 = x718 + x719;
  uint64_t x721 = x715 & 0x7ffffffffffff;
  uint64_t x722 = x712 & 0x7ffffffffffff;
- uint128_t x723 = (uint128_t) x10 * (uint128_t) x716;
- uint128_t x724 = (uint128_t) x12 * (uint128_t) x717;
- uint128_t x725 = (uint128_t) x14 * (uint128_t) x720;
- uint128_t x726 = (uint128_t) x16 * (uint128_t) x721;
- uint128_t x727 = (uint128_t) x15 * (uint128_t) x722;
+ uint128_t x723 = (uint128_t) x10 * x716;
+ uint128_t x724 = (uint128_t) x12 * x717;
+ uint128_t x725 = (uint128_t) x14 * x720;
+ uint128_t x726 = (uint128_t) x16 * x721;
+ uint128_t x727 = (uint128_t) x15 * x722;
  uint128_t x728 = x726 + x727;
  uint128_t x729 = x725 + x728;
  uint128_t x730 = x724 + x729;
  uint128_t x731 = x723 + x730;
- uint128_t x732 = (uint128_t) x10 * (uint128_t) x717;
- uint128_t x733 = (uint128_t) x12 * (uint128_t) x720;
- uint128_t x734 = (uint128_t) x14 * (uint128_t) x721;
- uint128_t x735 = (uint128_t) x16 * (uint128_t) x722;
+ uint128_t x732 = (uint128_t) x10 * x717;
+ uint128_t x733 = (uint128_t) x12 * x720;
+ uint128_t x734 = (uint128_t) x14 * x721;
+ uint128_t x735 = (uint128_t) x16 * x722;
  uint128_t x736 = x734 + x735;
  uint128_t x737 = x733 + x736;
  uint128_t x738 = x732 + x737;
- uint128_t x739 = (uint128_t) x15 * (uint128_t) x716;
- uint128_t x740 = (uint128_t) 0x13 * x739;
+ uint128_t x739 = (uint128_t) x15 * x716;
+ uint128_t x740 = 0x13 * x739;
  uint128_t x741 = x738 + x740;
- uint128_t x742 = (uint128_t) x10 * (uint128_t) x720;
- uint128_t x743 = (uint128_t) x12 * (uint128_t) x721;
- uint128_t x744 = (uint128_t) x14 * (uint128_t) x722;
+ uint128_t x742 = (uint128_t) x10 * x720;
+ uint128_t x743 = (uint128_t) x12 * x721;
+ uint128_t x744 = (uint128_t) x14 * x722;
  uint128_t x745 = x743 + x744;
  uint128_t x746 = x742 + x745;
- uint128_t x747 = (uint128_t) x16 * (uint128_t) x716;
- uint128_t x748 = (uint128_t) x15 * (uint128_t) x717;
+ uint128_t x747 = (uint128_t) x16 * x716;
+ uint128_t x748 = (uint128_t) x15 * x717;
  uint128_t x749 = x747 + x748;
- uint128_t x750 = (uint128_t) 0x13 * x749;
+ uint128_t x750 = 0x13 * x749;
  uint128_t x751 = x746 + x750;
- uint128_t x752 = (uint128_t) x10 * (uint128_t) x721;
- uint128_t x753 = (uint128_t) x12 * (uint128_t) x722;
+ uint128_t x752 = (uint128_t) x10 * x721;
+ uint128_t x753 = (uint128_t) x12 * x722;
  uint128_t x754 = x752 + x753;
- uint128_t x755 = (uint128_t) x14 * (uint128_t) x716;
- uint128_t x756 = (uint128_t) x16 * (uint128_t) x717;
- uint128_t x757 = (uint128_t) x15 * (uint128_t) x720;
+ uint128_t x755 = (uint128_t) x14 * x716;
+ uint128_t x756 = (uint128_t) x16 * x717;
+ uint128_t x757 = (uint128_t) x15 * x720;
  uint128_t x758 = x756 + x757;
  uint128_t x759 = x755 + x758;
- uint128_t x760 = (uint128_t) 0x13 * x759;
+ uint128_t x760 = 0x13 * x759;
  uint128_t x761 = x754 + x760;
- uint128_t x762 = (uint128_t) x10 * (uint128_t) x722;
- uint128_t x763 = (uint128_t) x12 * (uint128_t) x716;
- uint128_t x764 = (uint128_t) x14 * (uint128_t) x717;
- uint128_t x765 = (uint128_t) x16 * (uint128_t) x720;
- uint128_t x766 = (uint128_t) x15 * (uint128_t) x721;
+ uint128_t x762 = (uint128_t) x10 * x722;
+ uint128_t x763 = (uint128_t) x12 * x716;
+ uint128_t x764 = (uint128_t) x14 * x717;
+ uint128_t x765 = (uint128_t) x16 * x720;
+ uint128_t x766 = (uint128_t) x15 * x721;
  uint128_t x767 = x765 + x766;
  uint128_t x768 = x764 + x767;
  uint128_t x769 = x763 + x768;
- uint128_t x770 = (uint128_t) 0x13 * x769;
+ uint128_t x770 = 0x13 * x769;
  uint128_t x771 = x762 + x770;
  uint64_t x772 = (uint64_t) (x771 >> 0x33);
- uint128_t x773 = (uint128_t) x772 + x761;
+ uint128_t x773 = x772 + x761;
  uint64_t x774 = (uint64_t) (x773 >> 0x33);
- uint128_t x775 = (uint128_t) x774 + x751;
+ uint128_t x775 = x774 + x751;
  uint64_t x776 = (uint64_t) (x775 >> 0x33);
- uint128_t x777 = (uint128_t) x776 + x741;
+ uint128_t x777 = x776 + x741;
  uint64_t x778 = (uint64_t) (x777 >> 0x33);
- uint128_t x779 = (uint128_t) x778 + x731;
+ uint128_t x779 = x778 + x731;
  uint64_t x780 = (uint64_t) x771 & 0x7ffffffffffff;
  uint64_t x781 = (uint64_t) (x779 >> 0x33);
  uint64_t x782 = 0x13 * x781;
  uint64_t x783 = x780 + x782;
- uint64_t x784 = (uint64_t) (x783 >> 0x33);
+ uint64_t x784 = x783 >> 0x33;
  uint64_t x785 = (uint64_t) x773 & 0x7ffffffffffff;
  uint64_t x786 = x784 + x785;
  uint64_t x787 = (uint64_t) x779 & 0x7ffffffffffff;
  uint64_t x788 = (uint64_t) x777 & 0x7ffffffffffff;
- uint64_t x789 = (uint64_t) (x786 >> 0x33);
+ uint64_t x789 = x786 >> 0x33;
  uint64_t x790 = (uint64_t) x775 & 0x7ffffffffffff;
  uint64_t x791 = x789 + x790;
  uint64_t x792 = x786 & 0x7ffffffffffff;
diff --git a/src/Specific/IntegrationTestMulDisplay.log b/src/Specific/IntegrationTestMulDisplay.log
index 71e3e649b..864cbd444 100644
--- a/src/Specific/IntegrationTestMulDisplay.log
+++ b/src/Specific/IntegrationTestMulDisplay.log
@@ -2,73 +2,73 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
- uint128_t x20 = (uint128_t) x5 * (uint128_t) x18;
- uint128_t x21 = (uint128_t) x7 * (uint128_t) x19;
- uint128_t x22 = (uint128_t) x9 * (uint128_t) x17;
- uint128_t x23 = (uint128_t) x11 * (uint128_t) x15;
- uint128_t x24 = (uint128_t) x10 * (uint128_t) x13;
+ uint128_t x20 = (uint128_t) x5 * x18;
+ uint128_t x21 = (uint128_t) x7 * x19;
+ uint128_t x22 = (uint128_t) x9 * x17;
+ uint128_t x23 = (uint128_t) x11 * x15;
+ uint128_t x24 = (uint128_t) x10 * x13;
  uint128_t x25 = x23 + x24;
  uint128_t x26 = x22 + x25;
  uint128_t x27 = x21 + x26;
  uint128_t x28 = x20 + x27;
- uint128_t x29 = (uint128_t) x5 * (uint128_t) x19;
- uint128_t x30 = (uint128_t) x7 * (uint128_t) x17;
- uint128_t x31 = (uint128_t) x9 * (uint128_t) x15;
- uint128_t x32 = (uint128_t) x11 * (uint128_t) x13;
+ uint128_t x29 = (uint128_t) x5 * x19;
+ uint128_t x30 = (uint128_t) x7 * x17;
+ uint128_t x31 = (uint128_t) x9 * x15;
+ uint128_t x32 = (uint128_t) x11 * x13;
  uint128_t x33 = x31 + x32;
  uint128_t x34 = x30 + x33;
  uint128_t x35 = x29 + x34;
- uint128_t x36 = (uint128_t) x10 * (uint128_t) x18;
- uint128_t x37 = (uint128_t) 0x13 * x36;
+ uint128_t x36 = (uint128_t) x10 * x18;
+ uint128_t x37 = 0x13 * x36;
  uint128_t x38 = x35 + x37;
- uint128_t x39 = (uint128_t) x5 * (uint128_t) x17;
- uint128_t x40 = (uint128_t) x7 * (uint128_t) x15;
- uint128_t x41 = (uint128_t) x9 * (uint128_t) x13;
+ uint128_t x39 = (uint128_t) x5 * x17;
+ uint128_t x40 = (uint128_t) x7 * x15;
+ uint128_t x41 = (uint128_t) x9 * x13;
  uint128_t x42 = x40 + x41;
  uint128_t x43 = x39 + x42;
- uint128_t x44 = (uint128_t) x11 * (uint128_t) x18;
- uint128_t x45 = (uint128_t) x10 * (uint128_t) x19;
+ uint128_t x44 = (uint128_t) x11 * x18;
+ uint128_t x45 = (uint128_t) x10 * x19;
  uint128_t x46 = x44 + x45;
- uint128_t x47 = (uint128_t) 0x13 * x46;
+ uint128_t x47 = 0x13 * x46;
  uint128_t x48 = x43 + x47;
- uint128_t x49 = (uint128_t) x5 * (uint128_t) x15;
- uint128_t x50 = (uint128_t) x7 * (uint128_t) x13;
+ uint128_t x49 = (uint128_t) x5 * x15;
+ uint128_t x50 = (uint128_t) x7 * x13;
  uint128_t x51 = x49 + x50;
- uint128_t x52 = (uint128_t) x9 * (uint128_t) x18;
- uint128_t x53 = (uint128_t) x11 * (uint128_t) x19;
- uint128_t x54 = (uint128_t) x10 * (uint128_t) x17;
+ uint128_t x52 = (uint128_t) x9 * x18;
+ uint128_t x53 = (uint128_t) x11 * x19;
+ uint128_t x54 = (uint128_t) x10 * x17;
  uint128_t x55 = x53 + x54;
  uint128_t x56 = x52 + x55;
- uint128_t x57 = (uint128_t) 0x13 * x56;
+ uint128_t x57 = 0x13 * x56;
  uint128_t x58 = x51 + x57;
- uint128_t x59 = (uint128_t) x5 * (uint128_t) x13;
- uint128_t x60 = (uint128_t) x7 * (uint128_t) x18;
- uint128_t x61 = (uint128_t) x9 * (uint128_t) x19;
- uint128_t x62 = (uint128_t) x11 * (uint128_t) x17;
- uint128_t x63 = (uint128_t) x10 * (uint128_t) x15;
+ uint128_t x59 = (uint128_t) x5 * x13;
+ uint128_t x60 = (uint128_t) x7 * x18;
+ uint128_t x61 = (uint128_t) x9 * x19;
+ uint128_t x62 = (uint128_t) x11 * x17;
+ uint128_t x63 = (uint128_t) x10 * x15;
  uint128_t x64 = x62 + x63;
  uint128_t x65 = x61 + x64;
  uint128_t x66 = x60 + x65;
- uint128_t x67 = (uint128_t) 0x13 * x66;
+ uint128_t x67 = 0x13 * x66;
  uint128_t x68 = x59 + x67;
  uint64_t x69 = (uint64_t) (x68 >> 0x33);
- uint128_t x70 = (uint128_t) x69 + x58;
+ uint128_t x70 = x69 + x58;
  uint64_t x71 = (uint64_t) (x70 >> 0x33);
- uint128_t x72 = (uint128_t) x71 + x48;
+ uint128_t x72 = x71 + x48;
  uint64_t x73 = (uint64_t) (x72 >> 0x33);
- uint128_t x74 = (uint128_t) x73 + x38;
+ uint128_t x74 = x73 + x38;
  uint64_t x75 = (uint64_t) (x74 >> 0x33);
- uint128_t x76 = (uint128_t) x75 + x28;
+ uint128_t x76 = x75 + x28;
  uint64_t x77 = (uint64_t) x68 & 0x7ffffffffffff;
  uint64_t x78 = (uint64_t) (x76 >> 0x33);
  uint64_t x79 = 0x13 * x78;
  uint64_t x80 = x77 + x79;
- uint64_t x81 = (uint64_t) (x80 >> 0x33);
+ uint64_t x81 = x80 >> 0x33;
  uint64_t x82 = (uint64_t) x70 & 0x7ffffffffffff;
  uint64_t x83 = x81 + x82;
  uint64_t x84 = (uint64_t) x76 & 0x7ffffffffffff;
  uint64_t x85 = (uint64_t) x74 & 0x7ffffffffffff;
- uint64_t x86 = (uint64_t) (x83 >> 0x33);
+ uint64_t x86 = x83 >> 0x33;
  uint64_t x87 = (uint64_t) x72 & 0x7ffffffffffff;
  uint64_t x88 = x86 + x87;
  uint64_t x89 = x83 & 0x7ffffffffffff;
diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index 581ac0d3e..a5c11a0d9 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -2,73 +2,73 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x7, x8, x6, x4, x2)%core,
- uint128_t x9 = (uint128_t) x2 * (uint128_t) x7;
- uint128_t x10 = (uint128_t) x4 * (uint128_t) x8;
- uint128_t x11 = (uint128_t) x6 * (uint128_t) x6;
- uint128_t x12 = (uint128_t) x8 * (uint128_t) x4;
- uint128_t x13 = (uint128_t) x7 * (uint128_t) x2;
+ uint128_t x9 = (uint128_t) x2 * x7;
+ uint128_t x10 = (uint128_t) x4 * x8;
+ uint128_t x11 = (uint128_t) x6 * x6;
+ uint128_t x12 = (uint128_t) x8 * x4;
+ uint128_t x13 = (uint128_t) x7 * x2;
  uint128_t x14 = x12 + x13;
  uint128_t x15 = x11 + x14;
  uint128_t x16 = x10 + x15;
  uint128_t x17 = x9 + x16;
- uint128_t x18 = (uint128_t) x2 * (uint128_t) x8;
- uint128_t x19 = (uint128_t) x4 * (uint128_t) x6;
- uint128_t x20 = (uint128_t) x6 * (uint128_t) x4;
- uint128_t x21 = (uint128_t) x8 * (uint128_t) x2;
+ uint128_t x18 = (uint128_t) x2 * x8;
+ uint128_t x19 = (uint128_t) x4 * x6;
+ uint128_t x20 = (uint128_t) x6 * x4;
+ uint128_t x21 = (uint128_t) x8 * x2;
  uint128_t x22 = x20 + x21;
  uint128_t x23 = x19 + x22;
  uint128_t x24 = x18 + x23;
- uint128_t x25 = (uint128_t) x7 * (uint128_t) x7;
- uint128_t x26 = (uint128_t) 0x13 * x25;
+ uint128_t x25 = (uint128_t) x7 * x7;
+ uint128_t x26 = 0x13 * x25;
  uint128_t x27 = x24 + x26;
- uint128_t x28 = (uint128_t) x2 * (uint128_t) x6;
- uint128_t x29 = (uint128_t) x4 * (uint128_t) x4;
- uint128_t x30 = (uint128_t) x6 * (uint128_t) x2;
+ uint128_t x28 = (uint128_t) x2 * x6;
+ uint128_t x29 = (uint128_t) x4 * x4;
+ uint128_t x30 = (uint128_t) x6 * x2;
  uint128_t x31 = x29 + x30;
  uint128_t x32 = x28 + x31;
- uint128_t x33 = (uint128_t) x8 * (uint128_t) x7;
- uint128_t x34 = (uint128_t) x7 * (uint128_t) x8;
+ uint128_t x33 = (uint128_t) x8 * x7;
+ uint128_t x34 = (uint128_t) x7 * x8;
  uint128_t x35 = x33 + x34;
- uint128_t x36 = (uint128_t) 0x13 * x35;
+ uint128_t x36 = 0x13 * x35;
  uint128_t x37 = x32 + x36;
- uint128_t x38 = (uint128_t) x2 * (uint128_t) x4;
- uint128_t x39 = (uint128_t) x4 * (uint128_t) x2;
+ uint128_t x38 = (uint128_t) x2 * x4;
+ uint128_t x39 = (uint128_t) x4 * x2;
  uint128_t x40 = x38 + x39;
- uint128_t x41 = (uint128_t) x6 * (uint128_t) x7;
- uint128_t x42 = (uint128_t) x8 * (uint128_t) x8;
- uint128_t x43 = (uint128_t) x7 * (uint128_t) x6;
+ uint128_t x41 = (uint128_t) x6 * x7;
+ uint128_t x42 = (uint128_t) x8 * x8;
+ uint128_t x43 = (uint128_t) x7 * x6;
  uint128_t x44 = x42 + x43;
  uint128_t x45 = x41 + x44;
- uint128_t x46 = (uint128_t) 0x13 * x45;
+ uint128_t x46 = 0x13 * x45;
  uint128_t x47 = x40 + x46;
- uint128_t x48 = (uint128_t) x2 * (uint128_t) x2;
- uint128_t x49 = (uint128_t) x4 * (uint128_t) x7;
- uint128_t x50 = (uint128_t) x6 * (uint128_t) x8;
- uint128_t x51 = (uint128_t) x8 * (uint128_t) x6;
- uint128_t x52 = (uint128_t) x7 * (uint128_t) x4;
+ uint128_t x48 = (uint128_t) x2 * x2;
+ uint128_t x49 = (uint128_t) x4 * x7;
+ uint128_t x50 = (uint128_t) x6 * x8;
+ uint128_t x51 = (uint128_t) x8 * x6;
+ uint128_t x52 = (uint128_t) x7 * x4;
  uint128_t x53 = x51 + x52;
  uint128_t x54 = x50 + x53;
  uint128_t x55 = x49 + x54;
- uint128_t x56 = (uint128_t) 0x13 * x55;
+ uint128_t x56 = 0x13 * x55;
  uint128_t x57 = x48 + x56;
  uint64_t x58 = (uint64_t) (x57 >> 0x33);
- uint128_t x59 = (uint128_t) x58 + x47;
+ uint128_t x59 = x58 + x47;
  uint64_t x60 = (uint64_t) (x59 >> 0x33);
- uint128_t x61 = (uint128_t) x60 + x37;
+ uint128_t x61 = x60 + x37;
  uint64_t x62 = (uint64_t) (x61 >> 0x33);
- uint128_t x63 = (uint128_t) x62 + x27;
+ uint128_t x63 = x62 + x27;
  uint64_t x64 = (uint64_t) (x63 >> 0x33);
- uint128_t x65 = (uint128_t) x64 + x17;
+ uint128_t x65 = x64 + x17;
  uint64_t x66 = (uint64_t) x57 & 0x7ffffffffffff;
  uint64_t x67 = (uint64_t) (x65 >> 0x33);
  uint64_t x68 = 0x13 * x67;
  uint64_t x69 = x66 + x68;
- uint64_t x70 = (uint64_t) (x69 >> 0x33);
+ uint64_t x70 = x69 >> 0x33;
  uint64_t x71 = (uint64_t) x59 & 0x7ffffffffffff;
  uint64_t x72 = x70 + x71;
  uint64_t x73 = (uint64_t) x65 & 0x7ffffffffffff;
  uint64_t x74 = (uint64_t) x63 & 0x7ffffffffffff;
- uint64_t x75 = (uint64_t) (x72 >> 0x33);
+ uint64_t x75 = x72 >> 0x33;
  uint64_t x76 = (uint64_t) x61 & 0x7ffffffffffff;
  uint64_t x77 = x75 + x76;
  uint64_t x78 = x72 & 0x7ffffffffffff;
diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log
index 831da160f..7a7d67779 100644
--- a/src/Specific/IntegrationTestSubDisplay.log
+++ b/src/Specific/IntegrationTestSubDisplay.log
@@ -12,24 +12,24 @@ Interp-η
  uint64_t x27 = x26 - x15;
  uint64_t x28 = 0xfffffffffffda + x5;
  uint64_t x29 = x28 - x13;
- uint64_t x30 = (uint64_t) (x29 >> 0x33);
+ uint64_t x30 = x29 >> 0x33;
  uint64_t x31 = x30 + x27;
- uint64_t x32 = (uint64_t) (x31 >> 0x33);
+ uint64_t x32 = x31 >> 0x33;
  uint64_t x33 = x32 + x25;
- uint64_t x34 = (uint64_t) (x33 >> 0x33);
+ uint64_t x34 = x33 >> 0x33;
  uint64_t x35 = x34 + x23;
- uint64_t x36 = (uint64_t) (x35 >> 0x33);
+ uint64_t x36 = x35 >> 0x33;
  uint64_t x37 = x36 + x21;
  uint64_t x38 = x29 & 0x7ffffffffffff;
- uint64_t x39 = (uint64_t) (x37 >> 0x33);
+ uint64_t x39 = x37 >> 0x33;
  uint64_t x40 = 0x13 * x39;
  uint64_t x41 = x38 + x40;
- uint64_t x42 = (uint64_t) (x41 >> 0x33);
+ uint64_t x42 = x41 >> 0x33;
  uint64_t x43 = x31 & 0x7ffffffffffff;
  uint64_t x44 = x42 + x43;
  uint64_t x45 = x37 & 0x7ffffffffffff;
  uint64_t x46 = x35 & 0x7ffffffffffff;
- uint64_t x47 = (uint64_t) (x44 >> 0x33);
+ uint64_t x47 = x44 >> 0x33;
  uint64_t x48 = x33 & 0x7ffffffffffff;
  uint64_t x49 = x47 + x48;
  uint64_t x50 = x44 & 0x7ffffffffffff;