test/fixedbugs/issue80517_3.go

// run

// Copyright 2026 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.

// Same time-traveling prove bug as issue80517_2.go, but the victims are a
// signed division and a signed modulo. make([]byte, n) teaches prove that
// n >= 0 only after it runs; a buggy prove lets that fact travel back and
// rewrites the earlier n/4 and n%3 into unsigned operations, corrupting
// the result for negative n.

package main

var sink []byte

//go:noinline
func trigger(n int) (q, r int) {
	defer func() { recover() }()
	if n < 100 {
		q = n / 4              // signed division
		r = n % 3              // signed modulo
		sink = make([]byte, n) // only asserts n >= 0 after this point
	}
	return
}

func main() {
	if q, r := trigger(-8); q != -2 || r != -2 {
		println("n/4 =", q, "want -2;  n%3 =", r, "want -2")
		panic("prove miscompiled a signed div/mod")
	}
}