Update display logs and c files

26 files changed, 36 insertions, 36 deletions

diff --git a/src/Specific/solinas32_2e166m5/fesub.c b/src/Specific/solinas32_2e166m5/fesub.c
index 912d5f5d4..7fe218720 100644
--- a/src/Specific/solinas32_2e166m5/fesub.c
+++ b/src/Specific/solinas32_2e166m5/fesub.c
@@ -21,16 +21,16 @@ static void fesub(uint32_t out[11], const uint32_t in1[11], const uint32_t in2[1
   { const uint32_t x29 = in2[2];
   { const uint32_t x27 = in2[1];
   { const uint32_t x25 = in2[0];
-  out[0] = ((Const 131062 + x5) - x25);
-  out[1] = ((Const 65534 + x7) - x27);
-  out[2] = ((Const 65534 + x9) - x29);
-  out[3] = ((Const 65534 + x11) - x31);
-  out[4] = ((Const 65534 + x13) - x33);
-  out[5] = ((Const 65534 + x15) - x35);
-  out[6] = ((Const 65534 + x17) - x37);
-  out[7] = ((Const 65534 + x19) - x39);
-  out[8] = ((Const 65534 + x21) - x41);
-  out[9] = ((Const 65534 + x23) - x43);
-  out[10] = ((Const 65534 + x22) - x42);
+  out[0] = ((0x1fff6 + x5) - x25);
+  out[1] = ((0xfffe + x7) - x27);
+  out[2] = ((0xfffe + x9) - x29);
+  out[3] = ((0xfffe + x11) - x31);
+  out[4] = ((0xfffe + x13) - x33);
+  out[5] = ((0xfffe + x15) - x35);
+  out[6] = ((0xfffe + x17) - x37);
+  out[7] = ((0xfffe + x19) - x39);
+  out[8] = ((0xfffe + x21) - x41);
+  out[9] = ((0xfffe + x23) - x43);
+  out[10] = ((0xfffe + x22) - x42);
   }}}}}}}}}}}}}}}}}}}}}}
 }
