From 2343213e0d15c3e47d2895749e3c662898d573bf Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Mon, 4 Mar 2024 10:12:41 +0100 Subject: [PATCH] chore(StakeVault.spec): comment out purposefully failing rule This rule is only used for debugging purposes and serves no function for production formal verification. Hence we're commenting it out. --- certora/specs/StakeVault.spec | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec index 5532ebd..2d3d32f 100644 --- a/certora/specs/StakeVault.spec +++ b/certora/specs/StakeVault.spec @@ -16,6 +16,10 @@ rule reachability(method f){ satisfy true; } +/* + The rule below is commented out as it's merely used to easily have the + prover find all functions that change balances. + rule whoChangeERC20Balance(method f) { simplification(); @@ -26,3 +30,4 @@ rule whoChangeERC20Balance(method f) f(e,args); assert before == staked.balanceOf(user); } +*/