Proved after fix for #25086

new-proved.diff

--- proved-base-sorted.txt	2018-09-06 00:17:38.000000000 +0200
+++ proved-new-sorted.txt	2018-09-06 08:43:52.000000000 +0200
@@ -986,6 +986,7 @@
 cmd/compile/internal/gc/bv.go:272:13: Proved IsInBounds
 cmd/compile/internal/gc/bv.go:78:4: Proved IsInBounds
 cmd/compile/internal/gc/bv.go:86:4: Proved IsInBounds
+cmd/compile/internal/gc/class_string.go:15:33: Proved IsInBounds
 cmd/compile/internal/gc/closure.go:134:29: Proved IsNonNil
 cmd/compile/internal/gc/closure.go:139:35: Proved IsInBounds
 cmd/compile/internal/gc/closure.go:145:15: Proved IsInBounds
@@ -1365,8 +1366,10 @@
 cmd/compile/internal/gc/obj.go:272:33: Proved IsInBounds
 cmd/compile/internal/gc/obj.go:272:61: Proved IsInBounds
 cmd/compile/internal/gc/obj.go:275:21: Proved IsInBounds
+cmd/compile/internal/gc/obj.go:333:34: Proved Rsh32Ux64 bounded
 cmd/compile/internal/gc/obj.go:371:24: Proved IsInBounds
 cmd/compile/internal/gc/obj.go:85:19: Proved IsInBounds
+cmd/compile/internal/gc/op_string.go:15:27: Proved IsInBounds
 cmd/compile/internal/gc/order.go:1129:47: Proved IsInBounds
 cmd/compile/internal/gc/order.go:1184:2: Proved Eq8
 cmd/compile/internal/gc/order.go:1207:16: Proved IsInBounds
@@ -1461,12 +1464,14 @@
 cmd/compile/internal/gc/reflect.go:1509:30: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1515:19: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1554:18: Proved IsInBounds
+cmd/compile/internal/gc/reflect.go:1556:37: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1591:14: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1591:27: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1597:13: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1597:28: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1599:52: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:1728:26: Proved IsInBounds
+cmd/compile/internal/gc/reflect.go:1757:22: Proved Lsh8x64 bounded
 cmd/compile/internal/gc/reflect.go:1757:36: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:435:19: Proved IsInBounds
 cmd/compile/internal/gc/reflect.go:435:19: Proved IsNonNil
@@ -1687,6 +1692,9 @@
 cmd/compile/internal/gc/universe.go:110:23: Proved IsInBounds
 cmd/compile/internal/gc/universe.go:117:26: Proved IsInBounds
 cmd/compile/internal/gc/universe.go:123:25: Proved IsInBounds
+cmd/compile/internal/gc/universe.go:177:15: Proved IsInBounds
+cmd/compile/internal/gc/universe.go:199:13: Proved IsInBounds
+cmd/compile/internal/gc/universe.go:215:11: Proved IsInBounds
 cmd/compile/internal/gc/universe.go:216:16: Proved IsInBounds
 cmd/compile/internal/gc/universe.go:217:17: Proved IsInBounds
 cmd/compile/internal/gc/universe.go:218:19: Proved IsInBounds
@@ -2162,10 +2170,13 @@
 cmd/compile/internal/ssa/phiopt.go:43:27: Proved IsInBounds
 cmd/compile/internal/ssa/phiopt.go:54:22: Proved IsInBounds
 cmd/compile/internal/ssa/phiopt.go:95:45: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:1011:15: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:1070:15: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:1115:32: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:1116:15: Proved IsSliceInBounds
 cmd/compile/internal/ssa/poset.go:1128:3: Proved Eq8
 cmd/compile/internal/ssa/poset.go:1129:27: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:1129:27: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:1148:33: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:1149:22: Proved IsSliceInBounds
 cmd/compile/internal/ssa/poset.go:1152:3: Proved Eq8
@@ -2176,8 +2187,11 @@
 cmd/compile/internal/ssa/poset.go:206:25: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:210:12: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:213:12: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:29:24: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:29:32: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:33:25: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:33:33: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:37:28: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:423:8: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:432:8: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:433:6: Proved IsInBounds
@@ -2186,38 +2200,57 @@
 cmd/compile/internal/ssa/poset.go:443:38: Proved IsSliceInBounds
 cmd/compile/internal/ssa/poset.go:470:24: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:471:15: Proved IsSliceInBounds
+cmd/compile/internal/ssa/poset.go:477:19: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:478:15: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:478:15: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:478:15: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:480:24: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:502:23: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:503:14: Proved IsSliceInBounds
+cmd/compile/internal/ssa/poset.go:505:18: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:509:14: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:509:14: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:509:14: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:510:23: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:568:21: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:584:43: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:603:19: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:607:8: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:607:8: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:621:17: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:621:17: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:636:16: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:640:12: Proved IsInBounds
 cmd/compile/internal/ssa/poset.go:640:12: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:640:12: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:641:21: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:658:16: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:667:17: Proved Lsh64x32 bounded
 cmd/compile/internal/ssa/poset.go:763:27: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1000:22: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1014:20: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1019:39: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1051:29: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1239:29: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1242:18: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1242:29: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1246:18: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:1248:19: Proved IsInBounds
+cmd/compile/internal/ssa/poset.go:844:15: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/poset.go:861:26: Proved Lsh64x32 bounded
+cmd/compile/internal/ssa/prove.go:1036:22: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1050:20: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1055:39: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1087:29: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1275:29: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1278:18: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1278:29: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1282:18: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:1284:19: Proved IsInBounds
 cmd/compile/internal/ssa/prove.go:186:26: Proved IsInBounds
 cmd/compile/internal/ssa/prove.go:186:26: Proved IsSliceInBounds
 cmd/compile/internal/ssa/prove.go:187:26: Proved IsInBounds
 cmd/compile/internal/ssa/prove.go:187:26: Proved IsSliceInBounds
 cmd/compile/internal/ssa/prove.go:282:26: Proved IsNonNil
 cmd/compile/internal/ssa/prove.go:55:25: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:808:26: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:809:14: Proved IsSliceInBounds
+cmd/compile/internal/ssa/prove.go:793:19: Proved IsInBounds
 cmd/compile/internal/ssa/prove.go:80:10: Proved Lsh64x64 bounded
+cmd/compile/internal/ssa/prove.go:844:26: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:845:14: Proved IsSliceInBounds
 cmd/compile/internal/ssa/prove.go:85:12: Proved Lsh64x64 bounded
-cmd/compile/internal/ssa/prove.go:882:55: Proved IsInBounds
-cmd/compile/internal/ssa/prove.go:885:55: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:918:55: Proved IsInBounds
+cmd/compile/internal/ssa/prove.go:921:55: Proved IsInBounds
 cmd/compile/internal/ssa/regalloc.go:1026:18: Proved Ctz64 non-zero
 cmd/compile/internal/ssa/regalloc.go:1027:17: Proved IsInBounds
 cmd/compile/internal/ssa/regalloc.go:1041:16: Proved IsInBounds
@@ -3861,6 +3894,7 @@
 cmd/compile/internal/ssa/rewrite386.go:2597:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:2598:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:2603:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewrite386.go:2604:22: Proved Eq64
 cmd/compile/internal/ssa/rewrite386.go:2608:27: Proved Eq64
 cmd/compile/internal/ssa/rewrite386.go:2624:15: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:2625:17: Proved IsInBounds
@@ -3932,6 +3966,7 @@
 cmd/compile/internal/ssa/rewrite386.go:3212:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:3213:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:3218:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewrite386.go:3219:22: Proved Eq64
 cmd/compile/internal/ssa/rewrite386.go:3223:27: Proved Eq64
 cmd/compile/internal/ssa/rewrite386.go:3241:15: Proved IsInBounds
 cmd/compile/internal/ssa/rewrite386.go:3242:15: Proved IsInBounds
@@ -12940,6 +12975,7 @@
 cmd/compile/internal/ssa/rewriteAMD64.go:7935:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:7936:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:7941:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewriteAMD64.go:7942:22: Proved Eq64
 cmd/compile/internal/ssa/rewriteAMD64.go:7946:27: Proved Eq64
 cmd/compile/internal/ssa/rewriteAMD64.go:7962:15: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:7963:17: Proved IsInBounds
@@ -13067,6 +13103,7 @@
 cmd/compile/internal/ssa/rewriteAMD64.go:8990:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:8991:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:8996:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewriteAMD64.go:8997:22: Proved Eq64
 cmd/compile/internal/ssa/rewriteAMD64.go:9001:27: Proved Eq64
 cmd/compile/internal/ssa/rewriteAMD64.go:9017:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteAMD64.go:9023:17: Proved IsInBounds
