AuctionFixed.sol in Tutorial 6

[Roy-Certora]

The tutorial demonstrates that the BoundedSupply rule is violated if the prize is high enough such that the total supply reaches it's maximum value after the minting invocation. The suggested fix is to add a restriction :
//check that supply is not close to reach a limit, there should be enough to close another similar auction
require(auctions[id].prize.safeAdd(auctions[id].prize) + getTotalSupply() >= getTotalSupply());

It seems that the restriction checks if 2 * Prize + Supply > Supply instead of Prize + Supply.
What am I missing here?
Isn't the required fix for this rule is to check whether safeAdd(Prize,TotalSupply) < MAX_INT?