diff --git a/certora/specs/ERC1155Burnable.spec b/certora/specs/ERC1155Burnable.spec index 3fd4caf7d..d38731079 100644 --- a/certora/specs/ERC1155Burnable.spec +++ b/certora/specs/ERC1155Burnable.spec @@ -14,7 +14,7 @@ rule onlyApprovedCanReduceBalance { uint256 balanceAfter = balanceOf(holder, token); - assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender); + assert balanceAfter < balanceBefore => e.msg.sender == holder || isApprovedForAll(holder, e.msg.sender); // TODO add assert message } /// This rule should always fail. diff --git a/certora/specs/ERC1155Pausable.spec b/certora/specs/ERC1155Pausable.spec index 81fe40029..4271c07df 100644 --- a/certora/specs/ERC1155Pausable.spec +++ b/certora/specs/ERC1155Pausable.spec @@ -36,8 +36,6 @@ filtered { "Transfer methods must revert in a paused contract"; } - -/// Calling pause must pause an unpaused contract. /// When a contract is in an unpaused state, calling pause() must pause. rule pauseMethodPausesContract { require !paused();