diff --git a/src/Specific/solinas32_2e166m5/fesubDisplay.log b/src/Specific/solinas32_2e166m5/fesubDisplay.log
index 9cb67d72e..6c9ba7556 100644
--- a/src/Specific/solinas32_2e166m5/fesubDisplay.log
+++ b/src/Specific/solinas32_2e166m5/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x22, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x42, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25))%core,
- (((Const 65534 + x22) - x42), ((Const 65534 + x23) - x43), ((Const 65534 + x21) - x41), ((Const 65534 + x19) - x39), ((Const 65534 + x17) - x37), ((Const 65534 + x15) - x35), ((Const 65534 + x13) - x33), ((Const 65534 + x11) - x31), ((Const 65534 + x9) - x29), ((Const 65534 + x7) - x27), ((Const 131062 + x5) - x25)))
+ (((0xfffe + x22) - x42), ((0xfffe + x23) - x43), ((0xfffe + x21) - x41), ((0xfffe + x19) - x39), ((0xfffe + x17) - x37), ((0xfffe + x15) - x35), ((0xfffe + x13) - x33), ((0xfffe + x11) - x31), ((0xfffe + x9) - x29), ((0xfffe + x7) - x27), ((0x1fff6 + x5) - x25)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e191m19/fesub.c b/src/Specific/solinas32_2e191m19/fesub.c
index 34abdaf30..0f6205aaa 100644
--- a/src/Specific/solinas32_2e191m19/fesub.c
+++ b/src/Specific/solinas32_2e191m19/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint32_t out[10], const uint32_t in1[10], const uint32_t in2[1
   { const uint32_t x27 = in2[2];
   { const uint32_t x25 = in2[1];
   { const uint32_t x23 = in2[0];
-  out[0] = ((Const 2097114 + x5) - x23);
+  out[0] = ((0x1fffda + x5) - x23);
   out[1] = ((0xffffe + x7) - x25);
   out[2] = ((0xffffe + x9) - x27);
   out[3] = ((0xffffe + x11) - x29);
diff --git a/src/Specific/solinas32_2e191m19/fesubDisplay.log b/src/Specific/solinas32_2e191m19/fesubDisplay.log
index 823ae1fc4..ca10cda56 100644
--- a/src/Specific/solinas32_2e191m19/fesubDisplay.log
+++ b/src/Specific/solinas32_2e191m19/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xffffe + x20) - x38), ((0xffffe + x21) - x39), ((0xffffe + x19) - x37), ((0xffffe + x17) - x35), ((0xffffe + x15) - x33), ((0xffffe + x13) - x31), ((0xffffe + x11) - x29), ((0xffffe + x9) - x27), ((0xffffe + x7) - x25), ((Const 2097114 + x5) - x23)))
+ (((0xffffe + x20) - x38), ((0xffffe + x21) - x39), ((0xffffe + x19) - x37), ((0xffffe + x17) - x35), ((0xffffe + x15) - x33), ((0xffffe + x13) - x31), ((0xffffe + x11) - x29), ((0xffffe + x9) - x27), ((0xffffe + x7) - x25), ((0x1fffda + x5) - x23)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e205m45x2e198m1/fesub.c b/src/Specific/solinas32_2e205m45x2e198m1/fesub.c
index 583193f60..4765a9a13 100644
--- a/src/Specific/solinas32_2e205m45x2e198m1/fesub.c
+++ b/src/Specific/solinas32_2e205m45x2e198m1/fesub.c
@@ -28,6 +28,6 @@ static void fesub(uint32_t out[10], const uint32_t in1[10], const uint32_t in2[1
   out[6] = ((0x3ffffe + x17) - x35);
   out[7] = ((0x1ffffe + x19) - x37);
   out[8] = ((0x3ffffe + x21) - x39);
-  out[9] = ((Const 1359870 + x20) - x38);
+  out[9] = ((0x14bffe + x20) - x38);
   }}}}}}}}}}}}}}}}}}}}
 }
