useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
		useSlice(a[:i+12])

	}

	useInt(a[i])
	useInt(a[i]) // ERROR "Proved IsInBounds$"
}

func f11b(a []int, i int) {
	useSlice(a[i:])
	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
}

func f11c(a []int, i int) {
	useSlice(a[:i])
	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
}

func f11d(a []int, i int) {
	useInt(a[2*i+7])
	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
}

func f12(a []int, b int) {

				}
				if logopt.Enabled() {
					if v.Op == OpIsInBounds {
						logopt.LogOpt(v.Pos, "isInBounds", "checkbce", f.Name)
					}
					if v.Op == OpIsSliceInBounds {
						logopt.LogOpt(v.Pos, "isSliceInBounds", "checkbce", f.Name)
					}
				}
			}
		}
	}

	}
}

func g2(a []int) {
	useInt(a[3]) // ERROR "Found IsInBounds$"
	useInt(a[2])
	useInt(a[1])
	useInt(a[0])
}

func g3(a []int) {
	for i := range a[:256] { // ERROR "Found IsSliceInBounds$"
		useInt(a[i]) // ERROR "Found IsInBounds$"
	}
	b := a[:256]
	for i := range b {
		useInt(b[i])
	}
}

func g4(a [100]int) {
	for i := 10; i < 50; i++ {
		useInt(a[i-10])

(IsSliceInBounds x x) => (ConstBool [true])
(IsSliceInBounds (And32 (Const32 [c]) _) (Const32 [d])) && 0 <= c && c <= d => (ConstBool [true])
(IsSliceInBounds (And64 (Const64 [c]) _) (Const64 [d])) && 0 <= c && c <= d => (ConstBool [true])
(IsSliceInBounds (Const32 [0]) _) => (ConstBool [true])
(IsSliceInBounds (Const64 [0]) _) => (ConstBool [true])

(InterCall ...) => (LoweredInterCall ...)
(TailCall ...) => (LoweredTailCall ...)

// Miscellaneous
(Convert ...) => (LoweredConvert ...)
(IsNonNil p) => (I64Eqz (I64Eqz p))
(IsInBounds ...) => (I64LtU ...)
(IsSliceInBounds ...) => (I64LeU ...)
(NilCheck ...) => (LoweredNilCheck ...)
(GetClosurePtr ...) => (LoweredGetClosurePtr ...)
(GetCallerPC ...) => (LoweredGetCallerPC ...)
(GetCallerSP ...) => (LoweredGetCallerSP ...)

(AtomicCompareAndSwap64 ...) => (LoweredAtomicCas64 ...)

// checks
(NilCheck ...) => (LoweredNilCheck ...)
(IsNonNil ptr) => (SGTU ptr (MOVVconst [0]))
(IsInBounds idx len) => (SGTU len idx)
(IsSliceInBounds idx len) => (XOR (MOVVconst [1]) (SGTU idx len))

// pseudo-ops
(GetClosurePtr ...) => (LoweredGetClosurePtr ...)
(GetCallerSP ...) => (LoweredGetCallerSP ...)
(GetCallerPC ...) => (LoweredGetCallerPC ...)

	(LoweredZero [t.Alignment()]
		ptr
		(ADD <ptr.Type> ptr (MOVDconst [s-moveSize(t.Alignment(), config)]))
		mem)

// Checks
(IsNonNil ...) => (SNEZ ...)
(IsInBounds ...) => (Less64U ...)
(IsSliceInBounds ...) => (Leq64U ...)

// Trivial lowering
(NilCheck ...) => (LoweredNilCheck ...)
(GetClosurePtr ...) => (LoweredGetClosurePtr ...)
(GetCallerSP ...) => (LoweredGetCallerSP ...)

(AtomicOr32  ...) => (LoweredAtomicOr  ...)


// checks
(NilCheck ...) => (LoweredNilCheck ...)
(IsNonNil ptr) => (SGTU ptr (MOVWconst [0]))
(IsInBounds idx len) => (SGTU len idx)
(IsSliceInBounds idx len) => (XORconst [1] (SGTU idx len))

// pseudo-ops
(GetClosurePtr ...) => (LoweredGetClosurePtr ...)
(GetCallerSP ...) => (LoweredGetCallerSP ...)
(GetCallerPC ...) => (LoweredGetCallerPC ...)

(AtomicOr32  ...) => (LoweredAtomicOr32  ...)

// checks
(NilCheck ...) => (LoweredNilCheck ...)
(IsNonNil ptr) => (SGTU ptr (MOVVconst [0]))
(IsInBounds idx len) => (SGTU len idx)
(IsSliceInBounds idx len) => (XOR (MOVVconst [1]) (SGTU idx len))

// pseudo-ops
(GetClosurePtr ...) => (LoweredGetClosurePtr ...)
(GetCallerSP ...) => (LoweredGetCallerSP ...)
(GetCallerPC ...) => (LoweredGetCallerPC ...)