@@ -25800,6 +25837,7 @@
 cmd/compile/internal/ssa/rewriteS390X.go:12045:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:12046:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:12051:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewriteS390X.go:12056:27: Proved Eq64
 cmd/compile/internal/ssa/rewriteS390X.go:12068:14: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:12069:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:12076:17: Proved IsInBounds
@@ -26720,6 +26758,7 @@
 cmd/compile/internal/ssa/rewriteS390X.go:18566:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:18567:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:18572:17: Proved IsInBounds
+cmd/compile/internal/ssa/rewriteS390X.go:18577:27: Proved Eq64
 cmd/compile/internal/ssa/rewriteS390X.go:18589:14: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:18590:17: Proved IsInBounds
 cmd/compile/internal/ssa/rewriteS390X.go:18598:17: Proved IsInBounds
@@ -36561,6 +36600,7 @@
 cmd/compile/internal/syntax/source.go:101:45: Proved IsInBounds
 cmd/compile/internal/syntax/token_string.go:16:33: Proved IsInBounds
 cmd/compile/internal/syntax/token_string.go:16:52: Proved IsInBounds
+cmd/compile/internal/types/etype_string.go:15:33: Proved IsInBounds
 cmd/compile/internal/types/pkg.go:103:10: Proved IsInBounds
 cmd/compile/internal/types/pkg.go:119:19: Proved IsInBounds
 cmd/compile/internal/types/pkg.go:76:50: Proved IsInBounds
@@ -38462,6 +38502,7 @@
 cmd/internal/goobj/read.go:267:23: Proved Lsh64x64 bounded
 cmd/internal/goobj/read.go:427:3: Proved IsInBounds
 cmd/internal/goobj/read.go:485:17: Proved IsInBounds
+cmd/internal/obj/addrtype_string.go:15:39: Proved IsInBounds
 cmd/internal/obj/arm/asm5.go:1060:16: Proved Lsh32x64 bounded
 cmd/internal/obj/arm/asm5.go:1081:10: Proved Lsh32x32 bounded
 cmd/internal/obj/arm/asm5.go:1259:2: Proved Eq8
@@ -40686,6 +40727,7 @@
 cmd/internal/objabi/line.go:81:40: Proved IsInBounds
 cmd/internal/objabi/path.go:19:12: Proved IsInBounds
 cmd/internal/objabi/path.go:33:12: Proved IsInBounds
+cmd/internal/objabi/symkind_string.go:15:37: Proved IsInBounds
 cmd/internal/objabi/util.go:136:25: Proved IsInBounds
 cmd/internal/objabi/util.go:139:9: Proved IsInBounds
 cmd/internal/objabi/util.go:36:2: Proved IsInBounds
@@ -40841,6 +40883,7 @@
 cmd/link/internal/ld/data.go:1548:15: Proved Neq64
 cmd/link/internal/ld/data.go:1565:15: Proved Neq64
 cmd/link/internal/ld/data.go:1582:15: Proved Neq64
+cmd/link/internal/ld/data.go:1602:29: Proved IsInBounds
 cmd/link/internal/ld/data.go:1609:14: Proved IsInBounds
 cmd/link/internal/ld/data.go:1717:4: Proved IsInBounds
 cmd/link/internal/ld/data.go:1720:4: Proved IsInBounds
@@ -40951,6 +40994,8 @@
 cmd/link/internal/ld/elf.go:1768:16: Proved IsInBounds
 cmd/link/internal/ld/elf.go:1967:17: Proved IsInBounds
 cmd/link/internal/ld/elf.go:2075:17: Proved IsInBounds
+cmd/link/internal/ld/elf.go:659:12: Proved IsInBounds
+cmd/link/internal/ld/elf.go:677:12: Proved IsInBounds
 cmd/link/internal/ld/elf.go:735:29: Proved IsInBounds
 cmd/link/internal/ld/elf.go:883:23: Proved IsSliceInBounds
 cmd/link/internal/ld/go.go:122:15: Proved IsInBounds
@@ -41175,6 +41220,8 @@
 cmd/link/internal/loadmacho/ldmacho.go:223:25: Proved slicemask not needed
 cmd/link/internal/loadmacho/ldmacho.go:240:25: Proved slicemask not needed
 cmd/link/internal/loadmacho/ldmacho.go:258:25: Proved slicemask not needed
+cmd/link/internal/loadmacho/ldmacho.go:336:17: Proved Lsh8x32 bounded
+cmd/link/internal/loadmacho/ldmacho.go:346:17: Proved Lsh8x32 bounded
 cmd/link/internal/loadmacho/ldmacho.go:412:25: Proved IsSliceInBounds
 cmd/link/internal/loadmacho/ldmacho.go:560:19: Proved IsInBounds
 cmd/link/internal/loadmacho/ldmacho.go:560:47: Proved IsInBounds
@@ -41225,6 +41272,7 @@
 cmd/link/internal/sym/reloc.go:104:49: Proved IsInBounds
 cmd/link/internal/sym/symbols.go:59:27: Proved IsSliceInBounds
 cmd/link/internal/sym/symbols.go:77:17: Proved IsSliceInBounds
+cmd/link/internal/sym/symkind_string.go:15:37: Proved IsInBounds
 cmd/link/internal/wasm/asm.go:130:14: Proved IsInBounds
 cmd/link/internal/x86/asm.go:210:6: Proved IsInBounds
 cmd/link/internal/x86/asm.go:219:6: Proved IsInBounds
@@ -42134,6 +42182,7 @@
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:314:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:319:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:335:2: Proved Eq8
+cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:336:18: Proved Lsh32x32 bounded
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:341:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:347:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:364:2: Proved Eq8
@@ -42150,6 +42199,7 @@
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:510:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:520:8: Proved Rsh32Ux64 bounded
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:529:2: Proved Eq8
+cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:531:20: Proved Lsh16x32 bounded
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:533:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:539:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm/armasm/decode.go:57:33: Proved IsInBounds
@@ -42159,6 +42209,8 @@
 cmd/vendor/golang.org/x/arch/arm/armasm/gnu.go:142:13: Proved Lsh16x64 bounded
 cmd/vendor/golang.org/x/arch/arm/armasm/gnu.go:99:9: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:289:10: Proved Lsh16x64 bounded
+cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:332:19: Proved IsInBounds
+cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:40:34: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:420:8: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:429:8: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm/armasm/inst.go:433:8: Proved IsInBounds
@@ -42234,6 +42286,7 @@
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:1634:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:165:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:1668:2: Proved Eq16
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:1678:19: Proved Eq32
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:168:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:1710:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:1734:2: Proved Eq16
@@ -42280,12 +42333,18 @@
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:255:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2566:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2576:2: Proved Eq16
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2589:50: Proved Lsh32x32 bounded
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2591:2: Proved Eq16
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2594:50: Proved Lsh32x32 bounded
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2599:50: Proved Lsh32x32 bounded
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2601:2: Proved Eq16
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2604:50: Proved Lsh32x32 bounded
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2639:7: Proved Eq32
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2651:7: Proved Eq32
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2663:7: Proved Eq32
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2667:7: Proved Eq32
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2685:7: Proved Eq32
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:2689:7: Proved Eq32
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:270:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:280:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:291:2: Proved Eq16
@@ -42338,6 +42397,7 @@
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:946:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/decode.go:974:2: Proved Eq16
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/gnu.go:30:32: Proved IsSliceInBounds
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:21:34: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:24:14: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:432:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:441:2: Proved Eq8
@@ -42351,7 +42411,9 @@
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:671:7: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:683:7: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:759:7: Proved Eq8
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:763:7: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:769:7: Proved Eq8
+cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:773:7: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:882:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:888:2: Proved Eq8
 cmd/vendor/golang.org/x/arch/arm64/arm64asm/inst.go:892:2: Proved Eq8
@@ -42471,11 +42533,15 @@
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1030:3: Proved Eq16
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1046:3: Proved Eq16
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1108:16: Proved IsInBounds
+cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1111:41: Proved IsInBounds
+cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1119:19: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1127:3: Proved Eq16
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1138:3: Proved Eq16
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1148:16: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1188:3: Proved Eq16
+cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1226:29: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1229:3: Proved Eq16
+cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1234:29: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1237:3: Proved Eq16
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1277:32: Proved IsInBounds
 cmd/vendor/golang.org/x/arch/x86/x86asm/decode.go:1283:15: Proved IsInBounds
