Include check that deauthorization takes palce

euler-xyz · Mar 6, 2024 · 0b3f12d · 0b3f12d
1 parent 75bc1a1
commit 0b3f12d
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/certora/specs/CER-2-Operator/CER-52-Operator-deauthorization.spec b/certora/specs/CER-2-Operator/CER-52-Operator-deauthorization.spec
@@ -26,6 +26,7 @@ rule operatorDeauthorizationSetOperator {
     // since the function did not revert the caller must be the owner
     assert caller != operator;
     assert caller == getOwnerOf(addressPrefix);
+    assert getOperator(e, addressPrefix, operator) == 0;
 }
 
 rule operatorDeauthorizationSetAccountOperator() {