From 43e37f0184b09768a85d40ffd07553965743c69b Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Thu, 25 Nov 2021 16:25:40 +0200 Subject: [PATCH] executedImplyStartAndEndDateNonZero inv fix --- certora/specs/GovernorBase.spec | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index ef2d68baf..8487804ab 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -98,9 +98,9 @@ function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { // To use env with general preserved block disable type checking [--disableLocalTypeChecking] invariant startAndEndDatesNonZero(uint256 pId) proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0 - /*{ preserved with (env e){ + { preserved with (env e){ require e.block.number > 0; - }}*/ + }} /* @@ -121,7 +121,8 @@ invariant canceledImplyStartAndEndDateNonZero(uint pId) invariant executedImplyStartAndEndDateNonZero(uint pId) isExecuted(pId) => proposalSnapshot(pId) != 0 { preserved with (env e){ - require e.block.number > 0; + requireInvariant startAndEndDatesNonZero(pId); + require e.block.number > 0; }}