@@ -42656,6 +42722,8 @@
 cmd/vendor/golang.org/x/crypto/ssh/terminal/terminal.go:514:2: Proved Eq32
 cmd/vendor/golang.org/x/crypto/ssh/terminal/terminal.go:594:36: Proved IsSliceInBounds
 cmd/vendor/golang.org/x/crypto/ssh/terminal/terminal.go:843:13: Proved Greater64
+cmd/vendor/golang.org/x/sys/unix/sockcmsg_unix.go:53:52: Proved IsSliceInBounds
+cmd/vendor/golang.org/x/sys/unix/sockcmsg_unix.go:69:13: Proved IsSliceInBounds
 cmd/vendor/golang.org/x/sys/unix/str.go:25:19: Proved IsSliceInBounds
 cmd/vendor/golang.org/x/sys/unix/syscall_bsd.go:157:27: Proved IsInBounds
 cmd/vendor/golang.org/x/sys/unix/syscall_bsd.go:173:27: Proved IsInBounds
@@ -42923,6 +42991,7 @@
 compress/bzip2/huffman.go:130:28: Proved IsInBounds
 compress/bzip2/huffman.go:219:25: Proved IsInBounds
 compress/bzip2/huffman.go:231:27: Proved IsInBounds
+compress/bzip2/huffman.go:46:21: Proved Rsh64Ux64 bounded
 compress/bzip2/move_to_front.go:45:15: Proved IsSliceInBounds
 compress/bzip2/move_to_front.go:46:4: Proved IsInBounds
 compress/flate/deflate.go:126:26: Proved slicemask not needed
@@ -42961,8 +43030,10 @@
 compress/flate/huffman_bit_writer.go:347:19: Proved IsSliceInBounds
 compress/flate/huffman_bit_writer.go:545:5: Proved IsInBounds
 compress/flate/huffman_bit_writer.go:550:4: Proved IsInBounds
+compress/flate/huffman_bit_writer.go:551:26: Proved IsInBounds
 compress/flate/huffman_bit_writer.go:551:4: Proved IsInBounds
 compress/flate/huffman_bit_writer.go:561:48: Proved IsInBounds
+compress/flate/huffman_bit_writer.go:597:27: Proved IsInBounds
 compress/flate/huffman_bit_writer.go:685:18: Proved IsSliceInBounds
 compress/flate/huffman_code.go:101:60: Proved IsInBounds
 compress/flate/huffman_code.go:166:23: Proved IsInBounds
@@ -42992,10 +43063,14 @@
 compress/flate/inflate.go:201:54: Proved Lsh64x64 bounded
 compress/flate/inflate.go:505:32: Proved IsSliceInBounds
 compress/flate/inflate.go:605:29: Proved IsSliceInBounds
+compress/flate/inflate.go:726:19: Proved Lsh32x64 bounded
+compress/flate/inflate.go:742:12: Proved Rsh32Ux64 bounded
 compress/flate/inflate.go:761:14: Proved IsInBounds
 compress/flate/inflate.go:764:14: Proved IsInBounds
 compress/flate/inflate.go:767:14: Proved IsInBounds
 compress/flate/inflate.go:770:14: Proved IsInBounds
+compress/flate/token.go:91:21: Proved IsInBounds
+compress/flate/token.go:94:27: Proved IsInBounds
 compress/gzip/gunzip.go:152:11: Proved IsInBounds
 compress/gzip/gunzip.go:155:11: Proved IsInBounds
 compress/gzip/gunzip.go:157:60: Proved IsSliceInBounds
@@ -43235,7 +43310,11 @@
 crypto/elliptic/p256_asm.go:187:24: Proved IsInBounds
 crypto/elliptic/p256_asm.go:341:36: Proved IsInBounds
 crypto/elliptic/p256_asm.go:448:27: Proved IsInBounds
+crypto/elliptic/p256_asm.go:484:32: Proved Rsh64Ux64 bounded
+crypto/elliptic/p256_asm.go:486:31: Proved Rsh64Ux64 bounded
 crypto/elliptic/p256_asm.go:490:49: Proved IsInBounds
+crypto/elliptic/p256_asm.go:560:32: Proved Rsh64Ux64 bounded
+crypto/elliptic/p256_asm.go:562:31: Proved Rsh64Ux64 bounded
 crypto/elliptic/p256_asm.go:581:19: Proved IsInBounds
 crypto/hmac/hmac.go:50:23: Proved IsSliceInBounds
 crypto/hmac/hmac.go:86:5: Proved IsInBounds
@@ -43262,6 +43341,8 @@
 crypto/md5/md5.go:123:49: Proved IsInBounds
 crypto/md5/md5.go:123:68: Proved IsInBounds
 crypto/md5/md5.go:124:11: Proved IsSliceInBounds
+crypto/md5/md5.go:154:13: Proved IsSliceInBounds
+crypto/md5/md5.go:155:8: Proved IsSliceInBounds
 crypto/md5/md5.go:184:25: Proved IsInBounds
 crypto/md5/md5.go:73:41: Proved IsSliceInBounds
 crypto/md5/md5.go:79:11: Proved IsSliceInBounds
@@ -43346,10 +43427,14 @@
 crypto/sha1/sha1.go:103:49: Proved IsInBounds
 crypto/sha1/sha1.go:103:68: Proved IsInBounds
 crypto/sha1/sha1.go:104:11: Proved IsSliceInBounds
+crypto/sha1/sha1.go:144:13: Proved IsSliceInBounds
+crypto/sha1/sha1.go:145:8: Proved IsSliceInBounds
 crypto/sha1/sha1.go:202:31: Proved IsInBounds
 crypto/sha1/sha1.go:214:45: Proved IsInBounds
 crypto/sha1/sha1.go:221:32: Proved IsInBounds
 crypto/sha1/sha1.go:221:7: Proved IsInBounds
+crypto/sha1/sha1.go:239:11: Proved IsInBounds
+crypto/sha1/sha1.go:242:22: Proved IsInBounds
 crypto/sha1/sha1.go:250:36: Proved IsInBounds
 crypto/sha1/sha1.go:251:38: Proved IsInBounds
 crypto/sha1/sha1.go:252:38: Proved IsInBounds
@@ -43422,6 +43507,8 @@
 crypto/sha256/sha256.go:148:49: Proved IsInBounds
 crypto/sha256/sha256.go:148:68: Proved IsInBounds
 crypto/sha256/sha256.go:149:11: Proved IsSliceInBounds
+crypto/sha256/sha256.go:217:13: Proved IsSliceInBounds
+crypto/sha256/sha256.go:218:8: Proved IsSliceInBounds
 crypto/sha256/sha256.go:86:111: Proved IsSliceInBounds
 crypto/sha256/sha256.go:86:56: Proved IsSliceInBounds
 crypto/sha256/sha256.go:92:11: Proved IsSliceInBounds
@@ -43488,6 +43575,8 @@
 crypto/sha512/sha512.go:219:50: Proved IsInBounds
 crypto/sha512/sha512.go:219:69: Proved IsInBounds
 crypto/sha512/sha512.go:220:11: Proved IsSliceInBounds
+crypto/sha512/sha512.go:280:13: Proved IsSliceInBounds
+crypto/sha512/sha512.go:281:8: Proved IsSliceInBounds
 crypto/sha512/sha512block.go:101:78: Proved IsInBounds
 crypto/sha512/sha512block.go:104:14: Proved IsInBounds
 crypto/sha512/sha512block.go:106:14: Proved IsInBounds
@@ -43763,7 +43852,9 @@
 crypto/tls/key_agreement.go:39:67: Proved IsInBounds
 crypto/tls/key_agreement.go:43:31: Proved IsSliceInBounds
 crypto/tls/key_agreement.go:71:55: Proved IsSliceInBounds
+crypto/tls/prf.go:22:13: Proved IsSliceInBounds
 crypto/tls/prf.go:361:3: Proved IsInBounds
+crypto/tls/prf.go:56:32: Proved IsSliceInBounds
 crypto/tls/prf.go:62:9: Proved IsInBounds
 crypto/tls/ticket.go:109:23: Proved IsInBounds
 crypto/tls/ticket.go:109:41: Proved IsInBounds
@@ -44016,6 +44107,10 @@
 debug/dwarf/open.go:63:33: Proved IsInBounds
 debug/dwarf/open.go:63:54: Proved IsInBounds
 debug/dwarf/open.go:63:75: Proved IsInBounds
