Skip to content
This repository was archived by the owner on Sep 27, 2023. It is now read-only.
This repository was archived by the owner on Sep 27, 2023. It is now read-only.

AuctionFixed.sol in Tutorial 6 #3

@Roy-Certora

Description

@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?

Metadata

Metadata

Assignees

No one assigned

    Labels

    help wantedExtra attention is neededinvalidThis doesn't seem right

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions