From 728e2c8899acf9c7b3e861dbcb9b3252898a9c2e Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 14 Mar 2023 11:49:16 +0100 Subject: [PATCH] fix --- certora/specs/GovernorFunctions.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index 35fc57365..04d405658 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -123,14 +123,14 @@ rule queue(uint256 pId, env e) { // effect assert success => ( - state(e, pId) == QUEUED() + state(e, pId) == QUEUED() && !queuedBefore && isQueued(pId) ); // no side-effect - assert state(e, otherId) != otherStateBefore => otherId == pId; - assert isQueued(otherId) != queuedBefore => otherId == pId; + assert state(e, otherId) != otherStateBefore => otherId == pId; + assert isQueued(otherId) != otherQueuedBefore => otherId == pId; } /*