+debug/dwarf/tag_string.go:27:34: Proved IsInBounds
+debug/dwarf/tag_string.go:32:34: Proved IsInBounds
+debug/dwarf/tag_string.go:37:34: Proved IsInBounds
+debug/dwarf/tag_string.go:40:34: Proved IsInBounds
 debug/dwarf/type.go:427:49: Proved IsInBounds
 debug/dwarf/type.go:455:12: Proved IsInBounds
 debug/dwarf/type.go:466:3: Proved Eq64
@@ -44479,11 +44574,13 @@
 encoding/json/encode.go:571:9: Proved IsSliceInBounds
 encoding/json/encode.go:634:11: Proved IsInBounds
 encoding/json/encode.go:689:18: Proved IsInBounds
+encoding/json/encode.go:891:18: Proved IsInBounds
 encoding/json/encode.go:891:48: Proved IsInBounds
 encoding/json/encode.go:896:20: Proved IsSliceInBounds
 encoding/json/encode.go:922:39: Proved IsSliceInBounds
 encoding/json/encode.go:925:20: Proved IsSliceInBounds
 encoding/json/encode.go:941:20: Proved IsSliceInBounds
+encoding/json/encode.go:963:18: Proved IsInBounds
 encoding/json/encode.go:963:48: Proved IsInBounds
 encoding/json/encode.go:968:14: Proved IsSliceInBounds
 encoding/json/encode.go:994:31: Proved IsSliceInBounds
@@ -45353,6 +45450,7 @@
 html/template/attr.go:141:22: Proved IsSliceInBounds
 html/template/attr.go:147:19: Proved IsInBounds
 html/template/attr.go:157:22: Proved IsSliceInBounds
+html/template/attr_string.go:15:31: Proved IsInBounds
 html/template/content.go:153:29: Proved IsInBounds
 html/template/css.go:132:11: Proved IsInBounds
 html/template/css.go:134:12: Proved IsSliceInBounds
@@ -45373,6 +45471,8 @@
 html/template/css.go:92:37: Proved IsSliceInBounds
 html/template/css.go:92:37: Proved IsSliceInBounds
 html/template/css.go:95:30: Proved IsSliceInBounds
+html/template/delim_string.go:15:33: Proved IsInBounds
+html/template/element_string.go:15:37: Proved IsInBounds
 html/template/escape.go:166:68: Proved IsInBounds
 html/template/escape.go:183:3: Proved Eq8
 html/template/escape.go:219:2: Proved Eq8
@@ -45405,6 +45505,8 @@
 html/template/js.go:52:37: Proved IsInBounds
 html/template/js.go:58:7: Proved Eq8
 html/template/js.go:89:39: Proved IsInBounds
+html/template/jsctx_string.go:15:33: Proved IsInBounds
+html/template/state_string.go:15:33: Proved IsInBounds
 html/template/template.go:413:21: Proved Less64
 html/template/transition.go:106:95: Proved IsSliceInBounds
 html/template/transition.go:111:44: Proved IsInBounds
@@ -45421,6 +45523,7 @@
 html/template/url.go:165:7: Proved IsInBounds
 html/template/url.go:211:19: Proved IsSliceInBounds
 html/template/url.go:51:16: Proved IsSliceInBounds
+html/template/urlpart_string.go:15:37: Proved IsInBounds
 image/color/color.go:204:11: Proved Neq32
 image/color/color.go:205:11: Proved Neq32
 image/color/color.go:206:11: Proved Neq32
@@ -45522,8 +45625,10 @@
 image/jpeg/fdct.go:186:51: Proved IsInBounds
 image/jpeg/fdct.go:187:51: Proved IsInBounds
 image/jpeg/fdct.go:188:51: Proved IsInBounds
+image/jpeg/huffman.go:108:8: Proved IsInBounds
 image/jpeg/huffman.go:116:30: Proved IsInBounds
 image/jpeg/huffman.go:117:22: Proved IsInBounds
+image/jpeg/huffman.go:140:33: Proved IsInBounds
 image/jpeg/huffman.go:160:21: Proved IsInBounds
 image/jpeg/huffman.go:161:21: Proved IsInBounds
 image/jpeg/huffman.go:162:24: Proved IsInBounds
@@ -45593,8 +45698,10 @@
 image/jpeg/scan.go:244:10: Proved IsInBounds
 image/jpeg/scan.go:245:17: Proved IsInBounds
 image/jpeg/scan.go:252:40: Proved IsInBounds
+image/jpeg/scan.go:272:31: Proved Lsh16x8 bounded
 image/jpeg/scan.go:291:19: Proved IsInBounds
 image/jpeg/scan.go:307:24: Proved Neq64
+image/jpeg/scan.go:367:26: Proved Lsh16x8 bounded
 image/jpeg/scan.go:430:7: Proved IsInBounds
 image/jpeg/scan.go:431:5: Proved IsInBounds
 image/jpeg/scan.go:433:5: Proved IsInBounds
@@ -45636,8 +45743,11 @@
 image/jpeg/writer.go:613:25: Proved IsInBounds
 image/png/paeth.go:67:19: Proved IsInBounds
 image/png/reader.go:1014:2: Proved Eq64
+image/png/reader.go:271:35: Proved IsSliceInBounds
 image/png/reader.go:277:31: Proved IsSliceInBounds
+image/png/reader.go:292:35: Proved IsSliceInBounds
 image/png/reader.go:298:31: Proved IsSliceInBounds
+image/png/reader.go:305:35: Proved IsSliceInBounds
 image/png/reader.go:316:60: Proved IsInBounds
 image/png/reader.go:468:2: Proved Eq64
 image/png/reader.go:519:13: Proved IsInBounds
@@ -45719,6 +45829,7 @@
 internal/trace/order.go:90:40: Proved IsInBounds
 internal/trace/order.go:91:22: Proved IsSliceInBounds
 internal/trace/order.go:97:12: Proved IsInBounds
+internal/trace/parser.go:185:63: Proved IsInBounds
 internal/trace/parser.go:296:26: Proved IsInBounds
 internal/trace/parser.go:296:43: Proved IsInBounds
 internal/trace/parser.go:296:9: Proved IsInBounds
@@ -45789,6 +45900,7 @@
 math/big/float.go:268:12: Proved IsSliceInBounds
 math/big/float.go:316:8: Proved IsSliceInBounds
 math/big/float.go:417:20: Proved IsInBounds
+math/big/float.go:417:20: Proved Rsh64Ux64 bounded
 math/big/float.go:445:3: Proved Eq8
 math/big/float.go:478:6: Proved IsInBounds
 math/big/float.go:484:9: Proved IsInBounds
@@ -45885,8 +45997,10 @@
 math/big/int.go:920:13: Proved IsInBounds
 math/big/int.go:958:22: Proved IsInBounds
 math/big/int.go:967:15: Proved IsInBounds
+math/big/int.go:967:15: Proved Rsh64Ux64 bounded
 math/big/int.go:96:7: Proved IsSliceInBounds
 math/big/int.go:970:18: Proved IsInBounds
+math/big/int.go:970:18: Proved Rsh64Ux64 bounded
 math/big/intconv.go:115:28: Proved IsInBounds
 math/big/intconv.go:131:35: Proved IsInBounds
 math/big/intmarsh.go:29:12: Proved IsSliceInBounds
@@ -45937,6 +46051,7 @@
 math/big/nat.go:220:9: Proved IsInBounds
 math/big/nat.go:223:20: Proved IsSliceInBounds
 math/big/nat.go:302:21: Proved IsSliceInBounds
+math/big/nat.go:303:13: Proved IsSliceInBounds
 math/big/nat.go:303:21: Proved IsSliceInBounds
 math/big/nat.go:341:11: Proved IsSliceInBounds
 math/big/nat.go:351:16: Proved IsSliceInBounds
@@ -45957,6 +46072,7 @@
 math/big/nat.go:500:33: Proved IsSliceInBounds
 math/big/nat.go:502:33: Proved IsSliceInBounds
 math/big/nat.go:51:19: Proved IsInBounds
+math/big/nat.go:520:13: Proved IsSliceInBounds
 math/big/nat.go:520:21: Proved IsSliceInBounds
 math/big/nat.go:535:11: Proved IsSliceInBounds
 math/big/nat.go:537:16: Proved IsSliceInBounds
@@ -45992,11 +46108,13 @@
 math/big/nat.go:820:12: Proved IsSliceInBounds
 math/big/nat.go:821:16: Proved IsSliceInBounds
 math/big/nat.go:832:12: Proved IsSliceInBounds
