Add more constant notations

2 files changed, 96 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 82f6b76a3..7113173f6 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -43,20 +43,26 @@ nums = tuple(sorted(set(systematic_nums + [
     524269,
     524271,
     524279,
+    524286,
     679935,
     1048471,
+    1048526,
+    1048538,
     1048549,
     1048557,
     1048559,
     1048573,
+    1048574,
     2060031,
     2081439,
     2094335,
     2096127,
     2096128,
+    2097118,
     2097127,
     2097135,
     2097143,
+    2097150,
     4193327,
     4193539,
     4193735,
@@ -71,6 +77,7 @@ nums = tuple(sorted(set(systematic_nums + [
     8323583,
     8388491,
     8388558,
+    8388574,
     8388577,
     8388581,
     8388591,
@@ -121,6 +128,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268435398,
     268435406,
     268435426,
+    268435438,
     268435441,
     268435445,
     268435452,
@@ -138,6 +146,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1054736383,
     1065418751,
     1073709055,
+    1073741786,
     1073741814,
     1073741818,
     1073741821,
@@ -245,6 +254,7 @@ nums = tuple(sorted(set(systematic_nums + [
     70368744177659,
     70368744177661,
     140737471578110,
+    140737488355294,
     140737488355303,
     140737488355313,
     140737488355319,
@@ -330,7 +340,9 @@ nums = tuple(sorted(set(systematic_nums + [
     36028797018963966,
     72056494526300160,
     72057594037927819,
+    72057594037927874,
     72057594037927886,
+    72057594037927894,
     72057594037927898,
     72057594037927919,
     72057594037927931,
@@ -859,6 +871,8 @@ Notation "'0b1111111111111101111'" (* 524271 (0x7ffef) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
 Notation "'0b1111111111111110111'" (* 524279 (0x7fff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0b1111111111111111110'" (* 524286 (0x7fffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111111'" (* 524287 (0x7ffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b10000000000000000000'" (* 524288 (0x80000) *)
@@ -869,6 +883,10 @@ Notation "'0b10100101111111111111'" (* 679935 (0xa5fff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b11111111111110010111'" (* 1048471 (0xfff97) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1).
+Notation "'0b11111111111111001110'" (* 1048526 (0xfffce) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b11111111111111011010'" (* 1048538 (0xfffda) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b11111111111111100101'" (* 1048549 (0xfffe5) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
 Notation "'0b11111111111111101101'" (* 1048557 (0xfffed) *)
@@ -877,6 +895,8 @@ Notation "'0b11111111111111101111'" (* 1048559 (0xfffef) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
 Notation "'0b11111111111111111101'" (* 1048573 (0xffffd) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0b11111111111111111110'" (* 1048574 (0xffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b11111111111111111111'" (* 1048575 (0xfffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b100000000000000000000'" (* 1048576 (0x100000) *)
@@ -893,12 +913,16 @@ Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111110000000000'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0b111111111111111011110'" (* 2097118 (0x1fffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0b111111111111111100111'" (* 2097127 (0x1fffe7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
 Notation "'0b111111111111111101111'" (* 2097135 (0x1fffef) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
 Notation "'0b111111111111111110111'" (* 2097143 (0x1ffff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0b111111111111111111110'" (* 2097150 (0x1ffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b111111111111111111111'" (* 2097151 (0x1fffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *)
@@ -939,6 +963,8 @@ Notation "'0b11111111111111110001011'" (* 8388491 (0x7fff8b) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
 Notation "'0b11111111111111111001110'" (* 8388558 (0x7fffce) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b11111111111111111011110'" (* 8388574 (0x7fffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0b11111111111111111100001'" (* 8388577 (0x7fffe1) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
 Notation "'0b11111111111111111100101'" (* 8388581 (0x7fffe5) *)
@@ -1069,6 +1095,8 @@ Notation "'0b1111111111111111111111001110'" (* 268435406 (0xfffffce) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
 Notation "'0b1111111111111111111111100010'" (* 268435426 (0xfffffe2) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0b1111111111111111111111101110'" (* 268435438 (0xfffffee) *)
+  := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
 Notation "'0b1111111111111111111111110001'" (* 268435441 (0xffffff1) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
 Notation "'0b1111111111111111111111110101'" (* 268435445 (0xffffff5) *)
@@ -1115,6 +1143,8 @@ Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111110111111111111111'" (* 1073709055 (0x3fff7fff) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b111111111111111111111111011010'" (* 1073741786 (0x3fffffda) *)
+  := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b111111111111111111111111110110'" (* 1073741814 (0x3ffffff6) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
 Notation "'0b111111111111111111111111111010'" (* 1073741818 (0x3ffffffa) *)
@@ -1429,6 +1459,8 @@ Notation "'0b10000000000000000000000000000000000000000000001'" (* 70368744177665
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b11111111111111111111110111111111111111111111110'" (* 140737471578110 (0x7ffffefffffe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111011110'" (* 140737488355294 (0x7fffffffffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111100111'" (* 140737488355303 (0x7fffffffffe7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
 Notation "'0b11111111111111111111111111111111111111111110001'" (* 140737488355313 (0x7ffffffffff1) *)
@@ -1653,8 +1685,12 @@ Notation "'0b11111111111111110000000000000000000000000000000000000000'" (* 72056
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b11111111111111111111111111111111111111111111111110001011'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0b11111111111111111111111111111111111111111111111111000010'" (* 72057594037927874 (0xffffffffffffc2) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111001110'" (* 72057594037927886 (0xffffffffffffce) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111111111010110'" (* 72057594037927894 (0xffffffffffffd6) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111011010'" (* 72057594037927898 (0xffffffffffffda) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111101111'" (* 72057594037927919 (0xffffffffffffef) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 55878a0cd..807910f7d 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -43,20 +43,26 @@ nums = tuple(sorted(set(systematic_nums + [
     524269,
     524271,
     524279,
+    524286,
     679935,
     1048471,
+    1048526,
+    1048538,
     1048549,
     1048557,
     1048559,
     1048573,
+    1048574,
     2060031,
     2081439,
     2094335,
     2096127,
     2096128,
+    2097118,
     2097127,
     2097135,
     2097143,
+    2097150,
     4193327,
     4193539,
     4193735,
@@ -71,6 +77,7 @@ nums = tuple(sorted(set(systematic_nums + [
     8323583,
     8388491,
     8388558,
+    8388574,
     8388577,
     8388581,
     8388591,
@@ -121,6 +128,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268435398,
     268435406,
     268435426,
+    268435438,
     268435441,
     268435445,
     268435452,
@@ -138,6 +146,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1054736383,
     1065418751,
     1073709055,
+    1073741786,
     1073741814,
     1073741818,
     1073741821,
@@ -245,6 +254,7 @@ nums = tuple(sorted(set(systematic_nums + [
     70368744177659,
     70368744177661,
     140737471578110,
+    140737488355294,
     140737488355303,
     140737488355313,
     140737488355319,
@@ -330,7 +340,9 @@ nums = tuple(sorted(set(systematic_nums + [
     36028797018963966,
     72056494526300160,
     72057594037927819,
+    72057594037927874,
     72057594037927886,
+    72057594037927894,
     72057594037927898,
     72057594037927919,
     72057594037927931,
@@ -1241,6 +1253,10 @@ Notation "'0x7fff7'" (* 524279 (0x7fff7) *)
   := (Const 524279%Z).
 Notation "'0x7fff7'" (* 524279 (0x7fff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0x7fffe'" (* 524286 (0x7fffe) *)
+  := (Const 524286%Z).
+Notation "'0x7fffe'" (* 524286 (0x7fffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0x7ffff'" (* 524287 (0x7ffff) *)
   := (Const 524287%Z).
 Notation "'0x7ffff'" (* 524287 (0x7ffff) *)
@@ -1261,6 +1277,14 @@ Notation "'0xfff97'" (* 1048471 (0xfff97) *)
   := (Const 1048471%Z).
 Notation "'0xfff97'" (* 1048471 (0xfff97) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1).
+Notation "'0xfffce'" (* 1048526 (0xfffce) *)
+  := (Const 1048526%Z).
+Notation "'0xfffce'" (* 1048526 (0xfffce) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0xfffda'" (* 1048538 (0xfffda) *)
+  := (Const 1048538%Z).
+Notation "'0xfffda'" (* 1048538 (0xfffda) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0xfffe5'" (* 1048549 (0xfffe5) *)
   := (Const 1048549%Z).
 Notation "'0xfffe5'" (* 1048549 (0xfffe5) *)
@@ -1277,6 +1301,10 @@ Notation "'0xffffd'" (* 1048573 (0xffffd) *)
   := (Const 1048573%Z).
 Notation "'0xffffd'" (* 1048573 (0xffffd) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0xffffe'" (* 1048574 (0xffffe) *)
+  := (Const 1048574%Z).
+Notation "'0xffffe'" (* 1048574 (0xffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xfffff'" (* 1048575 (0xfffff) *)
   := (Const 1048575%Z).
 Notation "'0xfffff'" (* 1048575 (0xfffff) *)
@@ -1309,6 +1337,10 @@ Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const 2096128%Z).
 Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0x1fffde'" (* 2097118 (0x1fffde) *)
+  := (Const 2097118%Z).
+Notation "'0x1fffde'" (* 2097118 (0x1fffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0x1fffe7'" (* 2097127 (0x1fffe7) *)
   := (Const 2097127%Z).
 Notation "'0x1fffe7'" (* 2097127 (0x1fffe7) *)
@@ -1321,6 +1353,10 @@ Notation "'0x1ffff7'" (* 2097143 (0x1ffff7) *)
   := (Const 2097143%Z).
 Notation "'0x1ffff7'" (* 2097143 (0x1ffff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
+Notation "'0x1ffffe'" (* 2097150 (0x1ffffe) *)
+  := (Const 2097150%Z).
+Notation "'0x1ffffe'" (* 2097150 (0x1ffffe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0x1fffff'" (* 2097151 (0x1fffff) *)
   := (Const 2097151%Z).
 Notation "'0x1fffff'" (* 2097151 (0x1fffff) *)
@@ -1401,6 +1437,10 @@ Notation "'0x7fffce'" (* 8388558 (0x7fffce) *)
   := (Const 8388558%Z).
 Notation "'0x7fffce'" (* 8388558 (0x7fffce) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0x7fffde'" (* 8388574 (0x7fffde) *)
+  := (Const 8388574%Z).
+Notation "'0x7fffde'" (* 8388574 (0x7fffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0x7fffe1'" (* 8388577 (0x7fffe1) *)
   := (Const 8388577%Z).
 Notation "'0x7fffe1'" (* 8388577 (0x7fffe1) *)
@@ -1661,6 +1701,10 @@ Notation "'0xfffffe2'" (* 268435426 (0xfffffe2) *)
   := (Const 268435426%Z).
 Notation "'0xfffffe2'" (* 268435426 (0xfffffe2) *)
   := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0xfffffee'" (* 268435438 (0xfffffee) *)
+  := (Const 268435438%Z).
+Notation "'0xfffffee'" (* 268435438 (0xfffffee) *)
+  := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
 Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
   := (Const 268435441%Z).
 Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
@@ -1753,6 +1797,10 @@ Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
   := (Const 1073709055%Z).
 Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
   := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x3fffffda'" (* 1073741786 (0x3fffffda) *)
+  := (Const 1073741786%Z).
+Notation "'0x3fffffda'" (* 1073741786 (0x3fffffda) *)
+  := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
 Notation "'0x3ffffff6'" (* 1073741814 (0x3ffffff6) *)
   := (Const 1073741814%Z).
 Notation "'0x3ffffff6'" (* 1073741814 (0x3ffffff6) *)
@@ -2381,6 +2429,10 @@ Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
   := (Const 140737471578110%Z).
 Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0x7fffffffffde'" (* 140737488355294 (0x7fffffffffde) *)
+  := (Const 140737488355294%Z).
+Notation "'0x7fffffffffde'" (* 140737488355294 (0x7fffffffffde) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
 Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
   := (Const 140737488355303%Z).
 Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
@@ -2829,10 +2881,18 @@ Notation "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (Const 72057594037927819%Z).
 Notation "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0xffffffffffffc2'" (* 72057594037927874 (0xffffffffffffc2) *)
+  := (Const 72057594037927874%Z).
+Notation "'0xffffffffffffc2'" (* 72057594037927874 (0xffffffffffffc2) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0).
 Notation "'0xffffffffffffce'" (* 72057594037927886 (0xffffffffffffce) *)
   := (Const 72057594037927886%Z).
 Notation "'0xffffffffffffce'" (* 72057594037927886 (0xffffffffffffce) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0xffffffffffffd6'" (* 72057594037927894 (0xffffffffffffd6) *)
+  := (Const 72057594037927894%Z).
+Notation "'0xffffffffffffd6'" (* 72057594037927894 (0xffffffffffffd6) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~0).
 Notation "'0xffffffffffffda'" (* 72057594037927898 (0xffffffffffffda) *)
   := (Const 72057594037927898%Z).
 Notation "'0xffffffffffffda'" (* 72057594037927898 (0xffffffffffffda) *)