debugging handlerCalledIfSet rule, included an invariant that handler…

… is never self nor the zero address, and now the Prover is misbehaving. Committing here and opening a ticket

certora/specs/v1.5/Fallback.spec

@@ -10,7 +10,7 @@ methods {
     function getFallbackHandler() external returns (address) envfree;
     function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true);
 
-    unresolved external in SafeHarness._() => DISPATCH(use_fallback=true) [
+    unresolved external in safe._ => DISPATCH(use_fallback=true) [
         fallbackHandler._
     ] default NONDET;
 
@@ -49,6 +49,13 @@ invariant fallbackHanlderNeverSelf()
         f -> f.selector != sig:simulateAndRevert(address,bytes).selector 
     }
 
+/// @status TODOviolation: https://prover.certora.com/output/39601/cfde79a198b34aa78dbc5714a5e416b6?anonymousKey=f3e41441fbb2f941efc2033b10cccdee7c84249e
+invariant fallbackHanlderNeverZero() 
+    getFallbackHandler() != 0
+    filtered { 
+        f -> f.selector != sig:simulateAndRevert(address,bytes).selector 
+    }
+
 /// @dev for soundness of fallbackHanlderNeverSelf, we prove a rule that simulateAndRevert always reverts
 /// @status Done: https://prover.certora.com/output/39601/38653935d0db460994d1a8c5bfdf57bb?anonymousKey=988218ca4f784fd27ea96fd2f14644719e2e9468
 rule simulateAndRevertReverts(address caddr, bytes b) {
@@ -128,10 +135,13 @@ rule hanlderCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallbac
 }
 
 /// @dev a handler is called under expected conditions
-/// @status violated due to dispatching issues (problem with the Prover)
+/// @status violated due to Prover bug: https://prover.certora.com/output/39601/c3379d53af8d4639b2236d0be41af6b9?anonymousKey=df18d967edb98b99e5851a280d84728ce18724cb
 rule handlerCalledIfSet() {
     env e;
 
+    requireInvariant fallbackHanlderNeverSelf();
+    requireInvariant fallbackHanlderNeverZero();
+
     // the fallback handler is in the scene
     require (getFallbackHandler() == fallbackHandler);