+math/big/nat.go:840:15: Proved Lsh64x64 bounded
 math/big/nat.go:844:13: Proved IsSliceInBounds
 math/big/nat.go:850:8: Proved IsInBounds
 math/big/nat.go:857:14: Proved IsSliceInBounds
 math/big/nat.go:860:4: Proved IsInBounds
 math/big/nat.go:874:15: Proved IsInBounds
+math/big/nat.go:874:19: Proved Rsh64Ux64 bounded
 math/big/nat.go:888:21: Proved IsSliceInBounds
 math/big/nat.go:893:6: Proved IsInBounds
 math/big/nat.go:89:12: Proved IsSliceInBounds
@@ -46039,6 +46157,7 @@
 math/big/prime.go:190:28: Proved IsInBounds
 math/big/prime.go:253:23: Proved IsInBounds
 math/big/prime.go:254:11: Proved IsInBounds
+math/big/prime.go:254:11: Proved Rsh64Ux64 bounded
 math/big/prime.go:310:25: Proved IsInBounds
 math/big/prime.go:48:13: Proved IsInBounds
 math/big/prime.go:50:25: Proved Lsh64x64 bounded
@@ -46072,7 +46191,16 @@
 math/big/ratmarsh.go:38:12: Proved IsSliceInBounds
 math/big/ratmarsh.go:48:11: Proved IsInBounds
 math/big/ratmarsh.go:53:38: Proved slicemask not needed
+math/big/roundingmode_string.go:15:47: Proved IsInBounds
+math/bits/bits.go:180:10: Proved Lsh8x64 bounded
+math/bits/bits.go:188:10: Proved Lsh16x64 bounded
+math/bits/bits.go:196:10: Proved Lsh32x64 bounded
+math/bits/bits.go:204:10: Proved Lsh64x64 bounded
 math/expm1.go:227:63: Proved Rsh64Ux64 bounded
+math/jn.go:109:9: Proved Eq64
+math/jn.go:113:9: Proved Eq64
+math/jn.go:284:8: Proved Eq64
+math/jn.go:288:8: Proved Eq64
 math/rand/normal.go:43:22: Proved IsInBounds
 math/rand/normal.go:62:44: Proved IsInBounds
 math/rand/normal.go:62:8: Proved IsInBounds
@@ -47096,18 +47224,30 @@
 os/path.go:31:35: Proved IsInBounds
 os/path_unix.go:24:14: Proved IsSliceInBounds
 os/path_unix.go:29:15: Proved IsSliceInBounds
+os/signal/signal.go:132:13: Proved Rsh32Ux64 bounded
 os/signal/signal.go:133:9: Proved IsInBounds
+os/signal/signal.go:133:9: Proved IsInBounds
+os/signal/signal.go:133:9: Proved Lsh32x64 bounded
 os/signal/signal.go:137:16: Proved IsInBounds
 os/signal/signal.go:137:17: Proved IsInBounds
 os/signal/signal.go:146:15: Proved Less64
+os/signal/signal.go:173:12: Proved Rsh32Ux64 bounded
 os/signal/signal.go:174:16: Proved IsInBounds
 os/signal/signal.go:174:17: Proved IsInBounds
 os/signal/signal.go:175:19: Proved IsInBounds
 os/signal/signal.go:202:39: Proved IsSliceInBounds
+os/signal/signal.go:224:12: Proved Rsh32Ux64 bounded
+os/signal/signal.go:235:14: Proved Rsh32Ux64 bounded
+os/signal/signal.go:36:24: Proved Rsh32Ux64 bounded
+os/signal/signal.go:40:22: Proved Lsh32x64 bounded
 os/signal/signal.go:40:34: Proved IsInBounds
+os/signal/signal.go:44:23: Proved Lsh32x64 bounded
 os/signal/signal.go:44:35: Proved IsInBounds
+os/signal/signal.go:58:13: Proved Rsh32Ux64 bounded
 os/signal/signal.go:59:18: Proved IsInBounds
 os/signal/signal.go:60:12: Proved IsInBounds
+os/signal/signal.go:60:12: Proved IsInBounds
+os/signal/signal.go:60:12: Proved Lsh32x64 bounded
 os/signal/signal.go:75:15: Proved Less64
 os/str.go:32:19: Proved IsSliceInBounds
 os/types.go:76:12: Proved IsInBounds
@@ -47255,8 +47395,13 @@
 reflect/type.go:1925:45: Proved IsInBounds
 reflect/type.go:2074:2: Proved Eq64
 reflect/type.go:2098:2: Proved Eq64
+reflect/type.go:2177:19: Proved Rsh8Ux64 bounded
+reflect/type.go:2180:25: Proved Lsh8x64 bounded
 reflect/type.go:2180:36: Proved IsInBounds
+reflect/type.go:2193:19: Proved Rsh8Ux64 bounded
+reflect/type.go:2196:25: Proved Lsh8x64 bounded
 reflect/type.go:2196:36: Proved IsInBounds
+reflect/type.go:2205:21: Proved Lsh8x64 bounded
 reflect/type.go:2205:32: Proved IsInBounds
 reflect/type.go:2423:18: Proved slicemask not needed
 reflect/type.go:2423:19: Proved IsSliceInBounds
@@ -47274,15 +47419,22 @@
 reflect/type.go:2767:38: Proved IsInBounds
 reflect/type.go:2815:12: Proved IsInBounds
 reflect/type.go:2869:27: Proved Neq64
+reflect/type.go:2905:21: Proved Rsh8Ux64 bounded
+reflect/type.go:2908:21: Proved Lsh8x64 bounded
 reflect/type.go:2908:29: Proved IsInBounds
 reflect/type.go:2958:24: Proved IsInBounds
 reflect/type.go:3068:17: Proved IsInBounds
+reflect/type.go:3068:17: Proved Lsh8x32 bounded
+reflect/type.go:3146:25: Proved Lsh8x32 bounded
 reflect/type.go:3146:4: Proved IsInBounds
 reflect/type.go:3159:13: Proved IsInBounds
 reflect/type.go:3161:12: Proved IsInBounds
+reflect/type.go:3161:12: Proved Lsh8x32 bounded
 reflect/type.go:3166:13: Proved IsInBounds
 reflect/type.go:3168:12: Proved IsInBounds
+reflect/type.go:3168:12: Proved Lsh8x32 bounded
 reflect/type.go:3169:12: Proved IsInBounds
+reflect/type.go:3169:12: Proved Lsh8x32 bounded
 reflect/type.go:557:9: Proved IsSliceInBounds
 reflect/type.go:562:11: Proved IsSliceInBounds
 reflect/type.go:565:24: Proved IsInBounds
@@ -47308,17 +47460,30 @@
 reflect/value.go:602:10: Proved IsInBounds
 reflect/value.go:788:14: Proved IsInBounds
 reflect/value.go:814:24: Proved IsInBounds
+regexp/backtrack.go:108:32: Proved Lsh32x64 bounded
+regexp/backtrack.go:111:32: Proved Lsh32x64 bounded
 regexp/backtrack.go:111:3: Proved IsInBounds
 regexp/backtrack.go:120:67: Proved IsInBounds
+regexp/backtrack.go:120:67: Proved Lsh32x64 bounded
+regexp/backtrack.go:120:67: Proved Lsh32x64 bounded
 regexp/backtrack.go:130:8: Proved IsInBounds
+regexp/backtrack.go:130:8: Proved Lsh32x64 bounded
+regexp/backtrack.go:130:8: Proved Lsh32x64 bounded
 regexp/backtrack.go:134:10: Proved IsInBounds
 regexp/backtrack.go:135:11: Proved IsInBounds
 regexp/backtrack.go:136:11: Proved IsInBounds
 regexp/backtrack.go:137:13: Proved IsSliceInBounds
 regexp/backtrack.go:148:20: Proved IsInBounds
+regexp/backtrack.go:148:20: Proved Lsh32x64 bounded
+regexp/backtrack.go:148:20: Proved Lsh32x64 bounded
 regexp/backtrack.go:180:3: Proved Eq8
 regexp/backtrack.go:185:11: Proved IsInBounds
+regexp/backtrack.go:185:11: Proved Lsh32x64 bounded
+regexp/backtrack.go:185:11: Proved Lsh32x64 bounded
+regexp/backtrack.go:191:10: Proved IsInBounds
 regexp/backtrack.go:191:10: Proved IsInBounds
+regexp/backtrack.go:191:10: Proved Lsh32x64 bounded
+regexp/backtrack.go:191:10: Proved Lsh32x64 bounded
 regexp/backtrack.go:195:3: Proved Eq8
 regexp/backtrack.go:257:3: Proved Eq8
 regexp/backtrack.go:269:11: Proved IsInBounds
