}

func fEqLeqU(a uint64, f float64) bool {
	return a == 0 && f > Cf2 || a <= 0 && f < -Cf2 // ERROR "Redirect Eq64 based on Eq64$"
}

func fNeqEq(a int, f float64) bool {
	return a != 0 && f > Cf2 || a == 0 && f < -Cf2 // ERROR "Redirect Eq64 based on Neq64$"
}

func fNeqNeq(a int32, f float64) bool {
	return a != 0 && f > Cf2 || a != 0 && f < -Cf2 // ERROR "Redirect Neq32 based on Neq32$"
}

// some such cases, we can redirect the predecessor If block to the
// corresponding successor block directly. For example:
//
//	p:
//	  v11 = Less64 <bool> v10 v8
//	  If v11 goto b else u
//	b: <- p ...
//	  v17 = Leq64 <bool> v10 v8
//	  If v17 goto s else o
//
// We can redirect p to s directly.
//
// The implementation here borrows the framework of the prove pass.
//
//	1, Traverse all blocks of function f to find If blocks.