diff --git a/src/Specific/solinas32_2e205m45x2e198m1/fesubDisplay.log b/src/Specific/solinas32_2e205m45x2e198m1/fesubDisplay.log
index 73710dc9d..44e21f164 100644
--- a/src/Specific/solinas32_2e205m45x2e198m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e205m45x2e198m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((Const 1359870 + x20) - x38), ((0x3ffffe + x21) - x39), ((0x1ffffe + x19) - x37), ((0x3ffffe + x17) - x35), ((0x1ffffe + x15) - x33), ((0x3ffffe + x13) - x31), ((0x1ffffe + x11) - x29), ((0x3ffffe + x9) - x27), ((0x1ffffe + x7) - x25), ((0x3ffffe + x5) - x23)))
+ (((0x14bffe + x20) - x38), ((0x3ffffe + x21) - x39), ((0x1ffffe + x19) - x37), ((0x3ffffe + x17) - x35), ((0x1ffffe + x15) - x33), ((0x3ffffe + x13) - x31), ((0x1ffffe + x11) - x29), ((0x3ffffe + x9) - x27), ((0x1ffffe + x7) - x25), ((0x3ffffe + x5) - x23)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e221m3/fesub.c b/src/Specific/solinas32_2e221m3/fesub.c
index bde8658ed..d324a881f 100644
--- a/src/Specific/solinas32_2e221m3/fesub.c
+++ b/src/Specific/solinas32_2e221m3/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint32_t out[10], const uint32_t in1[10], const uint32_t in2[1
   { const uint32_t x27 = in2[2];
   { const uint32_t x25 = in2[1];
   { const uint32_t x23 = in2[0];
-  out[0] = ((Const 16777210 + x5) - x23);
+  out[0] = ((0xfffffa + x5) - x23);
   out[1] = ((0x7ffffe + x7) - x25);
   out[2] = ((0x7ffffe + x9) - x27);
   out[3] = ((0x7ffffe + x11) - x29);
diff --git a/src/Specific/solinas32_2e221m3/fesubDisplay.log b/src/Specific/solinas32_2e221m3/fesubDisplay.log
index 290e3f8d4..b3eb238fa 100644
--- a/src/Specific/solinas32_2e221m3/fesubDisplay.log
+++ b/src/Specific/solinas32_2e221m3/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0x7ffffe + x20) - x38), ((0x7ffffe + x21) - x39), ((0x7ffffe + x19) - x37), ((0x7ffffe + x17) - x35), ((0x7ffffe + x15) - x33), ((0x7ffffe + x13) - x31), ((0x7ffffe + x11) - x29), ((0x7ffffe + x9) - x27), ((0x7ffffe + x7) - x25), ((Const 16777210 + x5) - x23)))
+ (((0x7ffffe + x20) - x38), ((0x7ffffe + x21) - x39), ((0x7ffffe + x19) - x37), ((0x7ffffe + x17) - x35), ((0x7ffffe + x15) - x33), ((0x7ffffe + x13) - x31), ((0x7ffffe + x11) - x29), ((0x7ffffe + x9) - x27), ((0x7ffffe + x7) - x25), ((0xfffffa + x5) - x23)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e222m117/fesub.c b/src/Specific/solinas32_2e222m117/fesub.c
index 8a3ae582a..ebf300def 100644
--- a/src/Specific/solinas32_2e222m117/fesub.c
+++ b/src/Specific/solinas32_2e222m117/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint32_t out[10], const uint32_t in1[10], const uint32_t in2[1
   { const uint32_t x27 = in2[2];
   { const uint32_t x25 = in2[1];
   { const uint32_t x23 = in2[0];
-  out[0] = ((Const 16776982 + x5) - x23);
+  out[0] = ((0xffff16 + x5) - x23);
   out[1] = ((0x7ffffe + x7) - x25);
   out[2] = ((0x7ffffe + x9) - x27);
   out[3] = ((0x7ffffe + x11) - x29);
diff --git a/src/Specific/solinas32_2e222m117/fesubDisplay.log b/src/Specific/solinas32_2e222m117/fesubDisplay.log
index e1d387497..05a560f1e 100644
--- a/src/Specific/solinas32_2e222m117/fesubDisplay.log
+++ b/src/Specific/solinas32_2e222m117/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0x7ffffe + x20) - x38), ((0x7ffffe + x21) - x39), ((0x7ffffe + x19) - x37), ((0x7ffffe + x17) - x35), ((0xfffffe + x15) - x33), ((0x7ffffe + x13) - x31), ((0x7ffffe + x11) - x29), ((0x7ffffe + x9) - x27), ((0x7ffffe + x7) - x25), ((Const 16776982 + x5) - x23)))
+ (((0x7ffffe + x20) - x38), ((0x7ffffe + x21) - x39), ((0x7ffffe + x19) - x37), ((0x7ffffe + x17) - x35), ((0xfffffe + x15) - x33), ((0x7ffffe + x13) - x31), ((0x7ffffe + x11) - x29), ((0x7ffffe + x9) - x27), ((0x7ffffe + x7) - x25), ((0xffff16 + x5) - x23)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e230m27/fesub.c b/src/Specific/solinas32_2e230m27/fesub.c
index 7aac9e122..7a81c7e89 100644
--- a/src/Specific/solinas32_2e230m27/fesub.c
+++ b/src/Specific/solinas32_2e230m27/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint32_t out[10], const uint32_t in1[10], const uint32_t in2[1
   { const uint32_t x27 = in2[2];
   { const uint32_t x25 = in2[1];
   { const uint32_t x23 = in2[0];
-  out[0] = ((Const 16777162 + x5) - x23);
+  out[0] = ((0xffffca + x5) - x23);
   out[1] = ((0xfffffe + x7) - x25);
   out[2] = ((0xfffffe + x9) - x27);
   out[3] = ((0xfffffe + x11) - x29);
diff --git a/src/Specific/solinas32_2e230m27/fesubDisplay.log b/src/Specific/solinas32_2e230m27/fesubDisplay.log
index b9125ad53..d40b94113 100644
--- a/src/Specific/solinas32_2e230m27/fesubDisplay.log
+++ b/src/Specific/solinas32_2e230m27/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xfffffe + x20) - x38), ((0xfffffe + x21) - x39), ((0xfffffe + x19) - x37), ((0xfffffe + x17) - x35), ((0xfffffe + x15) - x33), ((0xfffffe + x13) - x31), ((0xfffffe + x11) - x29), ((0xfffffe + x9) - x27), ((0xfffffe + x7) - x25), ((Const 16777162 + x5) - x23)))
+ (((0xfffffe + x20) - x38), ((0xfffffe + x21) - x39), ((0xfffffe + x19) - x37), ((0xfffffe + x17) - x35), ((0xfffffe + x15) - x33), ((0xfffffe + x13) - x31), ((0xfffffe + x11) - x29), ((0xfffffe + x9) - x27), ((0xfffffe + x7) - x25), ((0xffffca + x5) - x23)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e254m127x2e240m1/fesub.c b/src/Specific/solinas32_2e254m127x2e240m1/fesub.c
index 1fdf14e21..a26cc1722 100644
--- a/src/Specific/solinas32_2e254m127x2e240m1/fesub.c
+++ b/src/Specific/solinas32_2e254m127x2e240m1/fesub.c
@@ -31,6 +31,6 @@ static void fesub(uint32_t out[11], const uint32_t in1[11], const uint32_t in2[1
   out[7] = ((0xfffffe + x19) - x39);
   out[8] = ((0xfffffe + x21) - x41);
   out[9] = ((0xfffffe + x23) - x43);
-  out[10] = ((Const 16647166 + x22) - x42);
+  out[10] = ((0xfe03fe + x22) - x42);
   }}}}}}}}}}}}}}}}}}}}}}
 }