@@ -47430,6 +47595,7 @@
 regexp/syntax/compile.go:284:55: Proved IsInBounds
 regexp/syntax/compile.go:284:73: Proved IsInBounds
 regexp/syntax/compile.go:59:21: Proved IsInBounds
+regexp/syntax/op_string.go:20:32: Proved IsInBounds
 regexp/syntax/parse.go:1071:18: Proved IsInBounds
 regexp/syntax/parse.go:1071:38: Proved IsInBounds
 regexp/syntax/parse.go:1075:22: Proved IsInBounds
@@ -47595,6 +47761,7 @@
 regexp/syntax/prog.go:317:2: Proved Eq8
 regexp/syntax/prog.go:323:2: Proved Eq8
 regexp/syntax/prog.go:329:2: Proved Eq8
+regexp/syntax/prog.go:58:20: Proved IsInBounds
 regexp/syntax/regexp.go:134:2: Proved Eq8
 regexp/syntax/regexp.go:142:21: Proved IsInBounds
 regexp/syntax/regexp.go:142:53: Proved IsInBounds
@@ -47612,7 +47779,10 @@
 runtime/cgocall.go:518:2: Proved Eq8
 runtime/cgocall.go:549:26: Proved IsInBounds
 runtime/cgocall.go:549:47: Proved IsInBounds
+runtime/cgocall.go:585:48: Proved Rsh32Ux32 bounded
+runtime/cgocall.go:589:22: Proved Rsh32Ux32 bounded
 runtime/cgocheck.go:145:26: Proved IsInBounds
+runtime/cgocheck.go:147:21: Proved Rsh32Ux32 bounded
 runtime/chan.go:81:44: Proved IsInBounds
 runtime/chan.go:81:44: Proved Neq64
 runtime/cpuprof.go:132:21: Proved IsSliceInBounds
@@ -47631,12 +47801,18 @@
 runtime/heapdump.go:165:14: Proved IsInBounds
 runtime/heapdump.go:168:20: Proved IsInBounds
 runtime/heapdump.go:178:18: Proved IsInBounds
+runtime/heapdump.go:237:16: Proved Rsh8Ux64 bounded
+runtime/heapdump.go:352:30: Proved IsInBounds
+runtime/heapdump.go:467:15: Proved Lsh8x64 bounded
 runtime/heapdump.go:473:15: Proved IsInBounds
 runtime/heapdump.go:474:17: Proved IsInBounds
 runtime/heapdump.go:493:12: Proved IsInBounds
 runtime/heapdump.go:496:28: Proved IsInBounds
 runtime/heapdump.go:564:28: Proved IsInBounds
 runtime/heapdump.go:599:17: Proved IsSliceInBounds
+runtime/heapdump.go:711:35: Proved Rsh32Ux32 bounded
+runtime/heapdump.go:714:21: Proved Rsh32Ux32 bounded
+runtime/heapdump.go:715:21: Proved Lsh8x64 bounded
 runtime/heapdump.go:715:29: Proved IsInBounds
 runtime/heapdump.go:81:32: Proved IsSliceInBounds
 runtime/iface.go:43:40: Proved IsInBounds
@@ -47645,51 +47821,104 @@
 runtime/malloc.go:369:50: Proved IsInBounds
 runtime/malloc.go:650:39: Proved IsInBounds
 runtime/malloc.go:752:14: Proved IsInBounds
+runtime/map.go:1013:31: Proved Lsh16x8 bounded
+runtime/map.go:1032:20: Proved Lsh64x8 bounded
+runtime/map.go:1037:22: Proved Lsh64x8 bounded
+runtime/map.go:1043:39: Proved Lsh64x8 bounded
+runtime/map.go:1066:25: Proved Lsh64x8 bounded
 runtime/map.go:1091:21: Proved IsInBounds
 runtime/map.go:1093:19: Proved IsInBounds
 runtime/map.go:1133:31: Proved IsInBounds
 runtime/map.go:1237:25: Proved Neq64
 runtime/map.go:1240:25: Proved Neq64
+runtime/map.go:180:20: Proved Lsh64x8 bounded
+runtime/map.go:185:20: Proved Lsh64x8 bounded
 runtime/map.go:299:39: Proved IsInBounds
 runtime/map.go:299:39: Proved Neq64
+runtime/map.go:311:20: Proved Lsh64x8 bounded
+runtime/map.go:338:21: Proved Lsh64x8 bounded
+runtime/map.go:346:26: Proved Lsh64x8 bounded
+runtime/map.go:405:17: Proved Lsh64x8 bounded
 runtime/map.go:420:16: Proved IsInBounds
+runtime/map.go:457:17: Proved Lsh64x8 bounded
 runtime/map.go:472:16: Proved IsInBounds
+runtime/map.go:498:17: Proved Lsh64x8 bounded
 runtime/map.go:513:16: Proved IsInBounds
+runtime/map.go:577:29: Proved Lsh64x8 bounded
 runtime/map.go:589:16: Proved IsInBounds
 runtime/map.go:590:17: Proved IsInBounds
 runtime/map.go:591:16: Proved IsInBounds
+runtime/map.go:622:36: Proved Lsh64x8 bounded
+runtime/map.go:622:78: Proved Lsh16x8 bounded
+runtime/map.go:684:29: Proved Lsh64x8 bounded
 runtime/map.go:693:16: Proved IsInBounds
 runtime/map.go:718:17: Proved IsInBounds
+runtime/map.go:768:33: Proved Lsh64x8 bounded
+runtime/map.go:812:44: Proved Lsh64x8 bounded
+runtime/map.go:825:27: Proved Lsh64x8 bounded
+runtime/map.go:853:23: Proved Lsh64x8 bounded
+runtime/map.go:958:20: Proved Lsh64x8 bounded
+runtime/map.go:998:73: Proved Lsh64x8 bounded
+runtime/map_fast32.go:113:29: Proved Lsh64x8 bounded
 runtime/map_fast32.go:125:16: Proved IsInBounds
+runtime/map_fast32.go:151:36: Proved Lsh64x8 bounded
+runtime/map_fast32.go:151:78: Proved Lsh16x8 bounded
+runtime/map_fast32.go:199:29: Proved Lsh64x8 bounded
 runtime/map_fast32.go:211:16: Proved IsInBounds
+runtime/map_fast32.go:237:36: Proved Lsh64x8 bounded
+runtime/map_fast32.go:237:78: Proved Lsh16x8 bounded
+runtime/map_fast32.go:281:29: Proved Lsh64x8 bounded
 runtime/map_fast32.go:289:40: Proved IsInBounds
+runtime/map_fast32.go:29:18: Proved Lsh64x8 bounded
 runtime/map_fast32.go:302:17: Proved IsInBounds
+runtime/map_fast32.go:317:46: Proved Lsh64x8 bounded
+runtime/map_fast32.go:327:25: Proved Lsh64x8 bounded
 runtime/map_fast32.go:352:21: Proved IsInBounds
 runtime/map_fast32.go:354:19: Proved IsInBounds
 runtime/map_fast32.go:370:31: Proved IsInBounds
 runtime/map_fast32.go:44:40: Proved IsInBounds
+runtime/map_fast32.go:69:18: Proved Lsh64x8 bounded
 runtime/map_fast32.go:84:40: Proved IsInBounds
+runtime/map_fast64.go:113:29: Proved Lsh64x8 bounded
 runtime/map_fast64.go:125:16: Proved IsInBounds
+runtime/map_fast64.go:151:36: Proved Lsh64x8 bounded
+runtime/map_fast64.go:151:78: Proved Lsh16x8 bounded
+runtime/map_fast64.go:199:29: Proved Lsh64x8 bounded
 runtime/map_fast64.go:211:16: Proved IsInBounds
+runtime/map_fast64.go:237:36: Proved Lsh64x8 bounded
+runtime/map_fast64.go:237:78: Proved Lsh16x8 bounded
+runtime/map_fast64.go:281:29: Proved Lsh64x8 bounded
 runtime/map_fast64.go:289:40: Proved IsInBounds
+runtime/map_fast64.go:29:18: Proved Lsh64x8 bounded
 runtime/map_fast64.go:302:17: Proved IsInBounds
+runtime/map_fast64.go:317:46: Proved Lsh64x8 bounded
+runtime/map_fast64.go:327:25: Proved Lsh64x8 bounded
 runtime/map_fast64.go:352:21: Proved IsInBounds
 runtime/map_fast64.go:354:19: Proved IsInBounds
 runtime/map_fast64.go:370:31: Proved IsInBounds
 runtime/map_fast64.go:44:40: Proved IsInBounds
