diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 697862f986..014535c0a4 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -776,6 +776,8 @@ func prove(f *Func) {
 	ft := newFactsTable(f)
 	ft.checkpoint()
 
+	var lensVars map[*Block][]*Value
+
 	// Find length and capacity ops.
 	for _, b := range f.Blocks {
 		for _, v := range b.Values {
@@ -793,12 +795,24 @@ func prove(f *Func) {
 				}
 				ft.lens[v.Args[0].ID] = v
 				ft.update(b, v, ft.zero, signed, gt|eq)
+				if v.Args[0].Op == OpSliceMake {
+					if lensVars == nil {
+						lensVars = make(map[*Block][]*Value)
+					}
+					lensVars[b] = append(lensVars[b], v)
+				}
 			case OpSliceCap:
 				if ft.caps == nil {
 					ft.caps = map[ID]*Value{}
 				}
 				ft.caps[v.Args[0].ID] = v
 				ft.update(b, v, ft.zero, signed, gt|eq)
+				if v.Args[0].Op == OpSliceMake {
+					if lensVars == nil {
+						lensVars = make(map[*Block][]*Value)
+					}
+					lensVars[b] = append(lensVars[b], v)
+				}
 			}
 		}
 	}
@@ -852,9 +866,22 @@ func prove(f *Func) {
 		switch node.state {
 		case descend:
 			ft.checkpoint()
+
+			// Entering the block, add the block-depending facts that we collected
+			// at the beginning: induction variables and lens/caps of slices.
 			if iv, ok := indVars[node.block]; ok {
 				addIndVarRestrictions(ft, parent, iv)
 			}
+			if lens, ok := lensVars[node.block]; ok {
+				for _, v := range lens {
+					switch v.Op {
+					case OpSliceLen:
+						ft.update(node.block, v, v.Args[0].Args[1], signed, eq)
+					case OpSliceCap:
+						ft.update(node.block, v, v.Args[0].Args[2], signed, eq)
+					}
+				}
+			}
 
 			if branch != unknown {
 				addBranchRestrictions(ft, parent, branch)
diff --git a/test/prove.go b/test/prove.go
index 7643031c62..6629982ba8 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -678,6 +678,30 @@ func oforuntil(b []int) {
 	}
 }
 
+func atexit(foobar []func()) {
+	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
+		f := foobar[i]
+		foobar = foobar[:i] // ERROR "IsSliceInBounds"
+		f()
+	}
+}
+
+func make1(n int) []int {
+	s := make([]int, n)
+	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+		s[i] = 1 // ERROR "Proved IsInBounds$"
+	}
+	return s
+}
+
+func make2(n int) []int {
+	s := make([]int, n)
+	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+		s[i] = 1 // ERROR "Proved IsInBounds$"
+	}
+	return s
+}
+
 // The range tests below test the index variable of range loops.
 
 // range1 compiles to the "efficiently indexable" form of a range loop.
@@ -862,13 +886,13 @@ func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
 		return 0
 	}
 	if j8 >= 0 && j8 < 22 {
-		return x[j8]  // ERROR "Proved IsInBounds$"
+		return x[j8] // ERROR "Proved IsInBounds$"
 	}
 	if j16 >= 0 && j16 < 22 {
-		return x[j16]  // ERROR "Proved IsInBounds$"
+		return x[j16] // ERROR "Proved IsInBounds$"
 	}
 	if j32 >= 0 && j32 < 22 {
-		return x[j32]  // ERROR "Proved IsInBounds$"
+		return x[j32] // ERROR "Proved IsInBounds$"
 	}
 	return 0
 }
@@ -878,13 +902,13 @@ func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
 		return 0
 	}
 	if j8 >= 0 && j8 < 22 {
-		return x[j8]  // ERROR "Proved IsInBounds$"
+		return x[j8] // ERROR "Proved IsInBounds$"
 	}
 	if j16 >= 0 && j16 < 22 {
-		return x[j16]  // ERROR "Proved IsInBounds$"
+		return x[j16] // ERROR "Proved IsInBounds$"
 	}
 	if j32 >= 0 && j32 < 22 {
-		return x[j32]  // ERROR "Proved IsInBounds$"
+		return x[j32] // ERROR "Proved IsInBounds$"
 	}
 	return 0
 }
@@ -894,7 +918,7 @@ func signExt32to64Fence(x []int, j int32) int {
 	if x[j] != 0 {
 		return 1
 	}
-	if j > 0 && x[j-1] != 0 {  // ERROR "Proved IsInBounds$"
+	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
 		return 1
 	}
 	return 0
@@ -904,7 +928,7 @@ func zeroExt32to64Fence(x []int, j uint32) int {
 	if x[j] != 0 {
 		return 1
 	}
-	if j > 0 && x[j-1] != 0 {  // ERROR "Proved IsInBounds$"
+	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
 		return 1
 	}
 	return 0