diff --git a/src/Specific/solinas32_2e254m127x2e240m1/fesubDisplay.log b/src/Specific/solinas32_2e254m127x2e240m1/fesubDisplay.log
index 840a685b5..563bea7e2 100644
--- a/src/Specific/solinas32_2e254m127x2e240m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e254m127x2e240m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x22, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x42, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25))%core,
- (((Const 16647166 + x22) - x42), ((0xfffffe + x23) - x43), ((0xfffffe + x21) - x41), ((0xfffffe + x19) - x39), ((0xfffffe + x17) - x37), ((0xfffffe + x15) - x35), ((0xfffffe + x13) - x33), ((0xfffffe + x11) - x31), ((0xfffffe + x9) - x29), ((0xfffffe + x7) - x27), ((0x1fffffe + x5) - x25)))
+ (((0xfe03fe + x22) - x42), ((0xfffffe + x23) - x43), ((0xfffffe + x21) - x41), ((0xfffffe + x19) - x39), ((0xfffffe + x17) - x37), ((0xfffffe + x15) - x35), ((0xfffffe + x13) - x33), ((0xfffffe + x11) - x31), ((0xfffffe + x9) - x29), ((0xfffffe + x7) - x27), ((0x1fffffe + x5) - x25)))
 (x, x0)%core
      : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas64_2e382m105/fesub.c b/src/Specific/solinas64_2e382m105/fesub.c