+runtime/map_fast64.go:69:18: Proved Lsh64x8 bounded
 runtime/map_fast64.go:84:40: Proved IsInBounds
 runtime/map_faststr.go:120:37: Proved IsInBounds
 runtime/map_faststr.go:133:36: Proved IsInBounds
+runtime/map_faststr.go:163:17: Proved Lsh64x8 bounded
 runtime/map_faststr.go:179:36: Proved IsInBounds
+runtime/map_faststr.go:212:29: Proved Lsh64x8 bounded
 runtime/map_faststr.go:225:16: Proved IsInBounds
 runtime/map_faststr.go:226:17: Proved IsInBounds
+runtime/map_faststr.go:255:36: Proved Lsh64x8 bounded
+runtime/map_faststr.go:255:78: Proved Lsh16x8 bounded
+runtime/map_faststr.go:299:29: Proved Lsh64x8 bounded
 runtime/map_faststr.go:309:36: Proved IsInBounds
 runtime/map_faststr.go:31:37: Proved IsInBounds
 runtime/map_faststr.go:323:17: Proved IsInBounds
+runtime/map_faststr.go:338:47: Proved Lsh64x8 bounded
+runtime/map_faststr.go:348:25: Proved Lsh64x8 bounded
 runtime/map_faststr.go:373:21: Proved IsInBounds
 runtime/map_faststr.go:375:19: Proved IsInBounds
 runtime/map_faststr.go:391:31: Proved IsInBounds
 runtime/map_faststr.go:44:36: Proved IsInBounds
+runtime/map_faststr.go:74:17: Proved Lsh64x8 bounded
 runtime/map_faststr.go:90:36: Proved IsInBounds
 runtime/mbitmap.go:1284:22: Proved Lsh64x64 bounded
 runtime/mbitmap.go:1297:16: Proved Lsh64x64 bounded
@@ -47699,34 +47928,59 @@
 runtime/mbitmap.go:1606:14: Proved IsInBounds
 runtime/mbitmap.go:1609:32: Proved IsInBounds
 runtime/mbitmap.go:1683:25: Proved Lsh64x64 bounded
+runtime/mbitmap.go:169:33: Proved Lsh8x64 bounded
 runtime/mbitmap.go:1701:25: Proved Lsh64x64 bounded
 runtime/mbitmap.go:1846:41: Proved Lsh64x64 bounded
+runtime/mbitmap.go:1862:32: Proved Lsh64x64 bounded
 runtime/mbitmap.go:1869:49: Proved Lsh64x64 bounded
+runtime/mbitmap.go:1885:32: Proved Lsh64x64 bounded
 runtime/mbitmap.go:1978:12: Proved IsSliceInBounds
+runtime/mbitmap.go:1997:49: Proved Rsh8Ux64 bounded
+runtime/mbitmap.go:2009:49: Proved Rsh8Ux64 bounded
+runtime/mbitmap.go:2021:22: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:2024:48: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:2049:40: Proved Rsh8Ux64 bounded
+runtime/mbitmap.go:250:33: Proved Lsh8x64 bounded
 runtime/mbitmap.go:267:13: Proved IsInBounds
+runtime/mbitmap.go:269:27: Proved Lsh8x64 bounded
+runtime/mbitmap.go:273:34: Proved Lsh8x64 bounded
 runtime/mbitmap.go:365:12: Proved IsInBounds
 runtime/mbitmap.go:490:10: Proved IsInBounds
+runtime/mbitmap.go:519:25: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:526:15: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:534:15: Proved Rsh32Ux32 bounded
 runtime/mbitmap.go:598:16: Proved IsInBounds
+runtime/mbitmap.go:628:18: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:638:18: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:669:17: Proved Rsh32Ux32 bounded
+runtime/mbitmap.go:690:19: Proved Lsh8x64 bounded
 runtime/mbitmap.go:786:28: Proved Neq64
+runtime/mbitmap.go:910:20: Proved Lsh8x64 bounded
 runtime/mcache.go:122:34: Proved IsInBounds
 runtime/mcache.go:131:15: Proved IsInBounds
 runtime/mcache.go:137:15: Proved IsInBounds
 runtime/mcache.go:139:30: Proved IsInBounds
 runtime/mcache.go:140:17: Proved IsInBounds
 runtime/mcache.go:81:16: Proved IsInBounds
+runtime/mcentral.go:146:15: Proved Rsh64Ux64 bounded
 runtime/mcentral.go:229:31: Proved IsInBounds
 runtime/mfinal.go:106:38: Proved IsInBounds
+runtime/mfinal.go:384:15: Proved IsSliceInBounds
 runtime/mgc.go:202:7: Proved IsInBounds
 runtime/mgc.go:2143:26: Proved IsInBounds
 runtime/mgc.go:2147:22: Proved IsInBounds
 runtime/mgc.go:2210:12: Proved IsSliceInBounds
 runtime/mgc.go:2223:15: Proved IsSliceInBounds
 runtime/mgcmark.go:1050:22: Proved IsInBounds
+runtime/mgcmark.go:1100:21: Proved Rsh32Ux32 bounded
+runtime/mgcmark.go:1165:32: Proved Lsh8x64 bounded
+runtime/mgcmark.go:1191:42: Proved Lsh8x64 bounded
 runtime/mgcmark.go:1227:13: Proved IsInBounds
 runtime/mgcmark.go:1235:26: Proved IsInBounds
 runtime/mgcmark.go:1339:56: Proved Neq64
 runtime/mgcmark.go:1348:57: Proved Neq64
 runtime/mgcmark.go:143:14: Proved IsInBounds
+runtime/mgcsweep.go:227:30: Proved Lsh8x64 bounded
 runtime/mgcsweep.go:335:49: Proved IsInBounds
 runtime/mgcsweepbuf.go:175:41: Proved IsInBounds
 runtime/mgcsweepbuf.go:176:16: Proved IsSliceInBounds
@@ -47738,6 +47992,7 @@
 runtime/mheap.go:1061:13: Proved IsInBounds
 runtime/mheap.go:1071:10: Proved IsInBounds
 runtime/mheap.go:1158:31: Proved IsInBounds
+runtime/mheap.go:1522:27: Proved Lsh8x64 bounded
 runtime/mheap.go:348:13: Proved Neq64
 runtime/mheap.go:386:40: Proved IsInBounds
 runtime/mheap.go:475:13: Proved IsInBounds
@@ -47782,6 +48037,7 @@
 runtime/mstats.go:646:15: Proved IsInBounds
 runtime/mstats.go:646:47: Proved IsInBounds
 runtime/mstats.go:647:27: Proved IsInBounds
+runtime/mwbbuf.go:258:33: Proved Lsh8x64 bounded
 runtime/os_darwin.go:345:61: Proved IsSliceInBounds
 runtime/os_darwin.go:346:34: Proved slicemask not needed
 runtime/os_darwin.go:346:38: Proved IsSliceInBounds
@@ -47813,6 +48069,7 @@
 runtime/panic.go:307:19: Proved IsInBounds
 runtime/panic.go:40:14: Proved IsSliceInBounds
 runtime/panic.go:50:14: Proved IsSliceInBounds
+runtime/panic.go:780:21: Proved IsInBounds
 runtime/plugin.go:104:57: Proved IsInBounds
 runtime/plugin.go:99:14: Proved IsInBounds
 runtime/pprof/elf.go:102:29: Proved IsSliceInBounds
@@ -48021,6 +48278,10 @@
 runtime/proc.go:4246:14: Proved IsInBounds
 runtime/proc.go:4439:14: Proved IsInBounds
 runtime/proc.go:4611:14: Proved IsInBounds
+runtime/proc.go:4622:80: Proved IsInBounds
+runtime/proc.go:4812:12: Proved IsInBounds
+runtime/proc.go:4817:11: Proved IsInBounds
+runtime/proc.go:4828:8: Proved IsInBounds
 runtime/proc.go:4832:18: Proved IsInBounds
 runtime/proc.go:501:16: Proved IsSliceInBounds
 runtime/proc.go:5064:10: Proved IsInBounds
@@ -48041,6 +48302,7 @@
 runtime/runtime1.go:419:13: Proved Lsh32x64 bounded
 runtime/runtime1.go:462:27: Proved IsInBounds
 runtime/runtime1.go:463:29: Proved IsSliceInBounds
+runtime/runtime2.go:825:26: Proved IsInBounds
 runtime/select.go:124:21: Proved IsSliceInBounds
 runtime/select.go:125:21: Proved IsSliceInBounds
 runtime/select.go:130:10: Proved IsInBounds
