bitwright 0.8.0

Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and verified simplification.
Documentation
# bitwright proof ledger v2. Generated; do not edit.
core.arith::add_and_or 231e32f29079f031059e35c9ff2c7c8d identity exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::add_disjoint c21668d593d2958761d618170fb36e1a rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=991)
core.arith::add_xor_and 91a74de0aba7b7ddb91240edcadabeb2 identity exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::mul_pow2 6496ccdcfe6d1bf9444d7f829bb87e6a rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=891)
core.arith::neg_not 15e193fa568fc257d7e9a277953b4ad3 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.arith::neg_or_one 98376163b2a5e94798912073d97d99ce rule exhaustive(inst=6,maxw=6,cases=126,fired=63) sampled(inst=22,cases=1408,fired=1063)
core.arith::not_neg 96eba82dd2b9705852f297d0e47405d2 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.arith::or_from_xor_and a443c4a7e3f9daf9bff105bcdadf5353 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::sub_and f494f97854ab0848902d5d10e05d614e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.arith::udiv_pow2 ba7f88934bfc987b78342932a53ee20c rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=920)
core.arith::urem_pow2 dc139eed7a696ecabc31d530548007af rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=892)
core.bitwise::and_absorb_or 9fd8d816ee32d581eb8d62a20c32876f rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::and_mask_disjoint 724ff9a4b679b662432c8d23dcd9fb85 rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=982)
core.bitwise::and_mask_redundant 4b04f26d37d4b772c21cf6f7c3c3c8dd rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=926)
core.bitwise::and_not_disjoint 83f48fcf27539de57d3fbbba72d0563d rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=990)
core.bitwise::and_not_self a7155cc265a14fe9cc6247305f489835 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::or_absorb_and 0575f368bd8b21ed6f428408bf9277b9 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::or_known_ones ac0b9516b1f47ebda223602957a6db4d rule exhaustive(inst=6,maxw=6,cases=5460,fired=1092) sampled(inst=22,cases=1408,fired=914)
core.bitwise::or_not_self 18cda80f123e6c06993304f495dab989 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::xor_and_or 158833683befb8f7c053b44791d1009e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.bitwise::xor_not_self 30728f4168caab17ae4a4a889bcd36cb rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.casts::sext_from_sign_word ee0eb576cde4badf54fe874b005b357d rule exhaustive(inst=9,maxw=6,cases=98,fired=98) sampled(inst=190,cases=12160,fired=12160)
core.casts::trunc_and_zext 638d880dd6e9330bb45c32e910b73e9b rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=359,cases=22976,fired=22976)
core.casts::zext_trunc 03adbad05bdae1e06b83d6d82f6cb943 rule exhaustive(inst=15,maxw=6,cases=516,fired=516) sampled(inst=350,cases=22400,fired=22400)
core.compare::eq_eq_distinct 6f255a110c3116629fa5e4079eb430d3 rule exhaustive(inst=5,maxw=5,cases=37448,fired=36084) sampled(inst=22,cases=1408,fired=1377)
core.compare::eq_sub_zero ca8026a4dea10e0d08061cffc2487da6 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::eq_xor_zero 17a6d95c209f639b59167b13239eaa14 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::eq_zext b39dea5b1d2ab79b1da6cc49558341c2 rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=371,cases=23744,fired=23744)
core.compare::ne_xor_zero 8d9ce66dad854a8bb63a966ebf47b034 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::sle_const_not 9d3b42f8abf8a183bdaf41f9b123d126 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::sle_not_const 00cc7faec017605e52c0f9773c69a695 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::sle_not_not 9f63c6f648a5ccdeaf76154670e57a09 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::sle_or_common 95caafa9316b0fa74c2596e994d79ee3 rule exhaustive(inst=4,maxw=4,cases=69904,fired=22620) sampled(inst=22,cases=1408,fired=551)
core.compare::sle_zero_or_low da747bdf6705f9a7d007db6d5e1d4139 rule exhaustive(inst=5,maxw=5,cases=37448,fired=4856) sampled(inst=22,cases=1408,fired=286)
core.compare::slt_const_not a3c2d89b684069a7350ca3da6e818b86 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::slt_not_const 1477618f1607506633d72e55d84ffa3a rule exhaustive(inst=6,maxw=6,cases=5460,fired=5334) sampled(inst=22,cases=1408,fired=1289)
core.compare::slt_not_not c41be862ef554dc1bf880a0e9e696dae rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::slt_not_zero 063df1dfe4c08374333e894a88facbf0 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.compare::slt_or_common 452241393b96dfe156ce18c9b4e9d253 rule exhaustive(inst=4,maxw=4,cases=69904,fired=22620) sampled(inst=22,cases=1408,fired=543)
core.compare::slt_sext 4357801fd5d32647845c78115b30f1c7 rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=360,cases=23040,fired=23040)
core.compare::slt_zero_or_low d69e23066c70f2d5c8aaf92f73d63ff5 rule exhaustive(inst=5,maxw=5,cases=37448,fired=6220) sampled(inst=22,cases=1408,fired=448)
core.compare::ule_const_not 60f09a2c18de403fbb90bb66ca244435 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ule_not_const fae7fc5f6ef76cb5fb794c63e0396322 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ule_not_not 20ad54740edb9169e34fea639af4e6a7 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ule_or_common a7aa4f6d1ddce762a5003977f74fb6d8 rule exhaustive(inst=4,maxw=4,cases=69904,fired=22620) sampled(inst=22,cases=1408,fired=572)
core.compare::ult_const_not d08ec3446fc4d658b83c709c5b501dd3 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ult_not_const c5d697169797939214a514fd38dfc194 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ult_not_not 89405c4d64c880b19d9440b5efbe6546 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.compare::ult_one 2aed343e84cf6eef6c63488913bf5f5e rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.compare::ult_or_common b9fce9a0571406aaf50d6d2fcc2f67ad rule exhaustive(inst=4,maxw=4,cases=69904,fired=22620) sampled(inst=22,cases=1408,fired=557)
core.compare::ult_zext 8f96fb762bf7187a560b7f4b3e5cd61b rule exhaustive(inst=15,maxw=6,cases=1812,fired=1812) sampled(inst=357,cases=22848,fired=22848)
core.compare::zero_sle_or_low b5373ec29026f6b9e1a5371c8a52c228 rule exhaustive(inst=5,maxw=5,cases=37448,fired=6220) sampled(inst=22,cases=1408,fired=394)
core.compare::zero_slt_or_low dd23eed5e80ee58c54a96385713c0aff rule exhaustive(inst=5,maxw=5,cases=37448,fired=4856) sampled(inst=22,cases=1408,fired=279)
core.guarded_recovery::boolean_lowbit_mask_keep decb0ae9975b4524d6a760bd56c01cb5 rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.guarded_recovery::boolean_zext_mask_keep ba529cbf951c488bc69994b270c55ae8 rule exhaustive(inst=5,maxw=6,cases=248,fired=248) sampled(inst=22,cases=1408,fired=1408)
core.guarded_recovery::complementary_shift_rotate 261d5549bede65cb93aa803da98ba7be rule exhaustive(inst=5,maxw=5,cases=37448,fired=196) sampled(inst=22,cases=1408,fired=1)
core.guarded_recovery::increment_boolean cb487c5a0ad51813425d4989d024e1dd rule exhaustive(inst=1,maxw=1,cases=2,fired=2,complete) sampled(inst=1,cases=64,fired=64)
core.guarded_recovery::mask_or_add_constant 73495126a3e1879dff9d23437ca68248 rule exhaustive(inst=4,maxw=4,cases=69904,fired=41370) sampled(inst=22,cases=1408,fired=782)
core.guarded_recovery::mask_or_add_constant_carry 9382ff59b9ba5b15f2af9c6d05ede08c rule exhaustive(inst=4,maxw=4,cases=69904,fired=69904) sampled(inst=22,cases=1408,fired=1408)
core.guarded_recovery::negate_boolean b4d4394fef3ac4a714420c8fb792df79 rule exhaustive(inst=1,maxw=1,cases=2,fired=2,complete) sampled(inst=1,cases=64,fired=64)
core.guarded_recovery::recombine_shifted_field_or 8f9b6c7b8382124830bab5f753252d29 rule exhaustive(inst=4,maxw=4,cases=69904,fired=9020) sampled(inst=22,cases=1408,fired=75)
core.guarded_recovery::select_nonzero_value cc0b354dea08b023f7289413606535a4 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.guarded_recovery::sle_neg_pair 9bed35d33e79ffb4f3d9eb767c5009d4 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5214) sampled(inst=22,cases=1408,fired=1281)
core.guarded_recovery::slt_neg_pair cd86bf982e9a8aa5a1d3ed7d503648d1 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5214) sampled(inst=22,cases=1408,fired=1299)
core.guarded_recovery::split_mask_add 5d82cae63e20c5d7a97a08ac2977290f rule exhaustive(inst=4,maxw=4,cases=69904,fired=22620) sampled(inst=22,cases=1408,fired=541)
core.guarded_recovery::split_mask_increment c20405c68570202ee3a38ecaf47a2a14 rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=49)
core.guarded_recovery::split_mask_sub b6194d1b7fc8b679a724698c0ade0002 rule exhaustive(inst=4,maxw=4,cases=69904,fired=4680) sampled(inst=22,cases=1408,fired=42)
core.guarded_recovery::xor_complement_mask 960927c6017b6c83bf53419b598bc6e7 rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=36)
core.guarded_recovery::xor_zext_lowmask 2b2f0ea31c4fc44a521c08b0e23352ae rule exhaustive(inst=15,maxw=6,cases=114,fired=114) sampled(inst=361,cases=23104,fired=23104)
core.guarded_recovery_canonical::sle_neg_zero 7ac0936c5fb77be524554960e952feb1 rule exhaustive(inst=6,maxw=6,cases=126,fired=120) sampled(inst=22,cases=1408,fired=1357)
core.guarded_recovery_canonical::sle_zero_neg 33b225889c13b7d3bcb813aafbb36c11 rule exhaustive(inst=6,maxw=6,cases=126,fired=120) sampled(inst=22,cases=1408,fired=1355)
core.guarded_recovery_canonical::slt_neg_zero 81c11c2d8bfbca369d43fa48da869854 rule exhaustive(inst=6,maxw=6,cases=126,fired=120) sampled(inst=22,cases=1408,fired=1355)
core.guarded_recovery_canonical::slt_zero_neg e37484a4cd2660cd2d9ef2a9ac396c81 rule exhaustive(inst=6,maxw=6,cases=126,fired=120) sampled(inst=22,cases=1408,fired=1356)
core.guarded_recovery_canonical::split_mask_or_add 61dd03408ebe1c1fdfaf7d74166bfc2d rule exhaustive(inst=4,maxw=4,cases=69904,fired=1554) sampled(inst=22,cases=1408,fired=32)
core.guarded_recovery_concat::add_aligned_to_concat 5b006118f34f29a2c4623e16c2f9e125 rule exhaustive(inst=16,maxw=7,cases=255904,fired=255904) sampled(inst=368,cases=23552,fired=23552)
core.guarded_recovery_layout::add_constant_to_concat a32dedd375d4c13d453b2ea554fa64c6 rule exhaustive(inst=16,maxw=7,cases=255904,fired=255904) sampled(inst=377,cases=24128,fired=24128)
core.guarded_recovery_layout::recombine_low_constant 423c3787ef3d8cc7a16be2133df45fd2 rule exhaustive(inst=4,maxw=4,cases=69904,fired=1592) sampled(inst=22,cases=1408,fired=27)
core.guarded_recovery_layout::shifted_masked_add 35964b8448e43aa19ccd89fe200c28f5 rule exhaustive(inst=4,maxw=4,cases=69904,fired=69904) sampled(inst=22,cases=1408,fired=1408)
core.guarded_recovery_layout::split_or_masked_sum 6edef400bd6df617521f08587feff1f1 rule exhaustive(inst=4,maxw=4,cases=69904,fired=6850) sampled(inst=22,cases=1408,fired=292)
core.guarded_recovery_mba_normalized::sum_from_distributed_double_or ef2e0e97970fdc326ea66b4443d3a4b4 rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=27)
core.guarded_recovery_mba_normalized::sum_from_vanishing_double_mask 032b3d9b00c8abe84e35da4485b84095 rule exhaustive(inst=6,maxw=6,cases=5460,fired=252) sampled(inst=22,cases=1408,fired=261)
core.guarded_recovery_mba_normalized::xor_from_distributed_double_or 885b7e2212f505db257876c9f0422bfd rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=22)
core.guarded_recovery_shuffle::recombine_extracted_field b550746379b99aa58a2c5bb6c72922e1 rule exhaustive(inst=76,maxw=8,cases=1728208,fired=1728208) sampled(inst=357,cases=22848,fired=22848)
core.recovery_arith::and_from_or_minus_xor 4f32959fb22c740ae27d6bc49c77c84a rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::and_from_sum_minus_or 0848fe67a2976f410e84b40dc96043a5 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::negative_double 2dd9b11601ee02c12c2481336865e595 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::or_from_sum_minus_and f019fb342a613546b666686fef018ce0 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::sum_from_double_or_xor c497d69b28f29fe5c7fddbf8f1ed618c rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::xor_from_double_or_sum a1a8b030220d48537138d9890d2f74e9 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::xor_from_or_minus_and da70d981bf49c9fd64529be76dc44a95 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_arith::xor_from_sum_double_and 87922c512335e9dc7aead0ac1f51b865 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_inside_mask b21547342b4764bdc78919382df28147 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_ones 1cf95e04cab11d45e16faa0e5723c7a5 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_outside_mask 6cdc6658fa1fe8581bc5d36bb0507523 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_pext 434127252d87556ee17c32e8adf9837b rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_pext_and c097cdca5f3d9cc029a256d06a38b93e rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_pext_or 38a73402ab077b98a5047b95debd96fb rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pdep_pext_xor 13f4d3e6262c06a78db84ce5421f27ee rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pext_complement_mask bef068d280e4b2d936ec9c774d55bf58 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_bmi2::pext_pdep 560d3ba6655ac3aea8ef21e16bc765ae rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_canonical::pdep_pext_xor_constant b0b52d691ec3d9f5890585cfa37eaa35 rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.recovery_canonical::ugt_constant_borrow df2566dd7d5038afcb647f8443468505 rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=43)
core.recovery_canonical::ule_constant_borrow 15f51e06628836a54b64ad1b0e91685f rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=44)
core.recovery_canonical::xor_sign_bit_add f18d342b0c28847a665ac1f8629c0834 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_cast::add_trunc_pair 22d99e3b7a0a00771533a5b3209a8ba6 rule exhaustive(inst=15,maxw=6,cases=25488,fired=25488) sampled(inst=352,cases=22528,fired=22528)
core.recovery_cast::mul_trunc_pair cbbe3d929d5b43bc2b2524468a81c421 rule exhaustive(inst=15,maxw=6,cases=25488,fired=25488) sampled(inst=351,cases=22464,fired=22464)
core.recovery_cast::sub_trunc_pair 0a45027a533fdf6e7540c65b13d3af95 rule exhaustive(inst=15,maxw=6,cases=25488,fired=25488) sampled(inst=348,cases=22272,fired=22272)
core.recovery_compare::eq_complement ae5289db8dc7bc237fee54151a2b6eaf rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ne_complement a5a8e1f78d8062ff7e27da7502452dc9 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ne_sub_zero e589b3357c2bc9540d2e8fccfc8d6eb5 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::uge_add_no_carry b23d2644f395495e95f2de495ef8dd89 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ugt_add_no_carry 4ae0d0e87d6a1676e842bddd2c251a1f rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ugt_sub_borrow be2b71afc9cd772f13fe077f3fd3994b rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ule_add_carry db11312c1c1f6aa3198a77f33167ec6e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_compare::ule_sub_no_borrow 1d9377217cd4738d39ea635185154c94 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::smax_select_add 202e1d091ce0cbd95c5fde56649bcc6b rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::smax_select_or a96b051e78b1e3b4ccf1cfdc72cdca65 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::smin_select_add 63fb767bb76c62b9657b8e1f7cb796e7 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::smin_select_or ea53e0964607354ca9ae67367784e9f7 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umax_ones_sext_add 31e261b9853c15d1b1ffe9d7c00a6334 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umax_ones_sext_or f692afaca1ea5639d7430e4cdd1c9939 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umax_select_add 8d29c6759163c70788136963409a0c5d rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umax_select_or 95e13c50ebb6c3206ae5203bd5f2fc3b rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umin_select_add e85d34b2314c76d8155e7c8549eb6680 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_minmax::umin_select_or d35f10229f29eec5051c058b953f81a0 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select::merge_complementary_select_add f6624bdbe048a26d0d370b585787c538 rule exhaustive(inst=6,maxw=6,cases=10920,fired=10920) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select::merge_complementary_select_or c3d0f83fc0665e2cd570488760be1ade rule exhaustive(inst=6,maxw=6,cases=10920,fired=10920) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select::select_nonzero_self 75a81d70dd3cf878ddec1c312e4506d9 rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::smax_one_add f252c3a0d5c21512088b191386344522 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::smax_one_or c808260942e93cc7428a0e7ca5f93469 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::smin_one_add 6f1d6148ecbc8753d2c1ec9754709835 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::smin_one_or 3d39dd507657d9392d1435a673c79a8b rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::umax_one_add f87d2c5af5961625f95309229a37c51f rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::umax_one_or e128527ba3d2bf7143cb11eb4facad42 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::umin_one_add a3f99d66a09c601ea8f5333aaaa9ff63 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_one::umin_one_or 3642653cb96cf91401c09c675f4b1f79 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_ones::smax_ones_add 130e46c5b562004757683fe2956d2e51 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_ones::smax_ones_or f2d12fc870021b2152f32b5054073de0 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_ones::smin_ones_add 65e455fb270251d1b026c0e5868e45df rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_select_ones::smin_ones_or 13ae505e7b40ee221d48a846777875f6 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_shift::ashr_ashr 2470743a4f433d82e228b6dc995fe955 rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.recovery_shift::lshr_xor_dead_constant bbeeb14021d97e8886bcf8592c4065aa rule exhaustive(inst=5,maxw=5,cases=37448,fired=32378) sampled(inst=22,cases=1408,fired=1121)
core.recovery_shift::negate_sign_bit 727f614c174e631cbad727114e8eeb9f rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.recovery_shift::nonzero_from_sign_union 2f5d37db586048bfff0350c45fbcd244 rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.recovery_shift::shl_lshr 40bcc0cd3f2033d7a8aa5dfe5af954cc rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.recovery_shift::shl_xor_dead_constant f76582445ce8a11bcba8e17a795fa4cb rule exhaustive(inst=5,maxw=5,cases=37448,fired=32378) sampled(inst=22,cases=1408,fired=1093)
core.recovery_shuffle::concat_low_zero 21a122a2e27ea38f2791ccd666efd22e rule exhaustive(inst=34,maxw=11,cases=294744,fired=9732) sampled(inst=373,cases=23872,fired=3107)
core.select::select_one_zero f389254f8f48d32f0573ee1a15809ada rule exhaustive(inst=5,maxw=6,cases=10,fired=10) sampled(inst=22,cases=1408,fired=1408)
core.select::select_ones_zero 2e36b373d0f0970a2e5fbe0ff85abc44 rule exhaustive(inst=5,maxw=6,cases=10,fired=10) sampled(inst=22,cases=1408,fired=1408)
core.shift::lshr_lshr 87af211bb3c75865cff47a3b491ddba9 rule exhaustive(inst=5,maxw=5,cases=37448,fired=702) sampled(inst=22,cases=1408,fired=86)
core.shift::lshr_shl a74d7b719fb9c7d2eb29c298c256a209 rule exhaustive(inst=6,maxw=6,cases=5460,fired=642) sampled(inst=22,cases=1408,fired=391)
core.shift::rotl_rotl 212c7db1879190f843986b16418f0f33 rule exhaustive(inst=5,maxw=5,cases=37448,fired=37448) sampled(inst=22,cases=1408,fired=1408)
core.shift::rotl_rotr 9937dde5021a4bece4aea51006fd3a78 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.shift::rotr_rotl 1811b7f0e3c2e1e5d95f0a8cddb8402a rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.shift::shl_shl efa9216e0faad669ca5020ba0de9e37d rule exhaustive(inst=5,maxw=5,cases=37448,fired=702) sampled(inst=22,cases=1408,fired=117)
core.sign::and_signs 141cd85c65274dc9446795f57d258782 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::eq_signs 4e247ce4d032df2fb29a7687877d1a4b rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::lshr_sign_eq_one 54f66f8c24eddcc2971398a66093dadd rule exhaustive(inst=5,maxw=6,cases=124,fired=124) sampled(inst=22,cases=1408,fired=1408)
core.sign::lshr_sign_ne_zero 9f335e8c40f00e4d46b48e1509cd4c9d rule exhaustive(inst=6,maxw=6,cases=126,fired=126) sampled(inst=22,cases=1408,fired=1408)
core.sign::ne_sign_bits 70d49403c8e0c50a946ffa3bb94115ed rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.sign::ne_signs 32365ad93877c7f50b513071facc263e rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::or_signs ecebadcfd942a430261c4617e1097502 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::sge_from_flag_bits 62c97662d4b98ada637c9a3013c8c46f rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.sign::sge_from_flags b944b3b931e674dc8e6c976d71c9b4f7 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::sge_from_flags_const 063b9a5d0e5e7ebc5fa5d36952a76c9b rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=49)
core.sign::slt_from_flag_bits f174d4a9429d3c1a3bfa756ee3f8b0de rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.sign::slt_from_flags 93ebea81412e6655ec05bfb1ca036bdd rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::slt_from_flags_const c9a84d15eabd5887bbfb37eb549c06b6 rule exhaustive(inst=5,maxw=5,cases=37448,fired=1364) sampled(inst=22,cases=1408,fired=34)
core.sign::slt_from_flags_word b2d108eb76f2ddf5509b3eab7551bd01 rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.sign::xor_lshr_signs 4593d16a8aafa26bda98589a0df02814 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)
core.sign::xor_sign_bits f15ce0296dc46643b83b0839a8440fbe rule exhaustive(inst=5,maxw=6,cases=5456,fired=5456) sampled(inst=22,cases=1408,fired=1408)
core.sign::xor_signs bebaf9924fb359930cc992afea76efa5 rule exhaustive(inst=6,maxw=6,cases=5460,fired=5460) sampled(inst=22,cases=1408,fired=1408)