index 7a07fe4cd..6716f8a9a 100644
--- a/src/Specific/solinas64_2e382m105/fesub.c
+++ b/src/Specific/solinas64_2e382m105/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   { const uint64_t x27 = in2[2];
   { const uint64_t x25 = in2[1];
   { const uint64_t x23 = in2[0];
-  out[0] = ((Const 1099511627566 + x5) - x23);
+  out[0] = ((0xffffffff2e + x5) - x23);
   out[1] = ((0x7ffffffffe + x7) - x25);
   out[2] = ((0x7ffffffffe + x9) - x27);
   out[3] = ((0x7ffffffffe + x11) - x29);
diff --git a/src/Specific/solinas64_2e382m105/fesubDisplay.log b/src/Specific/solinas64_2e382m105/fesubDisplay.log
index 960728d51..afaf245f9 100644
--- a/src/Specific/solinas64_2e382m105/fesubDisplay.log
+++ b/src/Specific/solinas64_2e382m105/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0x7ffffffffe + x20) - x38), ((0x7ffffffffe + x21) - x39), ((0x7ffffffffe + x19) - x37), ((0x7ffffffffe + x17) - x35), ((0xfffffffffe + x15) - x33), ((0x7ffffffffe + x13) - x31), ((0x7ffffffffe + x11) - x29), ((0x7ffffffffe + x9) - x27), ((0x7ffffffffe + x7) - x25), ((Const 1099511627566 + x5) - x23)))
+ (((0x7ffffffffe + x20) - x38), ((0x7ffffffffe + x21) - x39), ((0x7ffffffffe + x19) - x37), ((0x7ffffffffe + x17) - x35), ((0xfffffffffe + x15) - x33), ((0x7ffffffffe + x13) - x31), ((0x7ffffffffe + x11) - x29), ((0x7ffffffffe + x9) - x27), ((0x7ffffffffe + x7) - x25), ((0xffffffff2e + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e510m290x2e496m1/fesub.c b/src/Specific/solinas64_2e510m290x2e496m1/fesub.c
index 8fdc0e205..d1e8a3630 100644
--- a/src/Specific/solinas64_2e510m290x2e496m1/fesub.c
+++ b/src/Specific/solinas64_2e510m290x2e496m1/fesub.c
@@ -28,6 +28,6 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   out[6] = ((0xffffffffffffe + x17) - x35);
   out[7] = ((0xffffffffffffe + x19) - x37);
   out[8] = ((0xffffffffffffe + x21) - x39);
-  out[9] = ((Const 4423885034356734 + x20) - x38);
+  out[9] = ((0xfb77ffffffffe + x20) - x38);
   }}}}}}}}}}}}}}}}}}}}
 }
diff --git a/src/Specific/solinas64_2e510m290x2e496m1/fesubDisplay.log b/src/Specific/solinas64_2e510m290x2e496m1/fesubDisplay.log
index 48656a92f..928123979 100644
--- a/src/Specific/solinas64_2e510m290x2e496m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e510m290x2e496m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((Const 4423885034356734 + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0xffffffffffffe + x5) - x23)))
+ (((0xfb77ffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0xffffffffffffe + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e511m187/fesub.c b/src/Specific/solinas64_2e511m187/fesub.c
index 910b57602..f348c1776 100644
--- a/src/Specific/solinas64_2e511m187/fesub.c
+++ b/src/Specific/solinas64_2e511m187/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   { const uint64_t x27 = in2[2];
   { const uint64_t x25 = in2[1];
   { const uint64_t x23 = in2[0];
-  out[0] = ((Const 9007199254740618 + x5) - x23);
+  out[0] = ((0x1ffffffffffe8a + x5) - x23);
   out[1] = ((0xffffffffffffe + x7) - x25);
   out[2] = ((0xffffffffffffe + x9) - x27);
   out[3] = ((0xffffffffffffe + x11) - x29);
diff --git a/src/Specific/solinas64_2e511m187/fesubDisplay.log b/src/Specific/solinas64_2e511m187/fesubDisplay.log
index 69fbf1fc5..db1dc87a3 100644
--- a/src/Specific/solinas64_2e511m187/fesubDisplay.log
+++ b/src/Specific/solinas64_2e511m187/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((Const 9007199254740618 + x5) - x23)))
+ (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffe8a + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e511m481/fesub.c b/src/Specific/solinas64_2e511m481/fesub.c
index 1ee8b94fb..a7a7c08c9 100644
--- a/src/Specific/solinas64_2e511m481/fesub.c
+++ b/src/Specific/solinas64_2e511m481/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   { const uint64_t x27 = in2[2];
   { const uint64_t x25 = in2[1];
   { const uint64_t x23 = in2[0];
-  out[0] = ((Const 9007199254740030 + x5) - x23);
+  out[0] = ((0x1ffffffffffc3e + x5) - x23);
   out[1] = ((0xffffffffffffe + x7) - x25);
   out[2] = ((0xffffffffffffe + x9) - x27);
   out[3] = ((0xffffffffffffe + x11) - x29);
diff --git a/src/Specific/solinas64_2e511m481/fesubDisplay.log b/src/Specific/solinas64_2e511m481/fesubDisplay.log
index c5d4a9efe..993230713 100644
--- a/src/Specific/solinas64_2e511m481/fesubDisplay.log
+++ b/src/Specific/solinas64_2e511m481/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((Const 9007199254740030 + x5) - x23)))
+ (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0xffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffc3e + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m491x2e496m1/fesub.c b/src/Specific/solinas64_2e512m491x2e496m1/fesub.c
index 15300a2aa..b697af821 100644
--- a/src/Specific/solinas64_2e512m491x2e496m1/fesub.c
+++ b/src/Specific/solinas64_2e512m491x2e496m1/fesub.c
@@ -28,6 +28,6 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   out[6] = ((0xffffffffffffe + x17) - x35);
   out[7] = ((0xffffffffffffe + x19) - x37);
   out[8] = ((0xffffffffffffe + x21) - x39);
-  out[9] = ((Const 4469858364293118 + x20) - x38);
+  out[9] = ((0xfe14ffffffffe + x20) - x38);
   }}}}}}}}}}}}}}}}}}}}
 }