@@ -48053,37 +48315,64 @@
 runtime/select.go:528:9: Proved IsInBounds
 runtime/select.go:70:39: Proved IsInBounds
 runtime/signal_amd64x.go:61:26: Proved IsInBounds
+runtime/signal_sighandler.go:104:22: Proved IsInBounds
+runtime/signal_sighandler.go:48:24: Proved IsInBounds
+runtime/signal_sighandler.go:84:46: Proved Lsh32x32 bounded
 runtime/signal_unix.go:101:26: Proved IsInBounds
 runtime/signal_unix.go:104:13: Proved IsInBounds
 runtime/signal_unix.go:104:38: Proved IsInBounds
 runtime/signal_unix.go:106:20: Proved IsInBounds
 runtime/signal_unix.go:107:19: Proved IsInBounds
+runtime/signal_unix.go:107:19: Proved Lsh32x32 bounded
 runtime/signal_unix.go:112:20: Proved IsInBounds
+runtime/signal_unix.go:157:7: Proved IsInBounds
 runtime/signal_unix.go:162:17: Proved IsInBounds
 runtime/signal_unix.go:163:24: Proved IsInBounds
+runtime/signal_unix.go:182:7: Proved IsInBounds
 runtime/signal_unix.go:191:26: Proved IsInBounds
 runtime/signal_unix.go:192:17: Proved IsInBounds
 runtime/signal_unix.go:193:35: Proved IsInBounds
+runtime/signal_unix.go:211:7: Proved IsInBounds
 runtime/signal_unix.go:213:16: Proved IsInBounds
+runtime/signal_unix.go:226:18: Proved IsInBounds
 runtime/signal_unix.go:262:27: Proved Neq32
+runtime/signal_unix.go:33:22: Proved IsInBounds
+runtime/signal_unix.go:412:30: Proved IsInBounds
+runtime/signal_unix.go:460:32: Proved IsInBounds
+runtime/signal_unix.go:616:30: Proved IsInBounds
 runtime/signal_unix.go:617:24: Proved IsInBounds
 runtime/signal_unix.go:620:17: Proved IsInBounds
+runtime/signal_unix.go:92:8: Proved IsInBounds
 runtime/signal_unix.go:99:13: Proved IsInBounds
+runtime/sigqueue.go:125:24: Proved Lsh32x32 bounded
+runtime/sigqueue.go:126:26: Proved Lsh32x32 bounded
 runtime/sigqueue.go:126:34: Proved IsInBounds
 runtime/sigqueue.go:126:8: Proved IsInBounds
 runtime/sigqueue.go:152:16: Proved IsInBounds
 runtime/sigqueue.go:152:30: Proved IsInBounds
+runtime/sigqueue.go:200:9: Proved Lsh32x32 bounded
 runtime/sigqueue.go:201:29: Proved IsInBounds
 runtime/sigqueue.go:203:21: Proved IsInBounds
+runtime/sigqueue.go:204:10: Proved Lsh32x32 bounded
 runtime/sigqueue.go:205:30: Proved IsInBounds
+runtime/sigqueue.go:219:10: Proved Lsh32x32 bounded
 runtime/sigqueue.go:220:29: Proved IsInBounds
+runtime/sigqueue.go:232:10: Proved Lsh32x32 bounded
 runtime/sigqueue.go:233:29: Proved IsInBounds
 runtime/sigqueue.go:235:21: Proved IsInBounds
+runtime/sigqueue.go:236:9: Proved Lsh32x32 bounded
 runtime/sigqueue.go:237:30: Proved IsInBounds
+runtime/sigqueue.go:246:9: Proved Lsh32x32 bounded
 runtime/sigqueue.go:247:30: Proved IsInBounds
+runtime/sigqueue.go:254:13: Proved Lsh32x32 bounded
 runtime/sigqueue.go:83:22: Proved IsInBounds
 runtime/sigqueue.go:88:29: Proved IsInBounds
 runtime/slice.go:160:29: Proved Ctz64 non-zero
+runtime/slice.go:164:29: Proved Lsh64x64 bounded
+runtime/slice.go:165:28: Proved Lsh64x64 bounded
+runtime/slice.go:166:40: Proved Lsh64x64 bounded
+runtime/slice.go:167:42: Proved Rsh64Ux64 bounded
+runtime/slice.go:168:23: Proved Rsh64Ux64 bounded
 runtime/slice.go:173:43: Proved IsInBounds
 runtime/slice.go:173:43: Proved Neq64
 runtime/slice.go:174:27: Proved Neq64
@@ -48102,6 +48391,7 @@
 runtime/stack.go:278:29: Proved IsInBounds
 runtime/stack.go:287:27: Proved IsInBounds
 runtime/stack.go:288:27: Proved IsInBounds
+runtime/stack.go:298:27: Proved IsInBounds
 runtime/stack.go:304:30: Proved IsInBounds
 runtime/stack.go:305:30: Proved IsInBounds
 runtime/stack.go:344:43: Proved Less32U
@@ -48116,6 +48406,7 @@
 runtime/stack.go:456:38: Proved IsInBounds
 runtime/stack.go:457:29: Proved IsInBounds
 runtime/stack.go:458:23: Proved IsInBounds
+runtime/stack.go:557:12: Proved Rsh8Ux64 bounded
 runtime/string.go:158:10: Proved IsSliceInBounds
 runtime/string.go:234:43: Proved IsInBounds
 runtime/string.go:336:16: Proved IsInBounds
@@ -48142,6 +48433,7 @@
 runtime/symtab.go:578:73: Proved IsInBounds
 runtime/symtab.go:592:23: Proved IsInBounds
 runtime/symtab.go:729:11: Proved IsInBounds
+runtime/symtab.go:903:23: Proved Lsh32x32 bounded
 runtime/symtab.go:93:36: Proved IsInBounds
 runtime/symtab.go:93:36: Proved IsInBounds
 runtime/symtab.go:93:36: Proved IsSliceInBounds
@@ -48201,6 +48493,8 @@
 runtime/traceback.go:867:74: Proved IsInBounds
 runtime/traceback.go:875:16: Proved IsInBounds
 runtime/traceback.go:875:45: Proved IsInBounds
+runtime/traceback.go:897:26: Proved IsInBounds
+runtime/traceback.go:904:32: Proved IsInBounds
 runtime/type.go:100:2: Proved Eq8
 runtime/type.go:122:7: Proved IsInBounds
 runtime/type.go:291:18: Proved IsInBounds
@@ -48208,6 +48502,7 @@
 runtime/type.go:294:13: Proved IsInBounds
 runtime/type.go:294:65: Proved IsInBounds
 runtime/type.go:498:29: Proved IsSliceInBounds
+runtime/type.go:612:29: Proved IsSliceInBounds
 runtime/type.go:614:22: Proved IsInBounds
 runtime/type.go:620:23: Proved IsInBounds
 runtime/type.go:64:2: Proved Eq8
@@ -48308,6 +48603,7 @@
 strconv/extfloat.go:632:4: Proved IsInBounds
 strconv/ftoa.go:297:15: Proved IsInBounds
 strconv/ftoa.go:351:23: Proved IsSliceInBounds
+strconv/itoa.go:164:6: Proved Rsh64Ux64 bounded
 strconv/itoa.go:16:15: Proved IsSliceInBounds
 strconv/itoa.go:27:15: Proved IsSliceInBounds
 strconv/itoa.go:42:27: Proved IsSliceInBounds
@@ -48494,6 +48790,8 @@
 syscall/route_darwin.go:50:11: Proved IsInBounds
 syscall/route_darwin.go:57:11: Proved IsInBounds
 syscall/route_darwin.go:64:11: Proved IsInBounds
+syscall/sockcmsg_unix.go:53:52: Proved IsSliceInBounds
+syscall/sockcmsg_unix.go:69:13: Proved IsSliceInBounds
 syscall/str.go:23:19: Proved IsSliceInBounds
 syscall/syscall.go:49:7: Proved IsInBounds
 syscall/syscall_bsd.go:156:27: Proved IsInBounds
@@ -48936,6 +49234,7 @@
 unicode/letter.go:360:28: Proved IsInBounds
 unicode/letter.go:95:14: Proved IsInBounds
 unicode/utf16/utf16.go:97:27: Proved IsInBounds
+unicode/utf16/utf16.go:99:21: Proved Less32
 unicode/utf16/utf16.go:99:40: Proved IsInBounds
 unicode/utf8/utf8.go:107:15: Proved IsInBounds
 unicode/utf8/utf8.go:113:17: Proved IsInBounds