From 32a71e6eec78fdcc14883f870aa1d20f3bf89cd0 Mon Sep 17 00:00:00 2001
From: Paul Rigge <rigge@google.com>
Date: Fri, 23 Feb 2024 14:03:36 -0800
Subject: [PATCH] Fix canonicalization overflow bug.

A comparison of number of selector cases would fail with a large selector resulting in `1ULL << selector_bit_width` overflowing. Guard the comparison with a check on the selector width.

Also add crashers that found the bug.

PiperOrigin-RevId: 609831159
---
 xls/fuzzer/BUILD                              |   3 +
 xls/fuzzer/crashers/crasher_2023-11-13_cf6f.x |  83 +++++++
 xls/fuzzer/crashers/crasher_2024-02-23_b88e.x | 209 ++++++++++++++++++
 xls/passes/canonicalization_pass.cc           |   9 +-
 xls/passes/canonicalization_pass_test.cc      |  15 ++
 5 files changed, 316 insertions(+), 3 deletions(-)
 create mode 100644 xls/fuzzer/crashers/crasher_2023-11-13_cf6f.x
 create mode 100644 xls/fuzzer/crashers/crasher_2024-02-23_b88e.x

diff --git a/xls/fuzzer/BUILD b/xls/fuzzer/BUILD
index 79c384c9b0..d10287b7b1 100644
--- a/xls/fuzzer/BUILD
+++ b/xls/fuzzer/BUILD
@@ -416,6 +416,9 @@ generate_crasher_regression_tests(
         "crashers/crasher_2023-04-09_1f76.x": [
             "optonly",
         ],
+        "crashers/crasher_2024-02-23_b88e.x": [
+            "optonly",
+        ],
     },
 )
 