diff --git a/src/Specific/solinas64_2e512m491x2e496m1/fesubDisplay.log b/src/Specific/solinas64_2e512m491x2e496m1/fesubDisplay.log
index ab11c7015..070fac6ba 100644
--- a/src/Specific/solinas64_2e512m491x2e496m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e512m491x2e496m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((Const 4469858364293118 + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0x1ffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffffe + x5) - x23)))
+ (((0xfe14ffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0x1ffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffffe + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e512m569/fesub.c b/src/Specific/solinas64_2e512m569/fesub.c
index cb3077371..b2dd293f5 100644
--- a/src/Specific/solinas64_2e512m569/fesub.c
+++ b/src/Specific/solinas64_2e512m569/fesub.c
@@ -19,7 +19,7 @@ static void fesub(uint64_t out[10], const uint64_t in1[10], const uint64_t in2[1
   { const uint64_t x27 = in2[2];
   { const uint64_t x25 = in2[1];
   { const uint64_t x23 = in2[0];
-  out[0] = ((Const 9007199254739854 + x5) - x23);
+  out[0] = ((0x1ffffffffffb8e + x5) - x23);
   out[1] = ((0xffffffffffffe + x7) - x25);
   out[2] = ((0xffffffffffffe + x9) - x27);
   out[3] = ((0xffffffffffffe + x11) - x29);
diff --git a/src/Specific/solinas64_2e512m569/fesubDisplay.log b/src/Specific/solinas64_2e512m569/fesubDisplay.log
index 8471d38e7..07b0161a8 100644
--- a/src/Specific/solinas64_2e512m569/fesubDisplay.log
+++ b/src/Specific/solinas64_2e512m569/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
- (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0x1ffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((Const 9007199254739854 + x5) - x23)))
+ (((0xffffffffffffe + x20) - x38), ((0xffffffffffffe + x21) - x39), ((0xffffffffffffe + x19) - x37), ((0xffffffffffffe + x17) - x35), ((0x1ffffffffffffe + x15) - x33), ((0xffffffffffffe + x13) - x31), ((0xffffffffffffe + x11) - x29), ((0xffffffffffffe + x9) - x27), ((0xffffffffffffe + x7) - x25), ((0x1ffffffffffb8e + x5) - x23)))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)