diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index 4e1270a7e..8d185ab68 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -559,18 +559,6 @@ function expectRevert(bytes4 msg) external;
 function expectRevert(bytes calldata msg) external;
 ```
 
-All cheat code calls which take place while `expectRevert` is active are ignored.
-
-```k
-    rule [cheatcode.call.ignoreCalls]:
-         <k> #cheatcode_call _ _ => .K ... </k>
-         <expectedRevert>
-           <isRevertExpected> true </isRevertExpected>
-           ...
-         </expectedRevert>
-      [priority(35)]
-```
-
 We use the `#next[OP]` to identify OpCodes that can revert and insert a `#checkRevert` production used to examine the end of each call/create in KEVM.
 The check will be inserted only if the current depth is the same as the depth at which the `expectRevert` cheat code was used.
 WThe `#checkRevert` will be used to compare the status code of the execution and the output of the call against the expect reason provided.
@@ -579,23 +567,37 @@ WThe `#checkRevert` will be used to compare the status code of the execution and
     rule [foundry.set.expectrevert.1]:
          <k> #next [ _OP:CallOp ] ~> (.K => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
          <callDepth> CD </callDepth>
-         <wordStack> _ : _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
+         <wordStack> _ : ACCTTO : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
          <expectedRevert>
            <isRevertExpected> true </isRevertExpected>
            <expectedDepth> CD </expectedDepth>
            ...
          </expectedRevert>
+         requires ACCTTO =/=Int #address(FoundryCheat)
       [priority(32)]
 
     rule [foundry.set.expectrevert.2]:
          <k> #next [ _OP:CallSixOp ] ~> (.K => #checkRevert ~> #updateRevertOutput RETSTART RETWIDTH) ~> #execute ... </k>
          <callDepth> CD </callDepth>
-         <wordStack> _ : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
+         <wordStack> _ : ACCTTO : _ : _ : _ : RETSTART : RETWIDTH : _WS </wordStack>
+         <expectedRevert>
+           <isRevertExpected> true </isRevertExpected>
+           <expectedDepth> CD </expectedDepth>
+           ...
+         </expectedRevert>
+         requires ACCTTO =/=Int #address(FoundryCheat)
+      [priority(32)]
+
+    rule [foundry.clear.expectrevert]:
+         <k> #next [ DELEGATECALL ] ~> (.K => #clearExpectRevert) ~> #execute ... </k>
+         <callDepth> CD </callDepth>
+         <wordStack> _ : ACCTTO : _ : _ : _ : _ : _ : _WS </wordStack>
          <expectedRevert>
            <isRevertExpected> true </isRevertExpected>
            <expectedDepth> CD </expectedDepth>
            ...
          </expectedRevert>
+         requires ACCTTO ==Int #address(FoundryCheat)
       [priority(32)]
 
     rule [foundry.set.expectrevert.3]:
diff --git a/src/tests/integration/test-data/foundry-prove-skip b/src/tests/integration/test-data/foundry-prove-skip
index c4f39567b..f6e375626 100644
--- a/src/tests/integration/test-data/foundry-prove-skip
+++ b/src/tests/integration/test-data/foundry-prove-skip
@@ -113,7 +113,6 @@ MockCallRevertTest.testMockCallRevertResetsMockCall()
 MockCallRevertTest.testMockCallRevertWithCall()
 MockCallRevertTest.testMockCallEmptyAccount()
 OwnerUpOnlyTest.testFailIncrementAsNotOwner()
-OwnerUpOnlyTest.testIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsOwner()
 PlainPrankTest.testFail_startPrank_existingAlready()
 PrankTest.testAddAsOwner(uint256)