Update display logs and c files

17 files changed, 17 insertions, 17 deletions

diff --git a/src/Specific/solinas32_2e137m13/fesubDisplay.log b/src/Specific/solinas32_2e137m13/fesubDisplay.log
index aa440b343..5f17ed0c7 100644
--- a/src/Specific/solinas32_2e137m13/fesubDisplay.log
+++ b/src/Specific/solinas32_2e137m13/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((Const 262142 + x16) - x30), ((Const 262142 + x17) - x31), ((Const 262142 + x15) - x29), ((Const 262142 + x13) - x27), ((Const 262142 + x11) - x25), ((Const 262142 + x9) - x23), ((Const 262142 + x7) - x21), ((Const 524262 + x5) - x19)))
+ (((0x3fffe + x16) - x30), ((0x3fffe + x17) - x31), ((0x3fffe + x15) - x29), ((0x3fffe + x13) - x27), ((0x3fffe + x11) - x25), ((0x3fffe + x9) - x23), ((0x3fffe + x7) - x21), ((0x7ffe6 + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas32_2e192m2e64m1/fesubDisplay.log b/src/Specific/solinas32_2e192m2e64m1/fesubDisplay.log
index 93429a863..094fa5bc5 100644
--- a/src/Specific/solinas32_2e192m2e64m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e192m2e64m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffe + x16) - x30), ((0x1fffffe + x17) - x31), ((0x1fffffe + x15) - x29), ((0x1fffffe + x13) - x27), ((0x1fffffe + x11) - x25), ((Const 33423358 + x9) - x23), ((0x1fffffe + x7) - x21), ((0x1fffffe + x5) - x19)))
+ (((0x1fffffe + x16) - x30), ((0x1fffffe + x17) - x31), ((0x1fffffe + x15) - x29), ((0x1fffffe + x13) - x27), ((0x1fffffe + x11) - x25), ((0x1fdfffe + x9) - x23), ((0x1fffffe + x7) - x21), ((0x1fffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas32_2e194m33/fesubDisplay.log b/src/Specific/solinas32_2e194m33/fesubDisplay.log
index b7d9e6729..ed0218289 100644
--- a/src/Specific/solinas32_2e194m33/fesubDisplay.log
+++ b/src/Specific/solinas32_2e194m33/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffe + x16) - x30), ((0x1fffffe + x17) - x31), ((0x1fffffe + x15) - x29), ((0x3fffffe + x13) - x27), ((0x1fffffe + x11) - x25), ((0x1fffffe + x9) - x23), ((0x1fffffe + x7) - x21), ((Const 67108798 + x5) - x19)))
+ (((0x1fffffe + x16) - x30), ((0x1fffffe + x17) - x31), ((0x1fffffe + x15) - x29), ((0x3fffffe + x13) - x27), ((0x1fffffe + x11) - x25), ((0x1fffffe + x9) - x23), ((0x1fffffe + x7) - x21), ((0x3ffffbe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas32_2e212m29/fesubDisplay.log b/src/Specific/solinas32_2e212m29/fesubDisplay.log
index fd46595d4..06372c648 100644
--- a/src/Specific/solinas32_2e212m29/fesubDisplay.log
+++ b/src/Specific/solinas32_2e212m29/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x7fffffe + x16) - x30), ((0xffffffe + x17) - x31), ((0x7fffffe + x15) - x29), ((0xffffffe + x13) - x27), ((0x7fffffe + x11) - x25), ((0xffffffe + x9) - x23), ((0x7fffffe + x7) - x21), ((Const 268435398 + x5) - x19)))
+ (((0x7fffffe + x16) - x30), ((0xffffffe + x17) - x31), ((0x7fffffe + x15) - x29), ((0xffffffe + x13) - x27), ((0x7fffffe + x11) - x25), ((0xffffffe + x9) - x23), ((0x7fffffe + x7) - x21), ((0xfffffc6 + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas32_2e216m2e108m1/fesubDisplay.log b/src/Specific/solinas32_2e216m2e108m1/fesubDisplay.log
index cbd824a7d..2176f748f 100644
--- a/src/Specific/solinas32_2e216m2e108m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e216m2e108m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0xffffffe + x16) - x30), ((0xffffffe + x17) - x31), ((0xffffffe + x15) - x29), ((Const 268435452 + x13) - x27), ((0xffffffe + x11) - x25), ((0xffffffe + x9) - x23), ((0xffffffe + x7) - x21), ((0xffffffe + x5) - x19)))
+ (((0xffffffe + x16) - x30), ((0xffffffe + x17) - x31), ((0xffffffe + x15) - x29), ((0xffffffc + x13) - x27), ((0xffffffe + x11) - x25), ((0xffffffe + x9) - x23), ((0xffffffe + x7) - x21), ((0xffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas32_2e226m5/fesubDisplay.log b/src/Specific/solinas32_2e226m5/fesubDisplay.log
index 3c74d260d..de2ab67ea 100644
--- a/src/Specific/solinas32_2e226m5/fesubDisplay.log
+++ b/src/Specific/solinas32_2e226m5/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1ffffffe + x16) - x30), ((0x1ffffffe + x17) - x31), ((0x1ffffffe + x15) - x29), ((0x3ffffffe + x13) - x27), ((0x1ffffffe + x11) - x25), ((0x1ffffffe + x9) - x23), ((0x1ffffffe + x7) - x21), ((Const 1073741814 + x5) - x19)))
+ (((0x1ffffffe + x16) - x30), ((0x1ffffffe + x17) - x31), ((0x1ffffffe + x15) - x29), ((0x3ffffffe + x13) - x27), ((0x1ffffffe + x11) - x25), ((0x1ffffffe + x9) - x23), ((0x1ffffffe + x7) - x21), ((0x3ffffff6 + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e369m25/fesubDisplay.log b/src/Specific/solinas64_2e369m25/fesubDisplay.log
index 7f6742d9b..4001ced5a 100644
--- a/src/Specific/solinas64_2e369m25/fesubDisplay.log
+++ b/src/Specific/solinas64_2e369m25/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x7ffffffffffe + x16) - x30), ((0x7ffffffffffe + x17) - x31), ((0x7ffffffffffe + x15) - x29), ((0x7ffffffffffe + x13) - x27), ((0x7ffffffffffe + x11) - x25), ((0x7ffffffffffe + x9) - x23), ((0x7ffffffffffe + x7) - x21), ((Const 281474976710606 + x5) - x19)))
+ (((0x7ffffffffffe + x16) - x30), ((0x7ffffffffffe + x17) - x31), ((0x7ffffffffffe + x15) - x29), ((0x7ffffffffffe + x13) - x27), ((0x7ffffffffffe + x11) - x25), ((0x7ffffffffffe + x9) - x23), ((0x7ffffffffffe + x7) - x21), ((0xffffffffffce + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e384m317/fesubDisplay.log b/src/Specific/solinas64_2e384m317/fesubDisplay.log
index da6d96576..61c5edf9e 100644
--- a/src/Specific/solinas64_2e384m317/fesubDisplay.log
+++ b/src/Specific/solinas64_2e384m317/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffffffffe + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((Const 562949953420678 + x5) - x19)))
+ (((0x1fffffffffffe + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((0x1fffffffffd86 + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e384m5x2e368m1/fesubDisplay.log b/src/Specific/solinas64_2e384m5x2e368m1/fesubDisplay.log
index ed106a446..5f33a6593 100644
--- a/src/Specific/solinas64_2e384m5x2e368m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e384m5x2e368m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((Const 562907003748350 + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((0x1fffffffffffe + x5) - x19)))
+ (((0x1fff5fffffffe + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((0x1fffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e384m79x2e376m1/fesubDisplay.log b/src/Specific/solinas64_2e384m79x2e376m1/fesubDisplay.log
index 5d18bbb73..36f2cfdf8 100644
--- a/src/Specific/solinas64_2e384m79x2e376m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e384m79x2e376m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((Const 389227116232702 + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((0x1fffffffffffe + x5) - x19)))
+ (((0x161fffffffffe + x16) - x30), ((0x1fffffffffffe + x17) - x31), ((0x1fffffffffffe + x15) - x29), ((0x1fffffffffffe + x13) - x27), ((0x1fffffffffffe + x11) - x25), ((0x1fffffffffffe + x9) - x23), ((0x1fffffffffffe + x7) - x21), ((0x1fffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e401m31/fesubDisplay.log b/src/Specific/solinas64_2e401m31/fesubDisplay.log
index f9b5ffa72..1130a3297 100644
--- a/src/Specific/solinas64_2e401m31/fesubDisplay.log
+++ b/src/Specific/solinas64_2e401m31/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x7fffffffffffe + x16) - x30), ((0x7fffffffffffe + x17) - x31), ((0x7fffffffffffe + x15) - x29), ((0x7fffffffffffe + x13) - x27), ((0x7fffffffffffe + x11) - x25), ((0x7fffffffffffe + x9) - x23), ((0x7fffffffffffe + x7) - x21), ((Const 4503599627370434 + x5) - x19)))
+ (((0x7fffffffffffe + x16) - x30), ((0x7fffffffffffe + x17) - x31), ((0x7fffffffffffe + x15) - x29), ((0x7fffffffffffe + x13) - x27), ((0x7fffffffffffe + x11) - x25), ((0x7fffffffffffe + x9) - x23), ((0x7fffffffffffe + x7) - x21), ((0xfffffffffffc2 + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e416m2e208m1/fesubDisplay.log b/src/Specific/solinas64_2e416m2e208m1/fesubDisplay.log
index 837a44010..d2e418157 100644
--- a/src/Specific/solinas64_2e416m2e208m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e416m2e208m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1ffffffffffffe + x16) - x30), ((0x1ffffffffffffe + x17) - x31), ((0x1ffffffffffffe + x15) - x29), ((Const 9007199254740988 + x13) - x27), ((0x1ffffffffffffe + x11) - x25), ((0x1ffffffffffffe + x9) - x23), ((0x1ffffffffffffe + x7) - x21), ((0x1ffffffffffffe + x5) - x19)))
+ (((0x1ffffffffffffe + x16) - x30), ((0x1ffffffffffffe + x17) - x31), ((0x1ffffffffffffe + x15) - x29), ((0x1ffffffffffffc + x13) - x27), ((0x1ffffffffffffe + x11) - x25), ((0x1ffffffffffffe + x9) - x23), ((0x1ffffffffffffe + x7) - x21), ((0x1ffffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e448m2e224m1/fesubDisplay.log b/src/Specific/solinas64_2e448m2e224m1/fesubDisplay.log
index 3d058aa10..35a6385e4 100644
--- a/src/Specific/solinas64_2e448m2e224m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e448m2e224m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffffffffffe + x16) - x30), ((0x1fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((Const 144115188075855868 + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x1fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((0x1fffffffffffffe + x5) - x19)))
+ (((0x1fffffffffffffe + x16) - x30), ((0x1fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((0x1fffffffffffffc + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x1fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((0x1fffffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e450m2e225m1/fesubDisplay.log b/src/Specific/solinas64_2e450m2e225m1/fesubDisplay.log
index 31744190d..948e27940 100644
--- a/src/Specific/solinas64_2e450m2e225m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e450m2e225m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffffffffffe + x16) - x30), ((0x1fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((Const 288230376151711740 + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x1fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((0x3fffffffffffffe + x5) - x19)))
+ (((0x1fffffffffffffe + x16) - x30), ((0x1fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((0x3fffffffffffffc + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x1fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((0x3fffffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e452m3/fesubDisplay.log b/src/Specific/solinas64_2e452m3/fesubDisplay.log
index e7f440eb6..540d6117a 100644
--- a/src/Specific/solinas64_2e452m3/fesubDisplay.log
+++ b/src/Specific/solinas64_2e452m3/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x1fffffffffffffe + x16) - x30), ((0x3fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((0x3fffffffffffffe + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x3fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((Const 288230376151711738 + x5) - x19)))
+ (((0x1fffffffffffffe + x16) - x30), ((0x3fffffffffffffe + x17) - x31), ((0x1fffffffffffffe + x15) - x29), ((0x3fffffffffffffe + x13) - x27), ((0x1fffffffffffffe + x11) - x25), ((0x3fffffffffffffe + x9) - x23), ((0x1fffffffffffffe + x7) - x21), ((0x3fffffffffffffa + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e468m17/fesubDisplay.log b/src/Specific/solinas64_2e468m17/fesubDisplay.log
index f67353a39..4164d6bf6 100644
--- a/src/Specific/solinas64_2e468m17/fesubDisplay.log
+++ b/src/Specific/solinas64_2e468m17/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((0x7fffffffffffffe + x16) - x30), ((0xffffffffffffffe + x17) - x31), ((0x7fffffffffffffe + x15) - x29), ((0xffffffffffffffe + x13) - x27), ((0x7fffffffffffffe + x11) - x25), ((0xffffffffffffffe + x9) - x23), ((0x7fffffffffffffe + x7) - x21), ((Const 1152921504606846942 + x5) - x19)))
+ (((0x7fffffffffffffe + x16) - x30), ((0xffffffffffffffe + x17) - x31), ((0x7fffffffffffffe + x15) - x29), ((0xffffffffffffffe + x13) - x27), ((0x7fffffffffffffe + x11) - x25), ((0xffffffffffffffe + x9) - x23), ((0x7fffffffffffffe + x7) - x21), ((0xfffffffffffffde + x5) - x19)))
 (x, x0)%core
      : 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)
diff --git a/src/Specific/solinas64_2e480m2e240m1/fesubDisplay.log b/src/Specific/solinas64_2e480m2e240m1/fesubDisplay.log
index 092044bb9..de0b3ae96 100644
--- a/src/Specific/solinas64_2e480m2e240m1/fesubDisplay.log
+++ b/src/Specific/solinas64_2e480m2e240m1/fesubDisplay.log
@@ -2,6 +2,6 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- (((Const 2305843009213693950 + x16) - x30), ((Const 2305843009213693950 + x17) - x31), ((Const 2305843009213693950 + x15) - x29), ((Const 2305843009213693948 + x13) - x27), ((Const 2305843009213693950 + x11) - x25), ((Const 2305843009213693950 + x9) - x23), ((Const 2305843009213693950 + x7) - x21), ((Const 2305843009213693950 + x5) - x19)))
+ (((0x1ffffffffffffffe + x16) - x30), ((0x1ffffffffffffffe + x17) - x31), ((0x1ffffffffffffffe + x15) - x29), ((0x1ffffffffffffffc + x13) - x27), ((0x1ffffffffffffffe + x11) - x25), ((0x1ffffffffffffffe + x9) - x23), ((0x1ffffffffffffffe + x7) - x21), ((0x1ffffffffffffffe + x5) - x19)))
 (x, x0)%core
      : 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)