diff --git a/certora/funnels/automation/ConduitMover.spec b/certora/funnels/automation/ConduitMover.spec index 0b8eee25..a9315a27 100644 --- a/certora/funnels/automation/ConduitMover.spec +++ b/certora/funnels/automation/ConduitMover.spec @@ -7,7 +7,7 @@ methods { function ilk() external returns (bytes32) envfree; function buffer() external returns (address) envfree; function _.withdraw(bytes32 ilk, address gem, uint256 amount) external => withdrawSummary(calledContract, ilk, gem, amount) expect uint256; - function _.deposit(bytes32 ilk, address gem, uint256 amount) external => depositSummary(calledContract, ilk, gem, amount) expect bool; // Forcing to have a return value + function _.deposit(bytes32 ilk, address gem, uint256 amount) external => depositSummary(calledContract, ilk, gem, amount) expect bool; // Forcing to have a return value as otherwise Certora will throw a compiler error } ghost mapping(address => bool) nonZeroExtcodesize; diff --git a/certora/funnels/automation/VaultMinter.spec b/certora/funnels/automation/VaultMinter.spec index ed6576a3..3042b933 100644 --- a/certora/funnels/automation/VaultMinter.spec +++ b/certora/funnels/automation/VaultMinter.spec @@ -5,8 +5,8 @@ methods { function buds(address) external returns (uint256) envfree; function config() external returns (int64, uint32, uint32, uint128) envfree; function vault() external returns (address) envfree; - function _.draw(uint256 wad) external => drawSummary(calledContract, wad) expect bool; // Forcing to have a return value - function _.wipe(uint256 wad) external => wipeSummary(calledContract, wad) expect bool; // Forcing to have a return value + function _.draw(uint256 wad) external => drawSummary(calledContract, wad) expect bool; // Forcing to have a return value as otherwise Certora will throw a compiler error + function _.wipe(uint256 wad) external => wipeSummary(calledContract, wad) expect bool; // Forcing to have a return value as otherwise Certora will throw a compiler error } ghost mapping(address => bool) nonZeroExtcodesize;