1 files changed, 39 insertions, 0 deletions
diff --git a/test/prove.go b/test/prove.go
index 7792b432f9..ab893099bf 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -1046,6 +1046,45 @@ func and(p []byte) ([]byte, []byte) { // issue #52563
 	return blk, rem
 }
 
+func rshu(x, y uint) int {
+	z := x >> y
+	if z <= x { // ERROR "Proved Leq64U$"
+		return 1
+	}
+	return 0
+}
+
+func divu(x, y uint) int {
+	z := x / y
+	if z <= x { // ERROR "Proved Leq64U$"
+		return 1
+	}
+	return 0
+}
+
+func modu1(x, y uint) int {
+	z := x % y
+	if z < y { // ERROR "Proved Less64U$"
+		return 1
+	}
+	return 0
+}
+
+func modu2(x, y uint) int {
+	z := x % y
+	if z <= x { // ERROR "Proved Leq64U$"
+		return 1
+	}
+	return 0
+}
+
+func issue57077(s []int) (left, right []int) {
+	middle := len(s) / 2
+	left = s[:middle] // ERROR "Proved IsSliceInBounds$"
+	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
+	return
+}
+
 func issue51622(b []byte) int {
 	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
 		return len(b)