diff --git a/xls/fuzzer/crashers/crasher_2023-11-13_cf6f.x b/xls/fuzzer/crashers/crasher_2023-11-13_cf6f.x
new file mode 100644
index 0000000000..2168c26d05
--- /dev/null
+++ b/xls/fuzzer/crashers/crasher_2023-11-13_cf6f.x
@@ -0,0 +1,83 @@
+// Copyright 2023 The XLS Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+// BEGIN_CONFIG
+// sample_options {
+//   input_is_dslx: true
+//   sample_type: SAMPLE_TYPE_FUNCTION
+//   ir_converter_args: "--top=main"
+//   convert_to_ir: true
+//   optimize_ir: true
+//   use_jit: true
+//   codegen: false
+//   simulate: false
+//   use_system_verilog: true
+//   calls_per_sample: 8
+//   proc_ticks: 0
+//   known_failure {
+//     tool: ".*codegen_main"
+//     stderr_regex: ".*Impossible to schedule proc .* as specified; cannot achieve the specified pipeline length.*"
+//   }
+//   known_failure {
+//     tool: ".*codegen_main"
+//     stderr_regex: ".*Impossible to schedule proc .* as specified; cannot achieve full throughput.*"
+//   }
+// }
+// inputs {
+//   function_args {
+//     args: "[bits[15]:0x0, bits[15]:0x17b7, bits[15]:0x5555, bits[15]:0x2aaa, bits[15]:0x3fff, bits[15]:0x3fff, bits[15]:0x5555]; bits[29]:0xaaa_aaaa; bits[43]:0x3ff_ffff_ffff; bits[5]:0x13"
+//     args: "[bits[15]:0x7fff, bits[15]:0x77b3, bits[15]:0x7fff, bits[15]:0x5555, bits[15]:0x7fff, bits[15]:0x3fff, bits[15]:0x7fff]; bits[29]:0x4; bits[43]:0x4045_3f14; bits[5]:0x2"
+//     args: "[bits[15]:0x4000, bits[15]:0x3fff, bits[15]:0x3e6f, bits[15]:0x7fff, bits[15]:0x5555, bits[15]:0x64ee, bits[15]:0x532c]; bits[29]:0x1fff_ffff; bits[43]:0x3ff_ffff_ffff; bits[5]:0x1f"
+//     args: "[bits[15]:0x1de2, bits[15]:0x0, bits[15]:0x5555, bits[15]:0x5555, bits[15]:0x5555, bits[15]:0x5555, bits[15]:0x2aaa]; bits[29]:0xfff_ffff; bits[43]:0x7ff_ffff_ffff; bits[5]:0x8"
+//     args: "[bits[15]:0x2aaa, bits[15]:0x3fff, bits[15]:0x2aaa, bits[15]:0x5555, bits[15]:0x6b6d, bits[15]:0x1000, bits[15]:0x7a43]; bits[29]:0x40_0000; bits[43]:0x0; bits[5]:0x2"
+//     args: "[bits[15]:0x3fff, bits[15]:0x400, bits[15]:0x1482, bits[15]:0x5555, bits[15]:0x7fff, bits[15]:0x7fff, bits[15]:0x3fff]; bits[29]:0x0; bits[43]:0x3ff_ffff_ffff; bits[5]:0x1f"
+//     args: "[bits[15]:0x3fff, bits[15]:0x4000, bits[15]:0x0, bits[15]:0x5555, bits[15]:0x86d, bits[15]:0x2aaa, bits[15]:0x2aaa]; bits[29]:0xfff_ffff; bits[43]:0x2aa_aaaa_aaaa; bits[5]:0x7"
+//     args: "[bits[15]:0x0, bits[15]:0x40, bits[15]:0x8, bits[15]:0x5555, bits[15]:0x2aaa, bits[15]:0x3fff, bits[15]:0x0]; bits[29]:0x4_0000; bits[43]:0x7ff_ffff_ffff; bits[5]:0x10"
+//   }
+// }
+// 
+// END_CONFIG
+type x0 = u15;
+fn main(x1: x0[7], x2: u29, x3: u43, x4: u5) -> (u11, bool, u6, u43, u43, u4) {
+    {
+        let x5: u43 = clz(x3);
+        let x6: bool = x2 as u43 != x5;
+        let x8: u43 = {
+            let x7: (u43, u43) = umulp(x6 as u43, x3);
+            x7.0 + x7.1
+        };
+        let x9: u4 = u4:0x2;
+        let x10: u6 = u6:0x3f;
+        let x11: bool = x6 | x6;
+        let x12: u43 = x8 | x2 as u43;
+        let x13: bool = xor_reduce(x6);
+        let x14: u43 = x12 >> if x9 >= u4:0xe { u4:0xe } else { x9 };
+        let x15: u16 = x8[27+:u16];
+        let x16: x0[9] = slice(x1, x12, x0[9]:[x1[u32:0x0], ...]);
+        let x17: u7 = u7:0x8;
+        let x18: u11 = match x12 {
+            u43:0x3ff_ffff_ffff => u11:0x5b8,
+            u43:0x0 => u11:0x555,
+            _ => u11:0x1,
+        };
+        let x19: u15 = match x14 {
+            u43:0x0 => u15:0x3fff,
+            _ => u15:0x3fff,
+        };
+        let x21: s1 = {
+            let x20: (bool, bool) = smulp(x6 as s1, x3 as bool as s1);
+            (x20.0 + x20.1) as s1
+        };
+        (x18, x6, x10, x8, x8, x9)
+    }
+}
diff --git a/xls/fuzzer/crashers/crasher_2024-02-23_b88e.x b/xls/fuzzer/crashers/crasher_2024-02-23_b88e.x
new file mode 100644
index 0000000000..89571f869a
--- /dev/null
+++ b/xls/fuzzer/crashers/crasher_2024-02-23_b88e.x
@@ -0,0 +1,209 @@
+// Copyright 2024 The XLS Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+// BEGIN_CONFIG
+// sample_options {
+//   input_is_dslx: true
+//   sample_type: SAMPLE_TYPE_FUNCTION
+//   ir_converter_args: "--top=main"
+//   convert_to_ir: true
+//   optimize_ir: true
+//   use_jit: true
+//   codegen: true
+//   codegen_args: "--nouse_system_verilog"
+//   codegen_args: "--generator=pipeline"
+//   codegen_args: "--pipeline_stages=8"
+//   codegen_args: "--reset=rst"
+//   codegen_args: "--reset_active_low=false"
+//   codegen_args: "--reset_asynchronous=false"
+//   codegen_args: "--reset_data_path=false"
+//   codegen_args: "--output_block_ir_path=sample.block.ir"
+//   simulate: true
+//   simulator: "iverilog"
+//   use_system_verilog: false
+//   timeout_seconds: 1500
+//   calls_per_sample: 128
+//   proc_ticks: 0
+//   known_failure {
+//     tool: ".*codegen_main"
+//     stderr_regex: ".*Impossible to schedule proc .* as specified; cannot achieve the specified pipeline length.*"
+//   }
+//   known_failure {
+//     tool: ".*codegen_main"
+//     stderr_regex: ".*Impossible to schedule proc .* as specified; cannot achieve full throughput.*"
+//   }
+// }
+// inputs {
+//   function_args {
+//     args: "bits[15]:0x5555; bits[15]:0x415f; bits[33]:0x10_0000; bits[63]:0x5555_fdff_bfef_ffff; [bits[26]:0xcf_498d, bits[26]:0x155_5555, bits[26]:0x155_5555, bits[26]:0x2aa_aaaa, bits[26]:0x16f_dfed, bits[26]:0x800, bits[26]:0x2aa_aaaa, bits[26]:0x30c_f810, bits[26]:0x2c7_ee75]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0x90ea_03ed_fe9e; bits[9]:0x1ff; bits[21]:0xf_ffff; bits[7]:0x7b"
+//     args: "bits[15]:0x200; bits[15]:0x6cdc; bits[33]:0x1_a65d_3891; bits[63]:0x200_ffff_f7ef_fdfe; [bits[26]:0x98_020a, bits[26]:0x287_ddfe, bits[26]:0x2f0_7c04, bits[26]:0x14f_ddf4, bits[26]:0xac_c56e, bits[26]:0x2aa_aaaa, bits[26]:0x3a7_62da, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0xffff_ffff_ffff; bits[9]:0x1; bits[21]:0x13_892b; bits[7]:0x10"
+//     args: "bits[15]:0x7354; bits[15]:0x13f2; bits[33]:0x0; bits[63]:0x1079_a656_cd59_a2b1; [bits[26]:0x1ff_ffff, bits[26]:0x31b_e042, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x9_0244, bits[26]:0x9d_9376, bits[26]:0x9f_90f8, bits[26]:0x35a_d640]; bits[30]:0x959_a0b9; bits[1]:0x0; bits[49]:0x8b72_f131_2b4e; bits[9]:0x1f9; bits[21]:0x1c_65c5; bits[7]:0x3"
+//     args: "bits[15]:0x613c; bits[15]:0x5555; bits[33]:0x1_ffff_ffff; bits[63]:0x6703_3e77_be46_d47b; [bits[26]:0x63_a000, bits[26]:0x31b_e4a0, bits[26]:0x309_e555, bits[26]:0x400, bits[26]:0xaa_abc7, bits[26]:0x206_d433, bits[26]:0x2aa_abff, bits[26]:0x2e3_d53f, bits[26]:0x1ff_ffff]; bits[30]:0x0; bits[1]:0x1; bits[49]:0xefa0_8ab3_8ee9; bits[9]:0xdc; bits[21]:0xf_ffff; bits[7]:0x0"
+//     args: "bits[15]:0x7d6a; bits[15]:0x800; bits[33]:0x0; bits[63]:0x8_0000_0000; [bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x9_a46f, bits[26]:0x237_f649, bits[26]:0x3fe_a845, bits[26]:0x2aa_aaaa, bits[26]:0x26_9e12, bits[26]:0x28_2051]; bits[30]:0x800; bits[1]:0x1; bits[49]:0xffff_ffff_ffff; bits[9]:0x11a; bits[21]:0x12_a2eb; bits[7]:0x69"
+//     args: "bits[15]:0x100; bits[15]:0x100; bits[33]:0x100_0000; bits[63]:0x4125_5c02_155d_76f4; [bits[26]:0x1ff_ffff, bits[26]:0x8_0088, bits[26]:0x88_0755, bits[26]:0x2aa_aaaa, bits[26]:0x168_482d, bits[26]:0x228_2000, bits[26]:0x154_0010, bits[26]:0x30f_d232, bits[26]:0x161_4402]; bits[30]:0x91_3fb6; bits[1]:0x1; bits[49]:0x480_0000_0002; bits[9]:0x0; bits[21]:0x0; bits[7]:0x3f"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_545d_8000; bits[63]:0x53a1_0e0a_8c02_4ff9; [bits[26]:0x0, bits[26]:0x292_8016, bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x10e_8f72, bits[26]:0x155_5555, bits[26]:0x2_8df9, bits[26]:0x24a_aca0, bits[26]:0x0]; bits[30]:0x2188_c1ce; bits[1]:0x1; bits[49]:0x4ff1_34bf_74c3; bits[9]:0x1d2; bits[21]:0x15_5555; bits[7]:0x14"
+//     args: "bits[15]:0x2aaa; bits[15]:0x2b8a; bits[33]:0xffff_ffff; bits[63]:0x3bff_effe_b406_a3cd; [bits[26]:0x155_5555, bits[26]:0x1ff_ffff, bits[26]:0x37f_ecfd, bits[26]:0x15c_c7fc, bits[26]:0x1ff_ffff, bits[26]:0x55_43fd, bits[26]:0x58_c961, bits[26]:0x400, bits[26]:0x15c_5555]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0x5002_0004_0540; bits[9]:0x155; bits[21]:0x4_0542; bits[7]:0x5f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x5937; bits[33]:0x4cb9_1538; bits[63]:0x2baa_7ff6_bfff_ffff; [bits[26]:0x1_0000, bits[26]:0x289_0d79, bits[26]:0x2cd_3927, bits[26]:0x259_9130, bits[26]:0x2f8_c7b1, bits[26]:0x10, bits[26]:0xba_8d7f, bits[26]:0x95_e687, bits[26]:0x118_41d9]; bits[30]:0x1996_5190; bits[1]:0x0; bits[49]:0x1_ab4e_1ab8_9030; bits[9]:0xaa; bits[21]:0x0; bits[7]:0x30"
+//     args: "bits[15]:0x7fff; bits[15]:0x7fff; bits[33]:0x1_5555_5555; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x155_75a4, bits[26]:0x177_8615, bits[26]:0x1ff_fd5d, bits[26]:0x23b_f4ee, bits[26]:0x151_5555, bits[26]:0x41_c559, bits[26]:0x1ff_ffff, bits[26]:0x2cb_7fe8, bits[26]:0x14f_5d4d]; bits[30]:0x2aaa_aaaa; bits[1]:0x0; bits[49]:0xee49_99bf_bf9a; bits[9]:0xdf; bits[21]:0x11_6ee9; bits[7]:0x45"
+//     args: "bits[15]:0x3eb8; bits[15]:0x7fff; bits[33]:0x1_ffff_ffff; bits[63]:0x40_0000_0000; [bits[26]:0x16e_67ee, bits[26]:0x1000, bits[26]:0x0, bits[26]:0x3ff_fd55, bits[26]:0x0, bits[26]:0x155_5555, bits[26]:0x0, bits[26]:0xff_ee2a, bits[26]:0x40_0000]; bits[30]:0x3f5c_3f7d; bits[1]:0x0; bits[49]:0x1_fcfb_ffff_f555; bits[9]:0x153; bits[21]:0xf_ae32; bits[7]:0x3f"
+//     args: "bits[15]:0x7fca; bits[15]:0x7175; bits[33]:0x1_ef20_6058; bits[63]:0x3b18_1f17_fd5f_67ff; [bits[26]:0x2fc_9530, bits[26]:0x3ff_ffff, bits[26]:0x140_2569, bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x3ff_ffff, bits[26]:0x1c1_51c4, bits[26]:0x1f_67df, bits[26]:0x155_059e]; bits[30]:0x3d35_6ffa; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0xff; bits[21]:0xf_4fdc; bits[7]:0x55"
+//     args: "bits[15]:0x3fff; bits[15]:0x3fff; bits[33]:0x1_7daf_d82c; bits[63]:0x37c3_9528_808a_0a02; [bits[26]:0x1db_fadc, bits[26]:0x2aa_aaaa, bits[26]:0x2aa_aaaa, bits[26]:0x3cb_d70a, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x4, bits[26]:0x45_de08, bits[26]:0x155_5555]; bits[30]:0x1fff_ffff; bits[1]:0x1; bits[49]:0x418d_c2cd_ea65; bits[9]:0x2; bits[21]:0x0; bits[7]:0xb"
+//     args: "bits[15]:0x3fff; bits[15]:0x3fff; bits[33]:0xffff_ffff; bits[63]:0x0; [bits[26]:0x1fb_cdf7, bits[26]:0x1f7_aa34, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x260_e002, bits[26]:0x1ff_ffff, bits[26]:0x4_0224, bits[26]:0x1ff_ffff, bits[26]:0x2ff_fbca]; bits[30]:0x15bf_83be; bits[1]:0x1; bits[49]:0x4400_4004_1004; bits[9]:0x1ff; bits[21]:0x0; bits[7]:0x7e"
+//     args: "bits[15]:0x5555; bits[15]:0x3fff; bits[33]:0xfdfe_aaab; bits[63]:0x3797_aeeb_bad0_51d4; [bits[26]:0x252_d1d4, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_f546, bits[26]:0xcb_e902, bits[26]:0x2b8_80f6, bits[26]:0x2d0_d1d4, bits[26]:0x3ff_ffff, bits[26]:0x1000, bits[26]:0xff_e7ff]; bits[30]:0x3bd0_51d4; bits[1]:0x1; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0xff; bits[21]:0xa_aaaa; bits[7]:0x7f"
+//     args: "bits[15]:0x4; bits[15]:0x288; bits[33]:0x0; bits[63]:0x0; [bits[26]:0x25_402a, bits[26]:0x13a_1e00, bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x10_a01c, bits[26]:0x33d_4589, bits[26]:0x4_0014, bits[26]:0x104_4000, bits[26]:0x286_2455]; bits[30]:0x2000_0000; bits[1]:0x1; bits[49]:0xb003_4039_99ff; bits[9]:0x1ff; bits[21]:0xa_aaaa; bits[7]:0x5f"
+//     args: "bits[15]:0x17ba; bits[15]:0x152e; bits[33]:0x1_1dba_df4f; bits[63]:0x4000_0000; [bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x10e_2004, bits[26]:0xbd_d180, bits[26]:0x1b7_ffa6, bits[26]:0xb_5b6f, bits[26]:0x3db_ebc0]; bits[30]:0x1b9b_b255; bits[1]:0x1; bits[49]:0x1_9db0_1515_4ff4; bits[9]:0x1ff; bits[21]:0x1f_ffff; bits[7]:0x54"
+//     args: "bits[15]:0x3d4d; bits[15]:0x3d4f; bits[33]:0xf537_ffff; bits[63]:0x40; [bits[26]:0x135_f75f, bits[26]:0x40, bits[26]:0x800, bits[26]:0x10_0240, bits[26]:0x336_f803, bits[26]:0x3eb_5fff, bits[26]:0x4_2442, bits[26]:0x133_b7ff, bits[26]:0x104_ffe1]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0x8420_0000_0000; bits[9]:0x1ff; bits[21]:0x12_2966; bits[7]:0x2a"
+//     args: "bits[15]:0x4d39; bits[15]:0x4f39; bits[33]:0x1_34e7_edff; bits[63]:0x1db3_c4e3_55c0_2b6b; [bits[26]:0x0, bits[26]:0x15c_0cf0, bits[26]:0x155_5555, bits[26]:0x100_1a35, bits[26]:0x100, bits[26]:0x27b_9c04, bits[26]:0x3c2_c36b, bits[26]:0x279_caaa, bits[26]:0x263_cbfb]; bits[30]:0x19f_0bd1; bits[1]:0x1; bits[49]:0xf5d1_5728_1133; bits[9]:0xaa; bits[21]:0xab6b; bits[7]:0x2a"
+//     args: "bits[15]:0x0; bits[15]:0x51b8; bits[33]:0x1_ffff_ffff; bits[63]:0x51b9_7fff_bffb_dfff; [bits[26]:0x1f0_0d45, bits[26]:0x23b_c173, bits[26]:0x2_0000, bits[26]:0x155_5555, bits[26]:0x1ff_ffff, bits[26]:0x61_210b, bits[26]:0x3f1_dcc7, bits[26]:0x10_0200, bits[26]:0x155_5555]; bits[30]:0x3ffb_dfff; bits[1]:0x0; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0x0; bits[21]:0x1_47fe; bits[7]:0x2a"
+//     args: "bits[15]:0x5555; bits[15]:0x2aaa; bits[33]:0xaaab_fdfe; bits[63]:0x2a7b_fd5f_ab2a_a09b; [bits[26]:0x3bc_598f, bits[26]:0x32a_a09b, bits[26]:0x0, bits[26]:0x5_7788, bits[26]:0x2ba_ddde, bits[26]:0x3ae_acf2, bits[26]:0x31a_249b, bits[26]:0x3ff_ffff, bits[26]:0x23a_ae14]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x1_aae9_52be_c147; bits[9]:0x155; bits[21]:0xf_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x0; bits[15]:0x0; bits[33]:0x1_5527_93f7; bits[63]:0x4888_9bc6_5b4a_1481; [bits[26]:0x35b_1c0a, bits[26]:0x349_0cc5, bits[26]:0x1ff_ffff, bits[26]:0x239_13f6, bits[26]:0x2aa_aaaa, bits[26]:0x100_0000, bits[26]:0x190_04db, bits[26]:0xc1_6911, bits[26]:0x20_0808]; bits[30]:0x303a_d242; bits[1]:0x1; bits[49]:0x400_0000_0000; bits[9]:0xff; bits[21]:0xe_7604; bits[7]:0x20"
+//     args: "bits[15]:0x200; bits[15]:0x4440; bits[33]:0x8000; bits[63]:0x80; [bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x68_2098, bits[26]:0x20_1c0d, bits[26]:0x1002, bits[26]:0x2aa_03fe, bits[26]:0x1fa_64b8, bits[26]:0x1, bits[26]:0x230_2284]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x0; bits[9]:0x1b7; bits[21]:0x1f_ffff; bits[7]:0x2a"
+//     args: "bits[15]:0x7fff; bits[15]:0x61ad; bits[33]:0x1_ffff_ffff; bits[63]:0x60ac_08d0_4200_0280; [bits[26]:0x2aa_aaaa, bits[26]:0x3a7_bdc7, bits[26]:0x3ff_ffff, bits[26]:0x27f_fd91, bits[26]:0x335_6c9a, bits[26]:0x3ff_f800, bits[26]:0x3e9_6850, bits[26]:0x1_0000, bits[26]:0x28b_2c02]; bits[30]:0x3fff_bfff; bits[1]:0x1; bits[49]:0x4000_0000_0000; bits[9]:0x1f5; bits[21]:0x1f_ffff; bits[7]:0x77"
+//     args: "bits[15]:0x4045; bits[15]:0x400; bits[33]:0xaaaa_aaaa; bits[63]:0x6944_9fda_7ff5_2e56; [bits[26]:0x1ce_ca6f, bits[26]:0x3f5_2e56, bits[26]:0x3f9_ae5e, bits[26]:0x2aa_aaaa, bits[26]:0x20b_6831, bits[26]:0x0, bits[26]:0x375_2e57, bits[26]:0x32b_b8a8, bits[26]:0x3f4_2e1e]; bits[30]:0x200_0004; bits[1]:0x1; bits[49]:0x800_8022_aaea; bits[9]:0x0; bits[21]:0x15_5555; bits[7]:0x24"
+//     args: "bits[15]:0x3fff; bits[15]:0x0; bits[33]:0x1_ffff_ffff; bits[63]:0x5abf_0106_efd4_cc35; [bits[26]:0x3ff_ffff, bits[26]:0xaa_0218, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x3e3_37cb, bits[26]:0x3d0_b76e, bits[26]:0x0, bits[26]:0x1fd_ef45, bits[26]:0x3d4_cc35]; bits[30]:0x1ca7_431f; bits[1]:0x0; bits[49]:0x1_c083_8f07_0a86; bits[9]:0x1a; bits[21]:0x11_0c11; bits[7]:0x2a"
+//     args: "bits[15]:0x7fff; bits[15]:0x2b27; bits[33]:0xe41e_42ad; bits[63]:0x6bf5_bc7f_1f8e_f861; [bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x18a_7875, bits[26]:0x155_5555, bits[26]:0x5c_45e7, bits[26]:0x182_b8e5, bits[26]:0xa6_6b04, bits[26]:0x16_42ad, bits[26]:0x3ff_ffff]; bits[30]:0x9e1_b050; bits[1]:0x1; bits[49]:0x0; bits[9]:0x61; bits[21]:0x13_ff9b; bits[7]:0x21"
+//     args: "bits[15]:0x8; bits[15]:0xada; bits[33]:0xf6b_3eee; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x0, bits[26]:0x57_d77f, bits[26]:0x36f_01a7, bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x233_8e3e, bits[26]:0x1ba_0b16, bits[26]:0x155_5555, bits[26]:0x3ff_ffff]; bits[30]:0x19ce_4303; bits[1]:0x1; bits[49]:0x1_bede_526f_bf3f; bits[9]:0x1a; bits[21]:0x15_5555; bits[7]:0x54"
+//     args: "bits[15]:0x3fff; bits[15]:0x5555; bits[33]:0xa36_2102; bits[63]:0x800; [bits[26]:0x2aa_aaaa, bits[26]:0xca_c159, bits[26]:0x57_da4c, bits[26]:0x0, bits[26]:0xba_a818, bits[26]:0x17e_76b4, bits[26]:0x1ff_fbf3, bits[26]:0x233_6d03, bits[26]:0x3e3_7d76]; bits[30]:0x1fff_889c; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x4; bits[21]:0x8_f3a8; bits[7]:0x44"
+//     args: "bits[15]:0x5555; bits[15]:0x47d5; bits[33]:0x1_5564_5555; bits[63]:0x800_0000_0000; [bits[26]:0x174_b59e, bits[26]:0x3ce_4dc6, bits[26]:0x2fd_569b, bits[26]:0x2aa_a2a2, bits[26]:0x2ea_b74d, bits[26]:0x2ea_bc21, bits[26]:0x20_0000, bits[26]:0x118_a36b, bits[26]:0x364_dd14]; bits[30]:0x2aaa_8040; bits[1]:0x0; bits[49]:0x0; bits[9]:0xff; bits[21]:0x1aa; bits[7]:0x3f"
+//     args: "bits[15]:0x20; bits[15]:0x80; bits[33]:0x89a0_1626; bits[63]:0x1744_ef78_ee84_b94c; [bits[26]:0x1b0_2467, bits[26]:0x44_0555, bits[26]:0x280_ad44, bits[26]:0x11e_9d23, bits[26]:0x48_0ff5, bits[26]:0x71_00ba, bits[26]:0x109_531a, bits[26]:0x155_5555, bits[26]:0x255_a9dc]; bits[30]:0x7fa_9c67; bits[1]:0x0; bits[49]:0x63d8_3f3a_1849; bits[9]:0x1ff; bits[21]:0x1f_ffff; bits[7]:0x0"
+//     args: "bits[15]:0x3fff; bits[15]:0x5555; bits[33]:0x0; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x2aa_aaaa, bits[26]:0x15_b111, bits[26]:0x2aa_aaaa, bits[26]:0x2aa_aaaa, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x2aa_e800, bits[26]:0xfe_aa1e]; bits[30]:0x95b_bec6; bits[1]:0x1; bits[49]:0x8c70_c0fa_06a1; bits[9]:0x1ff; bits[21]:0x0; bits[7]:0x1"
+//     args: "bits[15]:0x7fff; bits[15]:0x57e7; bits[33]:0x1_5f9c_0500; bits[63]:0x5e7_0940_0101_b4cf; [bits[26]:0x51_7c0e, bits[26]:0x0, bits[26]:0x2af_2e43, bits[26]:0x0, bits[26]:0x155_5555, bits[26]:0x20, bits[26]:0x80_0000, bits[26]:0x288_1105, bits[26]:0x101_b0cf]; bits[30]:0x1f9c_0500; bits[1]:0x1; bits[49]:0xde1d_2042_2010; bits[9]:0x1ff; bits[21]:0x1f_ffff; bits[7]:0x7f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x2aaa; bits[33]:0xffff_ffff; bits[63]:0xddc_0bb2_0d49_a981; [bits[26]:0x16c_6ac0, bits[26]:0x2aa_aaaa, bits[26]:0x800, bits[26]:0x20_0000, bits[26]:0x3ff_ffff, bits[26]:0x206_0b9a, bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0xad_1950]; bits[30]:0x3fff_ffff; bits[1]:0x0; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0x10; bits[21]:0x1_4e36; bits[7]:0x1"
+//     args: "bits[15]:0x2aaa; bits[15]:0x5ac; bits[33]:0x0; bits[63]:0x6d93_01c0_e00b_e9e9; [bits[26]:0x0, bits[26]:0x1a0_6fda, bits[26]:0x9b_ef6b, bits[26]:0x0, bits[26]:0x100, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x5_380f, bits[26]:0x155_5555]; bits[30]:0x26b6_ad7f; bits[1]:0x1; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x109; bits[21]:0x16_2d7f; bits[7]:0x9"
+//     args: "bits[15]:0x3fff; bits[15]:0x3f55; bits[33]:0xfd55_efbf; bits[63]:0x40_0000_0000; [bits[26]:0x245_a3f9, bits[26]:0x1b4_e24e, bits[26]:0x1ff_ffff, bits[26]:0x155_63df, bits[26]:0x155_5555, bits[26]:0xf3_2be3, bits[26]:0x2000, bits[26]:0xc9_b4f5, bits[26]:0x92_24d1]; bits[30]:0x3d55_efbf; bits[1]:0x1; bits[49]:0xe577_e7ad_7fdf; bits[9]:0x1a8; bits[21]:0x0; bits[7]:0x37"
+//     args: "bits[15]:0x0; bits[15]:0x304d; bits[33]:0xb401_0c20; bits[63]:0x7fff_ffff_ffff; [bits[26]:0x100_02aa, bits[26]:0x20, bits[26]:0x1a2_4d41, bits[26]:0x2aa_aaaa, bits[26]:0x43_9e10, bits[26]:0x2aa_aaaa, bits[26]:0x3ff_ffff, bits[26]:0x1fa_5b2b, bits[26]:0x2ae_6dff]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0x1_11f0_0a08_11eb; bits[9]:0x20; bits[21]:0x1f_ffff; bits[7]:0x6a"
+//     args: "bits[15]:0x3fff; bits[15]:0x177d; bits[33]:0x8_0000; bits[63]:0x7fcf_3f57_4ac5_912e; [bits[26]:0x1_1b05, bits[26]:0x11a_0000, bits[26]:0x3ff_ffff, bits[26]:0x2c4_b13e, bits[26]:0x19d_d89f, bits[26]:0x155_5555, bits[26]:0x2, bits[26]:0x8_0500, bits[26]:0xfc_4499]; bits[30]:0x4b1_4c48; bits[1]:0x0; bits[49]:0x1_280b_11d4_6a80; bits[9]:0xaa; bits[21]:0x18_0e17; bits[7]:0x2a"
+//     args: "bits[15]:0x3fff; bits[15]:0x3bfb; bits[33]:0x0; bits[63]:0x2fc3_0183_2191_2665; [bits[26]:0x191_2ef4, bits[26]:0x7_a0a2, bits[26]:0x3ff_ffff, bits[26]:0x155_dcfd, bits[26]:0x3ff_ffff, bits[26]:0x1e4_d5c5, bits[26]:0x3ff_ffff, bits[26]:0x19f_9c0d, bits[26]:0x80_0020]; bits[30]:0x15bd_d17d; bits[1]:0x0; bits[49]:0x0; bits[9]:0x0; bits[21]:0x1e_5375; bits[7]:0x2a"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_d554_0022; bits[63]:0x7437_4100_c935_5332; [bits[26]:0x114_a271, bits[26]:0x38a_b883, bits[26]:0x114_5330, bits[26]:0x2aa_aaaa, bits[26]:0x15c_8a22, bits[26]:0x2aa_aaab, bits[26]:0x135_5332, bits[26]:0x179_5449, bits[26]:0x2aa_aaaa]; bits[30]:0x3fff_ffff; bits[1]:0x1; bits[49]:0x0; bits[9]:0xff; bits[21]:0x15_5555; bits[7]:0x52"
+//     args: "bits[15]:0x0; bits[15]:0x0; bits[33]:0x800; bits[63]:0x66c0_0f08_d9af_6a82; [bits[26]:0x0, bits[26]:0x40_4b75, bits[26]:0x155_5555, bits[26]:0x2aa_aaaa, bits[26]:0x8085, bits[26]:0x895, bits[26]:0x5_5041, bits[26]:0x280_9228, bits[26]:0x1ef_6b82]; bits[30]:0x3fff_ffff; bits[1]:0x1; bits[49]:0x1_0060_8423_1020; bits[9]:0x100; bits[21]:0x100; bits[7]:0x4"
+//     args: "bits[15]:0x2aaa; bits[15]:0x3fff; bits[33]:0xaa89_5555; bits[63]:0x100; [bits[26]:0xad_6255, bits[26]:0x155_5555, bits[26]:0x1d5_d2ae, bits[26]:0x0, bits[26]:0x0, bits[26]:0x1fe_4d18, bits[26]:0x155_5555, bits[26]:0x1ff_ffff, bits[26]:0xb7_1263]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0xfdee_080a_0002; bits[9]:0x5c; bits[21]:0x0; bits[7]:0x3f"
+//     args: "bits[15]:0x2aaa; bits[15]:0xbaa; bits[33]:0x400; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x5d_9191, bits[26]:0x119_409c, bits[26]:0x3ff_ffff, bits[26]:0x155_5594, bits[26]:0x3ff_ffff, bits[26]:0x157_5551, bits[26]:0x13_9a74, bits[26]:0x0, bits[26]:0x400]; bits[30]:0x1518_1ca2; bits[1]:0x0; bits[49]:0x1602_0324_18e1; bits[9]:0x110; bits[21]:0xa_aaaa; bits[7]:0x6a"
+//     args: "bits[15]:0x3fff; bits[15]:0x5555; bits[33]:0x4c52_17d5; bits[63]:0x2c3a_67b7_f9f7_efed; [bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x160_f157, bits[26]:0x0, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x10_0000, bits[26]:0x42_4ecf, bits[26]:0x1ff_fc00]; bits[30]:0x0; bits[1]:0x0; bits[49]:0x1_1bb0_6358_ff86; bits[9]:0x186; bits[21]:0x18_2d40; bits[7]:0x7e"
+//     args: "bits[15]:0x5a8a; bits[15]:0x0; bits[33]:0x0; bits[63]:0x800_0000_0000_0000; [bits[26]:0x304_d208, bits[26]:0x50_fdc1, bits[26]:0x14_45ff, bits[26]:0x155_5555, bits[26]:0x204_d079, bits[26]:0x155_5555, bits[26]:0x3dc_5545, bits[26]:0x2c4_555d, bits[26]:0x0]; bits[30]:0x4; bits[1]:0x0; bits[49]:0x8000_0020_0000; bits[9]:0x100; bits[21]:0x1f_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x5555; bits[33]:0x3544_a402; bits[63]:0x23ea_77ff_7ca7_d59b; [bits[26]:0x4000, bits[26]:0x144_f400, bits[26]:0x155_53fe, bits[26]:0x155_5555, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x29a_8afb, bits[26]:0x48_425d, bits[26]:0x155_5555]; bits[30]:0x3ae9_33a8; bits[1]:0x0; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0x2; bits[21]:0xf_ffff; bits[7]:0x2a"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_5555_fbff; bits[63]:0x1_0000_0000_0000; [bits[26]:0x1f4_6791, bits[26]:0x0, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x155_5555]; bits[30]:0x2928_8c7c; bits[1]:0x0; bits[49]:0x541a_f66c_eec2; bits[9]:0x155; bits[21]:0x1d_3f1c; bits[7]:0x55"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_7d72_72e1; bits[63]:0x5559_d082_2191_6386; [bits[26]:0x4b_6384, bits[26]:0x288_2a3a, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x2d4_2806, bits[26]:0x17a_bd2e, bits[26]:0x1, bits[26]:0xaa_8bdb, bits[26]:0x191_e382]; bits[30]:0x3d32_70e1; bits[1]:0x1; bits[49]:0xffff_ffff_ffff; bits[9]:0x186; bits[21]:0x12_52f5; bits[7]:0x51"
+//     args: "bits[15]:0x3d3e; bits[15]:0x0; bits[33]:0x1_04fe_4ace; bits[63]:0x400_e8c9_f787_c297; [bits[26]:0x38d_a293, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x1e9_f38d, bits[26]:0x1e9_f6ff, bits[26]:0x155_5555, bits[26]:0x40_0000, bits[26]:0xef_69ca, bits[26]:0xe5_ff4c]; bits[30]:0xaf3_4be3; bits[1]:0x0; bits[49]:0x100_0000_0000; bits[9]:0x1e7; bits[21]:0x15_5555; bits[7]:0x28"
+//     args: "bits[15]:0x0; bits[15]:0x2aaa; bits[33]:0x1_ffff_ffff; bits[63]:0x2aaa_aaaa_aaaa_aaaa; [bits[26]:0x3ff_feff, bits[26]:0x2ae_e228, bits[26]:0x3dc_9c9f, bits[26]:0x3ff_ffff, bits[26]:0x0, bits[26]:0x3ff_ebdf, bits[26]:0x1ff_ffff, bits[26]:0x365_b838, bits[26]:0x2df_7dbb]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0xffff_ffff_ffff; bits[9]:0xaa; bits[21]:0xf_ffff; bits[7]:0x0"
+//     args: "bits[15]:0x7fff; bits[15]:0x52f9; bits[33]:0x1_0f13_afe1; bits[63]:0x7ffd_fbdf_6b7d_f7bf; [bits[26]:0x2d7_c309, bits[26]:0x3ff_dfff, bits[26]:0x36f_f238, bits[26]:0x1ff_ffff, bits[26]:0x1e_e840, bits[26]:0x339_7f3f, bits[26]:0x1ff_ffff, bits[26]:0x13_2fa1, bits[26]:0x37d_f7bf]; bits[30]:0xbe8_b425; bits[1]:0x0; bits[49]:0xffff_ffff_ffff; bits[9]:0xda; bits[21]:0xf_ffff; bits[7]:0x55"
+//     args: "bits[15]:0x0; bits[15]:0x2000; bits[33]:0x12_aaaa; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x3df_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x16a_f387, bits[26]:0x3ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x33e_ffc6, bits[26]:0x203_4c1d, bits[26]:0x101_05c5, bits[26]:0x11d_0aab]; bits[30]:0x2_08c8; bits[1]:0x0; bits[49]:0x9937_4187_1f3b; bits[9]:0x16a; bits[21]:0x0; bits[7]:0x48"
+//     args: "bits[15]:0x0; bits[15]:0x7fff; bits[33]:0x1_bbf8_0600; bits[63]:0x7b4e_5d43_cd44_6d2f; [bits[26]:0x2aa, bits[26]:0xa7_fc83, bits[26]:0x1ff_ffff, bits[26]:0x55_256f, bits[26]:0x9f_3a95, bits[26]:0x155_5555, bits[26]:0x168_4990, bits[26]:0x231_2003, bits[26]:0x8e_4002]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x2aba_aa8a_ffff; bits[9]:0x108; bits[21]:0x6_6a56; bits[7]:0x48"
+//     args: "bits[15]:0x0; bits[15]:0x1126; bits[33]:0x0; bits[63]:0x40_0000; [bits[26]:0x299_75f3, bits[26]:0x400, bits[26]:0x155_5555, bits[26]:0x201_0401, bits[26]:0x309_6534, bits[26]:0x89_355d, bits[26]:0x3b_8282, bits[26]:0x155_5555, bits[26]:0x89_33fd]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0x1_8c50_005a_dd2d; bits[9]:0x1fd; bits[21]:0x1e_c88a; bits[7]:0x7c"
+//     args: "bits[15]:0x3987; bits[15]:0x3fff; bits[33]:0xc69b_4995; bits[63]:0x3907_7fbf_ffff_fbbf; [bits[26]:0x22f_adaf, bits[26]:0x155_5555, bits[26]:0x1cc_2eaa, bits[26]:0x1ff_ffff, bits[26]:0x18e_0706, bits[26]:0x155_5555, bits[26]:0x1cc_3bff, bits[26]:0x3d6_bb1f, bits[26]:0x3b5_13b3]; bits[30]:0x2aaa_aaaa; bits[1]:0x0; bits[49]:0x1_ec1f_922a_aeaa; bits[9]:0x19a; bits[21]:0x15_5555; bits[7]:0x10"
+//     args: "bits[15]:0x39c2; bits[15]:0x3bc2; bits[33]:0x0; bits[63]:0x38c2_017e_959b_7416; [bits[26]:0x1ce_13ff, bits[26]:0x155_5555, bits[26]:0x2aa_aaaa, bits[26]:0x4b_45ef, bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x0, bits[26]:0x19e_573f, bits[26]:0x19b_7016]; bits[30]:0x2180_4214; bits[1]:0x0; bits[49]:0x1_0c42_90b0_8abe; bits[9]:0x1f0; bits[21]:0xa_aaaa; bits[7]:0x70"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0xaaaa_aaaa; bits[63]:0x1600_794b_9c19_1b9d; [bits[26]:0x155_5555, bits[26]:0x58_5f9c, bits[26]:0x332_aaa2, bits[26]:0x100_0000, bits[26]:0x391_c5c5, bits[26]:0x2aa_aaaa, bits[26]:0x2aa_afff, bits[26]:0x1ab_bf2b, bits[26]:0xbb_2d75]; bits[30]:0x3faa_a0fd; bits[1]:0x1; bits[49]:0x1_4530_7103_7413; bits[9]:0xff; bits[21]:0x7_28f9; bits[7]:0x0"
+//     args: "bits[15]:0x5d8; bits[15]:0x4d6; bits[33]:0xaaaa_aaaa; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x0, bits[26]:0x22e_d4d5, bits[26]:0x26_b401, bits[26]:0x2aa_aaaa, bits[26]:0x16b_1437, bits[26]:0x1ff_ffff, bits[26]:0x155_5555, bits[26]:0xe2_2ac3, bits[26]:0x155_5555]; bits[30]:0x10_0000; bits[1]:0x0; bits[49]:0x1_501d_5555_5555; bits[9]:0xaa; bits[21]:0xf_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x2aaa; bits[33]:0x8d83_3215; bits[63]:0x0; [bits[26]:0x1ff_ffff, bits[26]:0x155_5555, bits[26]:0x100, bits[26]:0x0, bits[26]:0x392_502a, bits[26]:0x155_1f06, bits[26]:0x10_4003, bits[26]:0x13f_6a8a, bits[26]:0x155_5555]; bits[30]:0x929_36bc; bits[1]:0x0; bits[49]:0x2670_8f2e_a013; bits[9]:0xaa; bits[21]:0x4_0000; bits[7]:0x55"
+//     args: "bits[15]:0x400; bits[15]:0x7fff; bits[33]:0x10_0000; bits[63]:0x70bd_6652_96a4_b421; [bits[26]:0x3d3_8110, bits[26]:0x2aa_aaaa, bits[26]:0x800, bits[26]:0x1ff_ffff, bits[26]:0x20_4014, bits[26]:0x89_ed51, bits[26]:0x210_0080, bits[26]:0x3ff_dee2, bits[26]:0xa0_0100]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0x800; bits[9]:0x0; bits[21]:0x5_b405; bits[7]:0x0"
+//     args: "bits[15]:0x2aaa; bits[15]:0x28aa; bits[33]:0xa2a8_0010; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x2aa_aaaa, bits[26]:0x1db_3f7f, bits[26]:0x3ff_ffff, bits[26]:0x1ca_6063, bits[26]:0x155_5bfb, bits[26]:0x3ff_fffb, bits[26]:0x8, bits[26]:0x38a_2093, bits[26]:0x2aa_aaaa]; bits[30]:0x22ac_1070; bits[1]:0x0; bits[49]:0xa2a9_0010_7fff; bits[9]:0x1ff; bits[21]:0x1f_f515; bits[7]:0x4f"
+//     args: "bits[15]:0x7603; bits[15]:0x341c; bits[33]:0xaaaa_aaaa; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x17e_920d, bits[26]:0x3ff_ffff, bits[26]:0x100_0000, bits[26]:0xa3_ee64, bits[26]:0x2ab_abaa, bits[26]:0x8000, bits[26]:0x394_86f3, bits[26]:0x3ff_ffff, bits[26]:0x3ee_3504]; bits[30]:0x2a2b_8aab; bits[1]:0x1; bits[49]:0x0; bits[9]:0x142; bits[21]:0x1_0000; bits[7]:0xf"
+//     args: "bits[15]:0x7fff; bits[15]:0x2aaa; bits[33]:0x1_ffbb_6b66; bits[63]:0x6df4_5a9b_9102_0008; [bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x3f7_e7ff, bits[26]:0x1ff_ffff, bits[26]:0x2f6_fbff, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x3fe_fbff]; bits[30]:0x280_0309; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x0; bits[21]:0xa_aaaa; bits[7]:0x18"
+//     args: "bits[15]:0x3fff; bits[15]:0x2aaa; bits[33]:0xffff_ffff; bits[63]:0x6b7f_39d7_8d67_5902; [bits[26]:0x155_5555, bits[26]:0x3ff_ffff, bits[26]:0x123_f41f, bits[26]:0x155_53ff, bits[26]:0x2dd_fbe9, bits[26]:0x367_dffc, bits[26]:0x39b_3476, bits[26]:0x155_5555, bits[26]:0x167_5902]; bits[30]:0x28c0_3867; bits[1]:0x0; bits[49]:0x1_5555_5555_5555; bits[9]:0x1ff; bits[21]:0x100; bits[7]:0x20"
+//     args: "bits[15]:0x3fff; bits[15]:0x697f; bits[33]:0x462e_f66d; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x2df_ffac, bits[26]:0x349_ffbf, bits[26]:0x308_f2ad, bits[26]:0x22e_f66d, bits[26]:0x0, bits[26]:0x26e_f66d, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x24f_dafd]; bits[30]:0x16ac_fe15; bits[1]:0x0; bits[49]:0x1_fffb_cfbf_efda; bits[9]:0x47; bits[21]:0x13_7d7f; bits[7]:0x7d"
+//     args: "bits[15]:0x7fff; bits[15]:0x6e19; bits[33]:0xffff_ffff; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x20, bits[26]:0x1ff_ffff, bits[26]:0x37f_f830, bits[26]:0x1ff_ffff, bits[26]:0x3d5_5b7f, bits[26]:0x1ff_ffff, bits[26]:0x4_0000, bits[26]:0x8000, bits[26]:0x3ff_d5d2]; bits[30]:0x1fff_ffff; bits[1]:0x1; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x0; bits[21]:0x2_aee5; bits[7]:0x5f"
+//     args: "bits[15]:0x7fff; bits[15]:0x7fff; bits[33]:0x4000_0000; bits[63]:0x0; [bits[26]:0x299_8002, bits[26]:0x16b_2dde, bits[26]:0x2f1_7d96, bits[26]:0x12d_eafc, bits[26]:0x1ef_8090, bits[26]:0x3bb_d800, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x3ff_ffff]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0xffff_ffff_ffff; bits[9]:0x1ff; bits[21]:0x8000; bits[7]:0x7f"
+//     args: "bits[15]:0x0; bits[15]:0x80; bits[33]:0x8b82_aaf3; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x1d1_d541, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x387_abe1, bits[26]:0x108_9936, bits[26]:0x10_0000, bits[26]:0x75_5515, bits[26]:0x2e2_933b, bits[26]:0x23ff]; bits[30]:0x34ab_373b; bits[1]:0x1; bits[49]:0x1_fffe_f67f_effa; bits[9]:0x103; bits[21]:0x6_6fee; bits[7]:0x40"
+//     args: "bits[15]:0x5555; bits[15]:0x3fff; bits[33]:0xaaaa_aaaa; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x1ff_ffff, bits[26]:0x3b7_c7da, bits[26]:0xa8_6eee, bits[26]:0x2aa_2bff, bits[26]:0x2aa_b8aa, bits[26]:0x292_aaaa, bits[26]:0x1df_9c01, bits[26]:0x2aa_aaaa, bits[26]:0xea_569a]; bits[30]:0x1eb5_fbdf; bits[1]:0x0; bits[49]:0x1_5555_5555_5555; bits[9]:0x17b; bits[21]:0x1f_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x40; bits[15]:0x7fff; bits[33]:0x1_ffff_ffff; bits[63]:0x4baf_ea75_daee_aab8; [bits[26]:0x155_5555, bits[26]:0x10, bits[26]:0x0, bits[26]:0x0, bits[26]:0x3ff_ffff, bits[26]:0x9_425e, bits[26]:0x3ff_fbbf, bits[26]:0x34b_c3f5, bits[26]:0x2aa_aaaa]; bits[30]:0x37ff_20b4; bits[1]:0x1; bits[49]:0x0; bits[9]:0xb4; bits[21]:0x14_6051; bits[7]:0x24"
+//     args: "bits[15]:0x3fff; bits[15]:0x2aaa; bits[33]:0x1_ffff_ffff; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x352_0d17, bits[26]:0x3ff_dfff, bits[26]:0x2f7_7bff, bits[26]:0x26f_def6, bits[26]:0xaa_c96f, bits[26]:0x155_5555, bits[26]:0x2000, bits[26]:0x0, bits[26]:0x7f_c2dd]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x1_a4ae_d7ae_1017; bits[9]:0x20; bits[21]:0x0; bits[7]:0x4"
+//     args: "bits[15]:0x3fff; bits[15]:0x7fff; bits[33]:0xffff_ffff; bits[63]:0x4_0000_0000_0000; [bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x3bf_332c, bits[26]:0x1, bits[26]:0x1f2_35d2, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x155_5555, bits[26]:0x10_1008]; bits[30]:0x8_0000; bits[1]:0x0; bits[49]:0x0; bits[9]:0x155; bits[21]:0xb_d6d3; bits[7]:0x7f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x2a2b; bits[33]:0x1_719f_62ee; bits[63]:0x4c63_91bb_ba96_aaaa; [bits[26]:0x3ff_ffff, bits[26]:0x0, bits[26]:0xb1_d833, bits[26]:0x2d7_39c4, bits[26]:0x145_d860, bits[26]:0x155_5555, bits[26]:0x158_1805, bits[26]:0x26e_aff6, bits[26]:0x10c_1155]; bits[30]:0x3fff_ffff; bits[1]:0x1; bits[49]:0x0; bits[9]:0x20; bits[21]:0x0; bits[7]:0x2b"
+//     args: "bits[15]:0x7fff; bits[15]:0x3fed; bits[33]:0x100; bits[63]:0x3fed_a8aa_aaba_8aab; [bits[26]:0x1ff_6a00, bits[26]:0x2d7_5a12, bits[26]:0x280_4500, bits[26]:0x156_6043, bits[26]:0x3ff_ffff, bits[26]:0x900, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x155_5555]; bits[30]:0x10_0000; bits[1]:0x0; bits[49]:0xbbbd_5555_54d1; bits[9]:0x1c5; bits[21]:0x1f_ffff; bits[7]:0x51"
+//     args: "bits[15]:0x20; bits[15]:0x5555; bits[33]:0x1_ffff_ffff; bits[63]:0x5155_2aa2_92af_aa2a; [bits[26]:0x2a2_5946, bits[26]:0x297_ee21, bits[26]:0x2d7_fffc, bits[26]:0x26a_aaec, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffef, bits[26]:0x3ff_fbff, bits[26]:0x1_0155, bits[26]:0x29f_9f1c]; bits[30]:0x3fcf_beff; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0xff; bits[21]:0x0; bits[7]:0x1f"
+//     args: "bits[15]:0x3fff; bits[15]:0x37bb; bits[33]:0x4_0000; bits[63]:0x23db_aaaa_d2ae_2aab; [bits[26]:0x1ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x11c_308f, bits[26]:0x3ff_ffff, bits[26]:0x4_9000, bits[26]:0x336_9a84, bits[26]:0xf7_7bfb, bits[26]:0x2aa_aaaa, bits[26]:0x3f3_f810]; bits[30]:0x4_0000; bits[1]:0x1; bits[49]:0x1_5555_5555_5555; bits[9]:0x55; bits[21]:0x8_a08b; bits[7]:0x0"
+//     args: "bits[15]:0x5555; bits[15]:0x2aaa; bits[33]:0x1_ffff_ffff; bits[63]:0x0; [bits[26]:0x1ff_ffff, bits[26]:0x1ee_6fe3, bits[26]:0x1b_c800, bits[26]:0x20d_0870, bits[26]:0x2aa_2a2a, bits[26]:0x37f_ffff, bits[26]:0x352_042a, bits[26]:0x100_0000, bits[26]:0x15d_d7ff]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x0; bits[9]:0x1ff; bits[21]:0xa_f8a3; bits[7]:0x7f"
+//     args: "bits[15]:0x0; bits[15]:0x5555; bits[33]:0xaaaa_aaaa; bits[63]:0x2; [bits[26]:0xe9_e835, bits[26]:0x0, bits[26]:0x205_0406, bits[26]:0x1ff_ffff, bits[26]:0x2a2_e8ae, bits[26]:0x40_0cae, bits[26]:0x2aa_aaaa, bits[26]:0x3ff_ffff, bits[26]:0x28a_b0d7]; bits[30]:0x1fff_ffff; bits[1]:0x1; bits[49]:0xdfd9_bff7_ffbb; bits[9]:0x2; bits[21]:0x1f_ffff; bits[7]:0x6"
+//     args: "bits[15]:0x3fff; bits[15]:0x3fef; bits[33]:0xb7e9_25a0; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x155_5555, bits[26]:0x0, bits[26]:0x155_5555, bits[26]:0x3fd_eee7, bits[26]:0x100_0000, bits[26]:0x1a2_1e45, bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x39d_2ddc]; bits[30]:0x0; bits[1]:0x0; bits[49]:0x1_f338_266c_3655; bits[9]:0x18a; bits[21]:0x8_a7ff; bits[7]:0x3f"
+//     args: "bits[15]:0x2979; bits[15]:0x5555; bits[33]:0x1_575c_e2a8; bits[63]:0x7fd9_268b_241e_7cda; [bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x2ba_58f7, bits[26]:0x35f_73a8, bits[26]:0x1e_7cda, bits[26]:0x78_b468, bits[26]:0x17e_2bac, bits[26]:0x1ff_ffff, bits[26]:0x1e_d7fe]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x0; bits[9]:0xaa; bits[21]:0x9c49; bits[7]:0x40"
+//     args: "bits[15]:0x3fff; bits[15]:0x5555; bits[33]:0x0; bits[63]:0x5555_1020_0330_2030; [bits[26]:0x0, bits[26]:0x3ff_ffff, bits[26]:0x0, bits[26]:0x140_8803, bits[26]:0x3fd_e0c7, bits[26]:0xf1_35ea, bits[26]:0x140_34b2, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x0; bits[9]:0x30; bits[21]:0x19_68b4; bits[7]:0x0"
+//     args: "bits[15]:0x5570; bits[15]:0x7fff; bits[33]:0x5433_c7e2; bits[63]:0x7fbf_9044_081a_0038; [bits[26]:0x1ff_ffff, bits[26]:0x2, bits[26]:0x18b_2dc5, bits[26]:0x299_1044, bits[26]:0x1ff_ffff, bits[26]:0x377_7aa7, bits[26]:0x0, bits[26]:0x30b_c424, bits[26]:0x0]; bits[30]:0x0; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x0; bits[21]:0xa_aaaa; bits[7]:0x1b"
+//     args: "bits[15]:0x7fff; bits[15]:0x1; bits[33]:0xc6f9_d210; bits[63]:0x0; [bits[26]:0x2aa_aaaa, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x100, bits[26]:0x1ff_ffff, bits[26]:0x2f9_d210, bits[26]:0x110_0c21, bits[26]:0x2f8_1210, bits[26]:0x3e6_3816]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x1_0002_0300_0400; bits[9]:0xaa; bits[21]:0x15_5555; bits[7]:0x2a"
+//     args: "bits[15]:0x7268; bits[15]:0x0; bits[33]:0x1_c9b0_8000; bits[63]:0x0; [bits[26]:0x201_42bf, bits[26]:0x25bf, bits[26]:0x2, bits[26]:0x393_4e15, bits[26]:0x0, bits[26]:0x0, bits[26]:0x0, bits[26]:0x29e_b38e, bits[26]:0x1e0_9524]; bits[30]:0x122c_800d; bits[1]:0x1; bits[49]:0x1_8080_2008_4180; bits[9]:0x80; bits[21]:0x15_5555; bits[7]:0x70"
+//     args: "bits[15]:0x0; bits[15]:0x3fff; bits[33]:0xf76f_e18d; bits[63]:0x184_d9af_77fb_67ef; [bits[26]:0x0, bits[26]:0x0, bits[26]:0x17f_eb28, bits[26]:0x30b_ec89, bits[26]:0x2aa_aaaa, bits[26]:0x197_5175, bits[26]:0x244_29e6, bits[26]:0xf2_c8ab, bits[26]:0x1ff_ffff]; bits[30]:0x2aaa_aaaa; bits[1]:0x0; bits[49]:0x5d74_153f_efff; bits[9]:0x4e; bits[21]:0x19_42ee; bits[7]:0x10"
+//     args: "bits[15]:0x4973; bits[15]:0x0; bits[33]:0x0; bits[63]:0x2d81_2000_3dde_efcf; [bits[26]:0x1de_eee3, bits[26]:0x155_5555, bits[26]:0xde_ad4f, bits[26]:0x24b_9d55, bits[26]:0xa, bits[26]:0x310_07ff, bits[26]:0x3b2_87ba, bits[26]:0x1ff_ffff, bits[26]:0x155_5555]; bits[30]:0x1000_0240; bits[1]:0x0; bits[49]:0x0; bits[9]:0x1ff; bits[21]:0x15_5555; bits[7]:0x5f"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_5554_fdef; bits[63]:0x1517_b1f5_0392_21ef; [bits[26]:0x2aa_a840, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x2a8_2848, bits[26]:0x3ff_ffff, bits[26]:0x39c_e5ee, bits[26]:0x3ff_ffff, bits[26]:0xbe_2bff, bits[26]:0x3b2_35ee]; bits[30]:0x9f0_3e50; bits[1]:0x1; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0x1cf; bits[21]:0x1c_82e7; bits[7]:0x0"
+//     args: "bits[15]:0x0; bits[15]:0x0; bits[33]:0x1082_beaa; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x15_75ef, bits[26]:0x800, bits[26]:0x182_469f, bits[26]:0x71_725f, bits[26]:0x3bf_a2bb, bits[26]:0x3_b8aa, bits[26]:0x8000, bits[26]:0x280_05c3, bits[26]:0x230_dadf]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x1_9000_0000_0010; bits[9]:0xaa; bits[21]:0x0; bits[7]:0x13"
+//     args: "bits[15]:0x1; bits[15]:0x40; bits[33]:0x0; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x2aa_aaaa, bits[26]:0x3ff_ffff, bits[26]:0x2_0000, bits[26]:0x0, bits[26]:0x2aa_aaaa, bits[26]:0x8, bits[26]:0x0, bits[26]:0x219_2edc, bits[26]:0x302_59ff]; bits[30]:0x3fbb_feff; bits[1]:0x0; bits[49]:0x1_5555_5555_5555; bits[9]:0x33; bits[21]:0x1b_f7df; bits[7]:0x0"
+//     args: "bits[15]:0x3fff; bits[15]:0x800; bits[33]:0xe0d5_1158; bits[63]:0x2c20_d7ff_ff6f_f9ff; [bits[26]:0x3ff_ffff, bits[26]:0x10_0000, bits[26]:0x0, bits[26]:0x9d_991a, bits[26]:0x3a0_e40c, bits[26]:0x36f_f9ff, bits[26]:0x1d4_1158, bits[26]:0x26f_e927, bits[26]:0x36e_f9ff]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0xd7ff_ff6f_f9ff; bits[9]:0x0; bits[21]:0x13_000d; bits[7]:0x20"
+//     args: "bits[15]:0x7fff; bits[15]:0x2aaa; bits[33]:0x1_5555_5555; bits[63]:0x2828_dfef_6e7d_f7eb; [bits[26]:0x2d7_f881, bits[26]:0x155_5555, bits[26]:0x0, bits[26]:0x1000, bits[26]:0x145_5d55, bits[26]:0x155_5555, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff]; bits[30]:0x3fff_ffff; bits[1]:0x0; bits[49]:0x1_b4fe_726f_fcf5; bits[9]:0x1ff; bits[21]:0xa_aaaa; bits[7]:0x0"
+//     args: "bits[15]:0x200; bits[15]:0x0; bits[33]:0x2; bits[63]:0x2aaa_aaaa_aaaa_aaaa; [bits[26]:0x290_3574, bits[26]:0x2ae_ca0c, bits[26]:0x0, bits[26]:0x122_5922, bits[26]:0x303_78be, bits[26]:0x1ff_ffff, bits[26]:0x192_9e7d, bits[26]:0x0, bits[26]:0x155_5555]; bits[30]:0x0; bits[1]:0x0; bits[49]:0xbf28_54e4_307f; bits[9]:0x1aa; bits[21]:0x8; bits[7]:0x8"
+//     args: "bits[15]:0x200; bits[15]:0x2aaa; bits[33]:0x20c1_c380; bits[63]:0x87d_6b6b_d86e_98f1; [bits[26]:0x8000, bits[26]:0x0, bits[26]:0x12_0008, bits[26]:0x1dd_d716, bits[26]:0x4000, bits[26]:0x8000, bits[26]:0x0, bits[26]:0x2aa_aaaa, bits[26]:0x2aa_aaaa]; bits[30]:0x1755_5e71; bits[1]:0x1; bits[49]:0x0; bits[9]:0xff; bits[21]:0x0; bits[7]:0x15"
+//     args: "bits[15]:0x3fff; bits[15]:0x3fd9; bits[33]:0xefa7_ca20; bits[63]:0x0; [bits[26]:0x113_b210, bits[26]:0x80, bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x1ef_fd54, bits[26]:0x1ff_7d55, bits[26]:0x17a_f201, bits[26]:0x116_468a, bits[26]:0x1fa_dddd]; bits[30]:0x10_0000; bits[1]:0x0; bits[49]:0x624c_0800_2450; bits[9]:0x1b7; bits[21]:0x1; bits[7]:0x2a"
+//     args: "bits[15]:0x3fff; bits[15]:0x5555; bits[33]:0x7f51_bcdb; bits[63]:0x5f61_efff_efdf_feff; [bits[26]:0x1ff_ffff, bits[26]:0x31b_8fed, bits[26]:0x0, bits[26]:0x302_c331, bits[26]:0x100, bits[26]:0x29a_8c14, bits[26]:0x80, bits[26]:0x1ff_ffff, bits[26]:0x155_5555]; bits[30]:0x1fff_ffff; bits[1]:0x1; bits[49]:0x2_0000; bits[9]:0x125; bits[21]:0xf_ffff; bits[7]:0x4"
+//     args: "bits[15]:0x3fff; bits[15]:0x0; bits[33]:0x100_0000; bits[63]:0x5f8f_916b_3672_acc6; [bits[26]:0x555, bits[26]:0x1ff_ffff, bits[26]:0x1bb_a9e2, bits[26]:0x1ff_ffff, bits[26]:0x10b_cebd, bits[26]:0x2a_8cc6, bits[26]:0x1b9_f938, bits[26]:0x1ff_ffff, bits[26]:0x0]; bits[30]:0x15c2_6171; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x135; bits[21]:0x1f_ffff; bits[7]:0x41"
+//     args: "bits[15]:0x6a15; bits[15]:0x3fff; bits[33]:0xa6cc_e7df; bits[63]:0x3424_0c35_74f1_5dd5; [bits[26]:0x2fd_fd5d, bits[26]:0x4000, bits[26]:0x22a_e79d, bits[26]:0x2aa_aaaa, bits[26]:0x8c_e7df, bits[26]:0x200_0000, bits[26]:0x342_39a4, bits[26]:0x8, bits[26]:0x155_5555]; bits[30]:0x400_0000; bits[1]:0x0; bits[49]:0x2c17_64b5_5dc1; bits[9]:0xff; bits[21]:0x1f_ffff; bits[7]:0x4f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x4000; bits[33]:0x400; bits[63]:0x0; [bits[26]:0x80_f655, bits[26]:0x3ff_ffff, bits[26]:0xe_5600, bits[26]:0x8000, bits[26]:0x193_8e42, bits[26]:0x11f_dd1d, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x96_1bd5]; bits[30]:0x2aaa_aaaa; bits[1]:0x0; bits[49]:0x1_5555_5555_5555; bits[9]:0x8a; bits[21]:0xa_aaab; bits[7]:0x7a"
+//     args: "bits[15]:0x7fff; bits[15]:0x5555; bits[33]:0x1_5157_ffff; bits[63]:0x1417_feff_c120_1000; [bits[26]:0x1e_8f92, bits[26]:0x1ff_ffff, bits[26]:0x141_588a, bits[26]:0x177_ff3e, bits[26]:0x0, bits[26]:0x353_bdc5, bits[26]:0x3ff_ffff, bits[26]:0x3ff_fbfd, bits[26]:0x2aa_abfe]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0x2_0000; bits[9]:0x1b5; bits[21]:0x15_5555; bits[7]:0x4"
+//     args: "bits[15]:0x63ff; bits[15]:0x7bcf; bits[33]:0xaaaa_aaaa; bits[63]:0x7bcf_5d15_5755_5515; [bits[26]:0x31f_bc08, bits[26]:0x3ff_ffff, bits[26]:0x31f_f800, bits[26]:0x36b_1e41, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x2aa_a2ab, bits[26]:0x80_0000, bits[26]:0x209_df25]; bits[30]:0x1705_5515; bits[1]:0x1; bits[49]:0x1_b34a_c72d_ca7b; bits[9]:0x1ff; bits[21]:0x2_b78f; bits[7]:0x2a"
+//     args: "bits[15]:0x1d4a; bits[15]:0x48bc; bits[33]:0x1_0273_febf; bits[63]:0x20_0000; [bits[26]:0x347_e290, bits[26]:0x220_28c1, bits[26]:0x4000, bits[26]:0x3ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x2ba_9300, bits[26]:0x0, bits[26]:0x3ff_ffff, bits[26]:0x2aa_aaaa]; bits[30]:0x1f0d_446e; bits[1]:0x1; bits[49]:0x1_5e61_0100_532a; bits[9]:0x68; bits[21]:0xd_aca6; bits[7]:0x2a"
+//     args: "bits[15]:0x45ac; bits[15]:0x3fff; bits[33]:0xfff4_10ae; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x17e_dc62, bits[26]:0x3ff_ffff, bits[26]:0x4, bits[26]:0x1f6_5804, bits[26]:0x2d_67ff, bits[26]:0x3b5_6bfb, bits[26]:0x8_0000, bits[26]:0x4_0000, bits[26]:0x22d_66e6]; bits[30]:0x1fff_ffff; bits[1]:0x1; bits[49]:0x5467_0615_406e; bits[9]:0x1ef; bits[21]:0x0; bits[7]:0x3f"
+//     args: "bits[15]:0x7fff; bits[15]:0x6a99; bits[33]:0x1_aae2_ab68; bits[63]:0x6af2_a2c8_00d2_0063; [bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x1d1_408f, bits[26]:0x1ff_ffff, bits[26]:0x354_cbff, bits[26]:0x10, bits[26]:0xd2_1b63, bits[26]:0x0, bits[26]:0x3d2_6338]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0x2bbe_fbaa_cf94; bits[9]:0xe6; bits[21]:0x15_5555; bits[7]:0x14"
+//     args: "bits[15]:0x2aaa; bits[15]:0x2fbd; bits[33]:0xaaaa_aaaa; bits[63]:0x8aa_228a_a715_577c; [bits[26]:0x315_577c, bits[26]:0x1ff_ffff, bits[26]:0x155_5555, bits[26]:0x35c_e878, bits[26]:0x17c_ebff, bits[26]:0x0, bits[26]:0x135_d5bd, bits[26]:0x2aa_a3aa, bits[26]:0x400]; bits[30]:0x17de_a000; bits[1]:0x0; bits[49]:0xaaab_aaba_aaa2; bits[9]:0x155; bits[21]:0xe_ab61; bits[7]:0x70"
+//     args: "bits[15]:0x0; bits[15]:0x7fff; bits[33]:0xaaaa_aaaa; bits[63]:0x8_9212_5b63_f5a9; [bits[26]:0x168_3cd5, bits[26]:0x3e0_f7e9, bits[26]:0x2aa_aaaa, bits[26]:0x2a2_3aa2, bits[26]:0x398_8cbf, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x28d_a28b, bits[26]:0x221_8667]; bits[30]:0x80_0000; bits[1]:0x0; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x0; bits[21]:0x15_5555; bits[7]:0x57"
+//     args: "bits[15]:0x133e; bits[15]:0x133e; bits[33]:0x4cf8_0002; bits[63]:0x1733_4106_8030_0130; [bits[26]:0x112_3c73, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x2aa_aaaa, bits[26]:0x230_0339, bits[26]:0x218_8cb8, bits[26]:0x40_0000, bits[26]:0x99_73a6]; bits[30]:0x0; bits[1]:0x0; bits[49]:0x0; bits[9]:0xff; bits[21]:0x1f_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x4000; bits[15]:0x4420; bits[33]:0xaaaa_aaaa; bits[63]:0x5859_cedb_cb00_1c25; [bits[26]:0x2aa_aab2, bits[26]:0x400, bits[26]:0x8e_4ab6, bits[26]:0x29_6079, bits[26]:0x11a_d226, bits[26]:0x21_8041, bits[26]:0x394_1a80, bits[26]:0x200_0000, bits[26]:0x174_6335]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x1_f7bb_dbd4_fc48; bits[9]:0x155; bits[21]:0x1_912a; bits[7]:0x3f"
+//     args: "bits[15]:0x2000; bits[15]:0x14c5; bits[33]:0xffff_ffff; bits[63]:0x5555_5555_5555_5555; [bits[26]:0x0, bits[26]:0x3fd_7bff, bits[26]:0xab_afbf, bits[26]:0x100_02aa, bits[26]:0x104_0762, bits[26]:0xf6_0bff, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x1000]; bits[30]:0x942_bfbf; bits[1]:0x0; bits[49]:0x1_f37b_b081_459b; bits[9]:0x1ff; bits[21]:0x40; bits[7]:0x43"
+//     args: "bits[15]:0x2aaa; bits[15]:0x6cee; bits[33]:0x0; bits[63]:0x4869_6512_43ec_e1da; [bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x0, bits[26]:0x155_5555, bits[26]:0x4804, bits[26]:0x3ff_ffff, bits[26]:0x155_5555, bits[26]:0x1ae_a5d2]; bits[30]:0x2515_0201; bits[1]:0x1; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0xaa; bits[21]:0x1f_ffff; bits[7]:0x7f"
+//     args: "bits[15]:0x7fff; bits[15]:0x7ff6; bits[33]:0xaaaa_aaaa; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x155_5555, bits[26]:0x3fd_b0ac, bits[26]:0x1000, bits[26]:0x155_5555, bits[26]:0x3ff_ffff, bits[26]:0x3bf_f848, bits[26]:0x2ce_8bab, bits[26]:0x3b5_fbaa, bits[26]:0x3ad_4fbf]; bits[30]:0x3fff_ffff; bits[1]:0x0; bits[49]:0x1_c163_5428_6b8d; bits[9]:0x1e; bits[21]:0x18; bits[7]:0x0"
+//     args: "bits[15]:0x3fff; bits[15]:0x2aaa; bits[33]:0x1_32fa_b120; bits[63]:0x8a3_2e00_6b8c_59bc; [bits[26]:0x17f_fffe, bits[26]:0xcd_5130, bits[26]:0xff_f801, bits[26]:0x39d_59bc, bits[26]:0x2aa_aaaa, bits[26]:0x155_5555, bits[26]:0x80_0000, bits[26]:0x358_b527, bits[26]:0x2fa_b124]; bits[30]:0x0; bits[1]:0x1; bits[49]:0x1_ca69_3f75_f7b4; bits[9]:0x2; bits[21]:0xa_aaaa; bits[7]:0x3f"
+//     args: "bits[15]:0x3fff; bits[15]:0x3f7f; bits[33]:0xaaaa_aaaa; bits[63]:0x16ef_4020_1802_0470; [bits[26]:0x155_5555, bits[26]:0x223_cf1d, bits[26]:0x2aa_aaaa, bits[26]:0x2a9_f631, bits[26]:0x51_d190, bits[26]:0x1f_92d4, bits[26]:0x0, bits[26]:0x2aa_aaaa, bits[26]:0x0]; bits[30]:0x1fcf_8044; bits[1]:0x1; bits[49]:0x1_4820_6800_0670; bits[9]:0x100; bits[21]:0x1f_ffff; bits[7]:0x55"
+//     args: "bits[15]:0x3fff; bits[15]:0x2f07; bits[33]:0x1_5555_5555; bits[63]:0x2aaa_aaaa_aaaa_aaaa; [bits[26]:0x178_3fff, bits[26]:0x3ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x1ff_ffff, bits[26]:0x35b_74cd, bits[26]:0x2fa_22aa, bits[26]:0x1ff_ffff, bits[26]:0x158_3ea3, bits[26]:0x1ff_ffff]; bits[30]:0x1555_5555; bits[1]:0x1; bits[49]:0xa209_fa4a_1d0e; bits[9]:0xaa; bits[21]:0x18_e08a; bits[7]:0x37"
+//     args: "bits[15]:0x5555; bits[15]:0x51b5; bits[33]:0x0; bits[63]:0x4516_2404_4190_3002; [bits[26]:0x3ff_ffff, bits[26]:0x2ac_a0c4, bits[26]:0x67_2ff3, bits[26]:0x2, bits[26]:0x2aa_aaaa, bits[26]:0x200, bits[26]:0x3ff_ffff, bits[26]:0x2cd_ad54, bits[26]:0x98_a493]; bits[30]:0x2aaa_aaaa; bits[1]:0x1; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0x155; bits[21]:0x0; bits[7]:0x2"
+//     args: "bits[15]:0x5555; bits[15]:0x5555; bits[33]:0x1_5556_3058; bits[63]:0x1585_5d54_515d_455d; [bits[26]:0x2a6_ac02, bits[26]:0x1ff_ffff, bits[26]:0x349_724c, bits[26]:0x155_5555, bits[26]:0x3ff_931f, bits[26]:0x3ff_ffff, bits[26]:0x2ab_fc55, bits[26]:0x13d_6d5f, bits[26]:0x80]; bits[30]:0x100_0000; bits[1]:0x0; bits[49]:0xaaaa_aaaa_aaaa; bits[9]:0xfb; bits[21]:0xa_aaaa; bits[7]:0x7f"
+//     args: "bits[15]:0x7fff; bits[15]:0x6ffd; bits[33]:0x1_be6b_d777; bits[63]:0x7fff_ffff_ffff_ffff; [bits[26]:0x356_6926, bits[26]:0x240_d57f, bits[26]:0x25e_aa1e, bits[26]:0x3ad_7e02, bits[26]:0x247_da0c, bits[26]:0x278_89bc, bits[26]:0x27e_a3cf, bits[26]:0x2ff_ce59, bits[26]:0x2bb_691b]; bits[30]:0x3f6a_9ff4; bits[1]:0x1; bits[49]:0xffff_ffff_ffff; bits[9]:0xff; bits[21]:0x1a_9ff4; bits[7]:0x74"
+//     args: "bits[15]:0x7fff; bits[15]:0x23fd; bits[33]:0x800_0000; bits[63]:0x0; [bits[26]:0x32d_e02a, bits[26]:0x33f_d804, bits[26]:0x2aa_aaaa, bits[26]:0x211_002c, bits[26]:0x0, bits[26]:0x3ff_fa90, bits[26]:0xf0_0218, bits[26]:0x155_5555, bits[26]:0x61_0804]; bits[30]:0x100_0000; bits[1]:0x1; bits[49]:0x0; bits[9]:0x1d9; bits[21]:0x15_5555; bits[7]:0x2a"
+//     args: "bits[15]:0x3400; bits[15]:0x34d0; bits[33]:0x9b06_4c89; bits[63]:0x3681_130c_c555_55f1; [bits[26]:0x1ff_ffff, bits[26]:0x155_5555, bits[26]:0x238_eba9, bits[26]:0x120_1826, bits[26]:0x1ff_ffff, bits[26]:0x2aa_aaaa, bits[26]:0x1ae_9408, bits[26]:0xa8_8455, bits[26]:0x3a6_628d]; bits[30]:0x1555_5555; bits[1]:0x0; bits[49]:0x1_1305_cd55_91b1; bits[9]:0xff; bits[21]:0xa_aaaa; bits[7]:0x50"
+//     args: "bits[15]:0x7fff; bits[15]:0x7767; bits[33]:0xaaaa_aaaa; bits[63]:0x3b22_e08e_9fbf_e7ff; [bits[26]:0x3ff_fc0c, bits[26]:0x368_79b8, bits[26]:0x1ff_7e83, bits[26]:0x3be_afee, bits[26]:0x155_5555, bits[26]:0x3ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x3e4_0cd5, bits[26]:0x0]; bits[30]:0x3fff_ffff; bits[1]:0x0; bits[49]:0x1_ea42_f9e3_9da2; bits[9]:0x169; bits[21]:0x100; bits[7]:0x1f"
+//     args: "bits[15]:0x4dda; bits[15]:0x5555; bits[33]:0xffff_ffff; bits[63]:0x7376_5ffb_451f_94d5; [bits[26]:0x80, bits[26]:0x155_5555, bits[26]:0x26e_d3ff, bits[26]:0x155_5555, bits[26]:0x39f_94d5, bits[26]:0x1ff_ffff, bits[26]:0x308_aef4, bits[26]:0x5b_86d1, bits[26]:0x2f7_d7ad]; bits[30]:0x1fff_ffff; bits[1]:0x0; bits[49]:0x0; bits[9]:0x1ff; bits[21]:0x1d_cfe8; bits[7]:0x5f"
+//     args: "bits[15]:0x2aaa; bits[15]:0x3; bits[33]:0xffff_ffff; bits[63]:0x3fff_ffff_ffff_ffff; [bits[26]:0x8, bits[26]:0x80_8b8f, bits[26]:0x1_19ff, bits[26]:0x200_5fcf, bits[26]:0x1ff_ffff, bits[26]:0x59_ea76, bits[26]:0x3ff_ffff, bits[26]:0x391_18a3, bits[26]:0x12f_04f3]; bits[30]:0x1e27_d5f9; bits[1]:0x1; bits[49]:0x713d_eb83_d519; bits[9]:0xff; bits[21]:0x1a_aaa8; bits[7]:0x7f"
+//     args: "bits[15]:0x2aaa; bits[15]:0xabb; bits[33]:0x4a83_e8da; bits[63]:0x45aa_600a_4961_a49e; [bits[26]:0x155_5555, bits[26]:0x155_5000, bits[26]:0x363_acce, bits[26]:0x155_5555, bits[26]:0x3ff_ffff, bits[26]:0x3ff_ffff, bits[26]:0x155_5bff, bits[26]:0x57_56be, bits[26]:0x80]; bits[30]:0x200_0000; bits[1]:0x0; bits[49]:0x600a_4961_a49f; bits[9]:0x19e; bits[21]:0xf_ffff; bits[7]:0x7f"
+//     args: "bits[15]:0x2000; bits[15]:0x0; bits[33]:0x7107_9b46; bits[63]:0x820_be32_2f9d_b00a; [bits[26]:0x155_5555, bits[26]:0x31d_1110, bits[26]:0x2_c3ff, bits[26]:0x0, bits[26]:0x10c_a34f, bits[26]:0x100_03ff, bits[26]:0x1000, bits[26]:0x30f_940b, bits[26]:0x3_b552]; bits[30]:0x3394_9cc0; bits[1]:0x1; bits[49]:0x0; bits[9]:0x0; bits[21]:0x8_05a7; bits[7]:0x40"
+//     args: "bits[15]:0x32cd; bits[15]:0x3387; bits[33]:0x1_ffff_ffff; bits[63]:0x5555_5555_5555_5555; [bits[26]:0xd1_d345, bits[26]:0x3df_eff3, bits[26]:0x196_6aaa, bits[26]:0x31f_ce59, bits[26]:0x3dd_73e2, bits[26]:0x54_5545, bits[26]:0x155_5555, bits[26]:0x155_5555, bits[26]:0x3b7_dfff]; bits[30]:0x196e_8000; bits[1]:0x1; bits[49]:0x1_f909_92a5_e0be; bits[9]:0xaa; bits[21]:0xd_fdd5; bits[7]:0x3f"
+//     args: "bits[15]:0x3fff; bits[15]:0x2aaa; bits[33]:0x800_0000; bits[63]:0x6292_0200_9de7_55d1; [bits[26]:0x41_9225, bits[26]:0x1df_fbff, bits[26]:0x2aa_aaaa, bits[26]:0x0, bits[26]:0x1ff_ffff, bits[26]:0x45_96a0, bits[26]:0x218_ee5d, bits[26]:0x308_9156, bits[26]:0x1ff_ffff]; bits[30]:0x2137_0b11; bits[1]:0x0; bits[49]:0x20; bits[9]:0x0; bits[21]:0xf_ffff; bits[7]:0x30"
+//     args: "bits[15]:0x7fff; bits[15]:0x6eda; bits[33]:0x6d74_01ee; bits[63]:0x3a7a_87d5_61a1_3c04; [bits[26]:0x155_5555, bits[26]:0x176_0a1d, bits[26]:0x155_5555, bits[26]:0x155_5555, bits[26]:0x376_d7df, bits[26]:0x0, bits[26]:0x193_3c94, bits[26]:0x3a1_3227, bits[26]:0x1a0_6804]; bits[30]:0x2ad9_a5f9; bits[1]:0x1; bits[49]:0x0; bits[9]:0x8; bits[21]:0xf_ffff; bits[7]:0x3f"
+//     args: "bits[15]:0x0; bits[15]:0x60a4; bits[33]:0x1_8299_00d0; bits[63]:0x1048_b7d7_ddbb_ffff; [bits[26]:0x38d_1845, bits[26]:0x177_bedd, bits[26]:0x1ab_af3e, bits[26]:0x1ff_ffff, bits[26]:0x155_5555, bits[26]:0x3d9_2e22, bits[26]:0x0, bits[26]:0x99_a0d0, bits[26]:0x2_0000]; bits[30]:0x3012_0006; bits[1]:0x0; bits[49]:0x1_5555_5555_5555; bits[9]:0xaa; bits[21]:0x1_0000; bits[7]:0x4"
+//     args: "bits[15]:0x40; bits[15]:0x6142; bits[33]:0x0; bits[63]:0x8_0000; [bits[26]:0x155_5555, bits[26]:0x1ff_ffff, bits[26]:0x1ff_ffff, bits[26]:0x18_0030, bits[26]:0xf8_1893, bits[26]:0x88_0884, bits[26]:0x20, bits[26]:0x2aa_aaaa, bits[26]:0x14a_64cc]; bits[30]:0x0; bits[1]:0x1; bits[49]:0x1_ffff_ffff_ffff; bits[9]:0xc4; bits[21]:0x0; bits[7]:0x1"
+//   }
+// }
+// 
+// END_CONFIG
+const W32_V9 = u32:0x9;
+type x0 = u26;
+type x12 = bool;
+type x15 = s15;
+fn main(x1: s15, x2: u15, x3: u33, x4: u63, x5: x0[W32_V9], x6: s30, x7: s1, x8: u49, x9: s9, x10: u21, x11: s7) -> bool {
+    {
+        let x13: x12[63] = x4 as x12[63];
+        let x14: u63 = -x4;
+        let x16: x15[3] = [x1, x1, x1];
+        let x17: x0[1] = slice(x5, x14, x0[1]:[x5[u32:0x0], ...]);
+        let x18: u63 = x4 >> x2;
+        let x19: bool = x7 < x10 as s1;
+        let x20: s23 = s23:0x7f_ffff;
+        let x21: (x0[1], s15, u21, x12[63]) = (x17, x1, x10, x13);
+        let x22: s15 = x1 * x10 as s15;
+        let x23: bool = x21 != x21;
+        let x24: x0[1] = slice(x5, x23, x0[1]:[x5[u32:0x0], ...]);
+        let x25: bool = x18 as bool | x19;
+        let x26: s41 = s41:0x1ff_ffff_ffff;
+        let x27: bool = x21 != x21;
+        let x28: uN[65] = x23 ++ x18 ++ x23;
+        let x29: bool = or_reduce(x3);
+        let x30: bool = x23[x10+:bool];
+        let x31: u2 = one_hot(x30, bool:0x1);
+        let x32: bool = x30[x28+:bool];
+        let x33: s51 = s51:0x40;
+        let x34: bool = x32[-2:1];
+        x34
+    }
+}
diff --git a/xls/passes/canonicalization_pass.cc b/xls/passes/canonicalization_pass.cc
index 90b186b103..675e145462 100644
--- a/xls/passes/canonicalization_pass.cc
+++ b/xls/passes/canonicalization_pass.cc
@@ -312,9 +312,12 @@ static absl::StatusOr<bool> CanonicalizeNode(Node* n) {
   // selector with a select without a default.
   if (n->Is<Select>()) {
     Select* sel = n->As<Select>();
-    if (sel->default_value().has_value() &&
-        (sel->cases().size() + 1) ==
-            (1ULL << sel->selector()->BitCountOrDie())) {
+    int64_t selector_bit_count = sel->selector()->BitCountOrDie();
+    if (selector_bit_count < 63 &&  // don't consider 63+ bit selectors,
+                                    // otherwise 1ULL << selector_bit_count will
+                                    // overflow (it's too many cases anyways)
+        sel->default_value().has_value() &&
+        (sel->cases().size() + 1) == (1ULL << selector_bit_count)) {
       std::vector<Node*> new_cases(sel->cases().begin(), sel->cases().end());
       new_cases.push_back(*sel->default_value());
       XLS_RETURN_IF_ERROR(
diff --git a/xls/passes/canonicalization_pass_test.cc b/xls/passes/canonicalization_pass_test.cc
index 9c6dfb4cab..4f0ec5c868 100644
--- a/xls/passes/canonicalization_pass_test.cc
+++ b/xls/passes/canonicalization_pass_test.cc
@@ -255,5 +255,20 @@ TEST_F(CanonicalizePassTest, SelectWithInvertedSelector) {
                         /*cases=*/{m::Param("y"), m::Param("x")}));
 }
 
+TEST_F(CanonicalizePassTest, SelectWithGiantSelector) {
+  auto p = CreatePackage();
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, ParseFunction(R"(
+     fn f(p: bits[128], x: bits[8], y: bits[8]) -> bits[8] {
+        ret sel.2: bits[8] = sel(p, cases=[x], default=y)
+     }
+  )",
+                                                       p.get()));
+
+  EXPECT_THAT(Run(p.get()), IsOkAndHolds(false));
+  EXPECT_THAT(f->return_value(), m::Select(m::Param("p"),
+                                           /*cases=*/{m::Param("x")},
+                                           /*default_value=*/m::Param("y")));
+}
+
 }  // namespace
 }  // namespace xls