fix filtered blocks

safe-global · Jun 23, 2023 · 7c86420 · 7c86420
1 parent 7913fc7
commit 7c86420
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -145,6 +145,7 @@ invariant noOwnerDeadEnds(address dead, address lost)
 
 invariant noSelfPoint(address self)
     self != 1 && self != 0 => getOwner(self) != self
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
     {
         preserved {
             requireInvariant noOwnerDeadEnds(getOwner(1), 1);